aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Machregsaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc/Machregsaux.ml')
-rw-r--r--powerpc/Machregsaux.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index 8c3017ff..664f71a0 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -22,13 +22,13 @@ let _ =
(fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
Machregs.register_names
-let scratch_register_names = [ "R0" ]
+let is_scratch_register s = s = "R0" || s = "r0"
let name_of_register r =
try Some (Hashtbl.find register_names r) with Not_found -> None
let register_by_name s =
- Machregs.register_by_name (coqstring_of_camlstring (String.uppercase s))
+ Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
let can_reserve_register r =
List.mem r Conventions1.int_callee_save_regs