diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-02 07:46:23 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-05-02 07:46:23 +0000 |
| commit | e96b2dd600239a44b5d857d23dfacd4733583fe4 (patch) | |
| tree | 734c9dacb97310fd58e533781f5467647954a660 /powerpc | |
| parent | 91558f0db1e919fbb99d1f830179688fea4002bd (diff) | |
| download | compcert-kvx-e96b2dd600239a44b5d857d23dfacd4733583fe4.tar.gz compcert-kvx-e96b2dd600239a44b5d857d23dfacd4733583fe4.zip | |
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.ml | 6 | ||||
| -rw-r--r-- | powerpc/Machregsaux.mli | 1 |
2 files changed, 7 insertions, 0 deletions
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml index b729d100..2ff3cd92 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 6d819882..400c5abb 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 |