aboutsummaryrefslogtreecommitdiffstats
path: root/arm
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-06-21 15:49:07 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-06-21 15:49:07 +0200
commit7237ccb621d58b2c86ef250f1c3e3ffd29260955 (patch)
treee770b9a015468751e0b006496fa7518402c88c96 /arm
parent8f444dec7112e5b125bf3ead8481ae0f698bbb96 (diff)
downloadcompcert-kvx-7237ccb621d58b2c86ef250f1c3e3ffd29260955.tar.gz
compcert-kvx-7237ccb621d58b2c86ef250f1c3e3ffd29260955.zip
Remove code that will is deprecated in ocaml 4.03
Most of the code can be String.uppercase usages can either be replaced by a more specialized version of coqstring_of_camlstring (which is also slightly more effecient) or by specialized checks that reject wrong code earlier. Bug 19187
Diffstat (limited to 'arm')
-rw-r--r--arm/Machregsaux.ml4
-rw-r--r--arm/Machregsaux.mli2
2 files changed, 3 insertions, 3 deletions
diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml
index d59ec8b8..ce5c67f6 100644
--- a/arm/Machregsaux.ml
+++ b/arm/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 = [ "R14" ]
+let is_scratch_register s = s = "R14" || s = "r14"
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
diff --git a/arm/Machregsaux.mli b/arm/Machregsaux.mli
index d4877a62..9404568d 100644
--- a/arm/Machregsaux.mli
+++ b/arm/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