aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/ExtendedAsm.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 /cparser/ExtendedAsm.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 'cparser/ExtendedAsm.ml')
-rw-r--r--cparser/ExtendedAsm.ml7
1 files changed, 3 insertions, 4 deletions
diff --git a/cparser/ExtendedAsm.ml b/cparser/ExtendedAsm.ml
index c3d80272..fc228aca 100644
--- a/cparser/ExtendedAsm.ml
+++ b/cparser/ExtendedAsm.ml
@@ -159,10 +159,9 @@ let transf_outputs loc env = function
let check_clobbers loc clob =
List.iter
(fun c ->
- let c' = String.uppercase c in
- if Machregsaux.register_by_name c' <> None
- || List.mem c' Machregsaux.scratch_register_names
- || c' = "MEMORY" || c' = "CC"
+ if Machregsaux.register_by_name c <> None
+ || Machregsaux.is_scratch_register c
+ || c = "memory" || c = "cc" (* GCC does not accept MEMORY or CC *)
then ()
else error "%aError: unrecognized asm register clobber '%s'"
formatloc loc c)