aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Machregsaux.ml
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/Machregsaux.ml
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/Machregsaux.ml')
-rw-r--r--arm/Machregsaux.ml4
1 files changed, 2 insertions, 2 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