diff options
| -rw-r--r-- | Makefile.extr | 6 | ||||
| -rwxr-xr-x | configure | 14 | ||||
| -rw-r--r-- | cparser/Elab.ml | 6 | ||||
| -rw-r--r-- | lib/Camlcoq.ml | 6 | ||||
| -rw-r--r-- | lib/Printlines.ml | 6 |
5 files changed, 21 insertions, 17 deletions
diff --git a/Makefile.extr b/Makefile.extr index 87d5107d..324feea9 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -38,9 +38,9 @@ INCLUDES=$(patsubst %,-I %, $(DIRS)) # 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 -3 -strict-sequence -extraction/%.cmx: WARNINGS +=-w -20 -extraction/%.cmo: WARNINGS +=-w -20 +WARNINGS=-w +a-4-9-29 -strict-sequence -safe-string -warn-error +a +extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45 +extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45 COMPFLAGS+=-g $(INCLUDES) $(MENHIR_INCLUDES) $(WARNINGS) @@ -283,15 +283,19 @@ esac echo "Testing OCaml... " | tr -d '\n' ocaml_ver=`ocamlopt -version 2>/dev/null` case "$ocaml_ver" in - 4.*) + 4.00.*|4.01.*) + echo "version $ocaml_ver -- UNSUPPORTED" + echo "Error: CompCert requires OCaml version 4.02 or later." + missingtools=true;; + 4.0*) echo "version $ocaml_ver -- good!";; ?.*) echo "version $ocaml_ver -- UNSUPPORTED" - echo "Error: CompCert requires OCaml version 4.00 or later." + echo "Error: CompCert requires OCaml version 4.02 or later." missingtools=true;; *) echo "NOT FOUND" - echo "Error: make sure OCaml version 4.00 or later is installed." + echo "Error: make sure OCaml version 4.02 or later is installed." missingtools=true;; esac @@ -334,7 +338,7 @@ for mk in make gmake gnumake; do break;; esac done -if test -z "$make"; then +if test -z "$make"; then echo "NOT FOUND" echo "Error: make sure GNU Make version 3.80 or later is installed." missingtools=true @@ -391,7 +395,7 @@ cat >> Makefile.config <<'EOF' ARCH= # Hardware variant -# MODEL=ppc32 # for plain PowerPC +# MODEL=ppc32 # for plain PowerPC # MODEL=ppc64 # for PowerPC with 64-bit instructions # MODEL=e5500 # for Freescale e5500 PowerPC variant # MODEL=armv6 # for ARM diff --git a/cparser/Elab.ml b/cparser/Elab.ml index ceab0aa5..fb75c687 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -253,11 +253,11 @@ let elab_string_literal loc wide chars = if wide then CWStr chars else begin - let res = String.create (List.length chars) in + let res = Bytes.create (List.length chars) in List.iteri - (fun i c -> res.[i] <- Char.unsafe_chr (Int64.to_int c)) + (fun i c -> Bytes.set res i (Char.unsafe_chr (Int64.to_int c))) chars; - CStr res + CStr (Bytes.to_string res) end let elab_constant loc = function diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index c5fb2e55..90c3ab3f 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -307,11 +307,11 @@ let first_unused_ident () = !next_atom (* Strings *) let camlstring_of_coqstring (s: char list) = - let r = String.create (List.length s) in + let r = Bytes.create (List.length s) in let rec fill pos = function | [] -> r - | c :: s -> r.[pos] <- c; fill (pos + 1) s - in fill 0 s + | c :: s -> Bytes.set r pos c; fill (pos + 1) s + in Bytes.to_string (fill 0 s) let coqstring_of_camlstring s = let rec cstring accu pos = diff --git a/lib/Printlines.ml b/lib/Printlines.ml index e0805f15..453096bc 100644 --- a/lib/Printlines.ml +++ b/lib/Printlines.ml @@ -48,7 +48,7 @@ let forward b dest = (* Position [b] to the beginning of line [dest], which must be less than the current line. *) -let backward_buf = lazy (String.create 65536) +let backward_buf = lazy (Bytes.create 65536) (* 65536 to match [IO_BUFFER_SIZE] in the OCaml runtime. lazy to allocate on demand. *) @@ -65,13 +65,13 @@ let backward b dest = seek_in b.chan 0; b.lineno <- 1 end else begin - let pos' = max 0 (pos - String.length buf) in + let pos' = max 0 (pos - Bytes.length buf) in let len = pos - pos' in seek_in b.chan pos'; really_input b.chan buf 0 len; backward pos' (pos - pos') end - end else if buf.[idx-1] = '\n' then begin + end else if Bytes.get buf (idx-1) = '\n' then begin (* Reached beginning of current line *) if b.lineno = dest then begin (* Found line number dest *) |