diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-06-21 15:49:07 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-06-21 15:49:07 +0200 |
commit | 7237ccb621d58b2c86ef250f1c3e3ffd29260955 (patch) | |
tree | e770b9a015468751e0b006496fa7518402c88c96 | |
parent | 8f444dec7112e5b125bf3ead8481ae0f698bbb96 (diff) | |
download | compcert-7237ccb621d58b2c86ef250f1c3e3ffd29260955.tar.gz compcert-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
-rw-r--r-- | Makefile.extr | 4 | ||||
-rw-r--r-- | arm/Machregsaux.ml | 4 | ||||
-rw-r--r-- | arm/Machregsaux.mli | 2 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 2 | ||||
-rw-r--r-- | cparser/Elab.ml | 7 | ||||
-rw-r--r-- | cparser/ExtendedAsm.ml | 7 | ||||
-rw-r--r-- | ia32/Machregsaux.ml | 4 | ||||
-rw-r--r-- | ia32/Machregsaux.mli | 2 | ||||
-rw-r--r-- | lib/Camlcoq.ml | 10 | ||||
-rw-r--r-- | powerpc/Machregsaux.ml | 4 | ||||
-rw-r--r-- | powerpc/Machregsaux.mli | 2 |
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 |