aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
diff options
context:
space:
mode:
Diffstat (limited to 'ia32')
-rw-r--r--ia32/Machregsaux.ml4
-rw-r--r--ia32/Machregsaux.mli2
2 files changed, 3 insertions, 3 deletions
diff --git a/ia32/Machregsaux.ml b/ia32/Machregsaux.ml
index 3ec9596a..473e0602 100644
--- a/ia32/Machregsaux.ml
+++ b/ia32/Machregsaux.ml
@@ -22,12 +22,12 @@ let _ =
(fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
Machregs.register_names
-let scratch_register_names = []
+let is_scratch_register r = false
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 = Conventions1.is_callee_save r
diff --git a/ia32/Machregsaux.mli b/ia32/Machregsaux.mli
index d4877a62..9404568d 100644
--- a/ia32/Machregsaux.mli
+++ b/ia32/Machregsaux.mli
@@ -14,5 +14,5 @@
val name_of_register: Machregs.mreg -> string option
val register_by_name: string -> Machregs.mreg option
-val scratch_register_names: string list
+val is_scratch_register: string -> bool
val can_reserve_register: Machregs.mreg -> bool