summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-05-02 07:46:23 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-05-02 07:46:23 +0000
commite96b2dd600239a44b5d857d23dfacd4733583fe4 (patch)
tree734c9dacb97310fd58e533781f5467647954a660 /powerpc
parent91558f0db1e919fbb99d1f830179688fea4002bd (diff)
Pretty-printers for RTL and LTL. Not yet well integrated.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1332 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/Machregsaux.ml6
-rw-r--r--powerpc/Machregsaux.mli1
2 files changed, 7 insertions, 0 deletions
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index b729d10..2ff3cd9 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -33,6 +33,12 @@ let register_names = [
("F11", FT1); ("F12", FT2); ("F0", FT3)
]
+let name_of_register r =
+ let rec rev_assoc = function
+ | [] -> None
+ | (a, b) :: rem -> if b = r then Some a else rev_assoc rem
+ in rev_assoc register_names
+
let register_by_name s =
try
Some(List.assoc (String.uppercase s) register_names)
diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli
index 6d81988..400c5ab 100644
--- a/powerpc/Machregsaux.mli
+++ b/powerpc/Machregsaux.mli
@@ -14,3 +14,4 @@
val register_by_name: string -> Machregs.mreg option
val can_reserve_register: Machregs.mreg -> bool
+val name_of_register: Machregs.mreg -> string option