11 files changed, 29 insertions, 19 deletions

diff --git a/Makefile.extr b/Makefile.extr
index faec34a6..51dbd767 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -35,10 +35,8 @@ DIRS=extraction \
 INCLUDES=$(patsubst %,-I %, $(DIRS))
 
 # Control of warnings:
-# warning 3 = deprecated feature.  Turned off for OCaml 4.02 (bytes vs strings)
-# warning 20 = unused function argument.  There are some in extracted code
 
-WARNINGS=-w +a-3-4-9-27 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03
+WARNINGS=-w +a-4-9-27 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03
 extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45
 extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45
 cparser/pre_parser.cmx: WARNINGS += -w -41
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
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 16e8a80d..decbf58b 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -876,7 +876,7 @@ let convertAsm loc env txt outputs inputs clobber =
   let (txt', output', inputs') =
     ExtendedAsm.transf_asm loc env txt outputs inputs clobber in
   let clobber' =
-    List.map (fun s -> coqstring_of_camlstring (String.uppercase s)) clobber in
+    List.map (fun s -> coqstring_uppercase_ascii_of_camlstring s) clobber in
   let ty_res =
     match output' with None -> TVoid [] | Some e -> e.etyp in
   (* Build the Ebuiltin expression *)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index cdae2fd9..722303d2 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -154,7 +154,10 @@ let integer_representable v ik =
     v >= 0L && v < Int64.shift_left 1L (bitsize - 1)
 
 let elab_int_constant loc s0 =
-  let s = String.uppercase s0 in
+  let s = String.map (fun d -> match d with
+  | '0'..'9' | 'A'..'F' | 'L' | 'U' | 'X' -> d
+  | 'a'..'f' | 'l' | 'u' | 'x' -> Char.chr (Char.code d - 32)
+  | _ -> error loc "bad digit '%c' in integer literal '%s'" d s0; d) s0 in
   (* Determine possible types and chop type suffix *)
   let (s, dec_kinds, hex_kinds) =
     if has_suffix s "ULL" || has_suffix s "LLU" then
@@ -190,7 +193,7 @@ let elab_int_constant loc s0 =
         error loc "integer literal '%s' is too large" s0;
         0L
     | Bad_digit ->
-        error loc "bad digit in integer literal '%s'" s0;
+        (*error loc "bad digit in integer literal '%s'" s0;*) (* Is caught earlier *)
         0L
   in
   (* Find smallest allowable type that fits *)
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)
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
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 90c3ab3f..7e8a1018 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -318,6 +318,16 @@ let coqstring_of_camlstring s =
     if pos < 0 then accu else cstring (s.[pos] :: accu) (pos - 1)
   in cstring [] (String.length s - 1)
 
+let coqstring_uppercase_ascii_of_camlstring s =
+  let rec cstring accu pos =
+    if pos < 0 then accu else
+    let d = if s.[pos] >= 'a' && s.[pos] <= 'z' then
+      Char.chr (Char.code s.[pos] - 32)
+    else
+      s.[pos] in
+    cstring (d :: accu) (pos - 1)
+  in cstring [] (String.length s - 1)
+
 (* Floats *)
 
 let coqfloat_of_camlfloat f =
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
diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli
index d4877a62..9404568d 100644
--- a/powerpc/Machregsaux.mli
+++ b/powerpc/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