diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/Machregsaux.ml | 2 | ||||
-rw-r--r-- | powerpc/Machregsaux.mli | 3 |
2 files changed, 4 insertions, 1 deletions
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml index f8253ca4..ba111089 100644 --- a/powerpc/Machregsaux.ml +++ b/powerpc/Machregsaux.ml @@ -33,6 +33,8 @@ let register_names = [ ("F28", F28); ("F29", F29); ("F30", F30); ("F31", F31) ] +let scratch_register_names = [ "R0" ] + let name_of_register r = let rec rev_assoc = function | [] -> None diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli index 90343b5b..f0feec96 100644 --- a/powerpc/Machregsaux.mli +++ b/powerpc/Machregsaux.mli @@ -12,7 +12,8 @@ (** Auxiliary functions on machine registers *) +val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option +val scratch_register_names: string list val can_reserve_register: Machregs.mreg -> bool -val name_of_register: Machregs.mreg -> string option val mregs_of_clobber: Camlcoq.atom list -> Machregs.mreg list |