Compile with -safe-string to help transition toward OCaml 4.06.0.

Makefile.in

@@ -98,8 +98,8 @@ INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
 
 WARNINGS = A-4-9-41-44-45-50-52@5@48
 
-OFLAGS = -w $(WARNINGS) -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
-BFLAGS = -w $(WARNINGS) -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
+OFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
+BFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
 
 OLINKFLAGS = -linkall $(EXTCMXA)
 BLINKFLAGS = -linkall $(EXTCMA)

src/driver/prove_client.ml

@@ -55,12 +55,12 @@ let send_request_string msg =
       let to_write = String.length msg in
       let rec write pointer =
         if pointer < to_write then
-          let written = Unix.write sock msg pointer (to_write - pointer) in
+          let written = Unix.write_substring sock msg pointer (to_write - pointer) in
           write (pointer + written)
       in write 0
 
 let read_from_client =
-  let buf = String.make 1024 ' ' in
+  let buf = Bytes.make 1024 ' ' in
   fun blocking ->
     match !socket with
     | None -> raise NotConnected
@@ -73,7 +73,7 @@ let read_from_client =
         in
         if do_read then
           let read = Unix.read sock buf 0 1024 in
-          String.sub buf 0 read
+          Bytes.sub_string buf 0 read
         else ""
 
 (* TODO/FIXME: should we be able to change this setting when

src/printer/coq.ml

@@ -489,10 +489,10 @@ let read_old_proof =
           Vernacular
         end in
       let len = pos_in ch - !start in
-      let s = Strings.create len in
+      let s = Bytes.create len in
       seek_in ch !start;
       really_input ch s 0 len;
-      Query (name, k, s)
+      Query (name, k, Bytes.unsafe_to_string s)
   with StringValue s -> Other s
 
 (* Load old-style proofs where users were confined to a few sections. *)

src/session/compress.mli

@@ -11,7 +11,7 @@
 
 val compression_supported : bool
 
-module type S = sig 
+module type S = sig
 
 type out_channel
 
@@ -19,7 +19,7 @@ val open_out: string -> out_channel
 
 val output_char: out_channel -> char -> unit
 
-val output: out_channel -> string -> int -> int -> unit
+val output_substring: out_channel -> string -> int -> int -> unit
 
 val output_string: out_channel -> string -> unit
 
@@ -29,9 +29,9 @@ type in_channel
 
 val open_in: string -> in_channel
 
-val input: in_channel -> string -> int -> int -> int
+val input: in_channel -> bytes -> int -> int -> int
 
-val really_input: in_channel -> string -> int -> int -> unit
+val really_input: in_channel -> bytes -> int -> int -> unit
 
 val input_char: in_channel -> char
 

src/session/compress_none.ml

@@ -9,9 +9,10 @@
 (*                                                                  *)
 (********************************************************************)
 
+#13 "src/session/compress_none.ml"
 let compression_supported = false
 
-module type S = sig 
+module type S = sig
 
 type out_channel
 
@@ -19,7 +20,7 @@ val open_out: string -> out_channel
 
 val output_char: out_channel -> char -> unit
 
-val output: out_channel -> string -> int -> int -> unit
+val output_substring: out_channel -> string -> int -> int -> unit
 
 val output_string: out_channel -> string -> unit
 
@@ -29,9 +30,9 @@ type in_channel
 
 val open_in: string -> in_channel
 
-val input: in_channel -> string -> int -> int -> int
+val input: in_channel -> bytes -> int -> int -> int
 
-val really_input: in_channel -> string -> int -> int -> unit
+val really_input: in_channel -> bytes -> int -> int -> unit
 
 val input_char: in_channel -> char
 

src/session/compress_z.ml

@@ -9,9 +9,10 @@
 (*                                                                  *)
 (********************************************************************)
 
+#13 "src/session/compress_z.ml"
 let compression_supported = true
 
-module type S = sig 
+module type S = sig
 
 type out_channel
 
@@ -19,7 +20,7 @@ val open_out: string -> out_channel
 
 val output_char: out_channel -> char -> unit
 
-val output: out_channel -> string -> int -> int -> unit
+val output_substring: out_channel -> string -> int -> int -> unit
 
 val output_string: out_channel -> string -> unit
 
@@ -29,9 +30,9 @@ type in_channel
 
 val open_in: string -> in_channel
 
-val input: in_channel -> string -> int -> int -> int
+val input: in_channel -> bytes -> int -> int -> int
 
-val really_input: in_channel -> string -> int -> int -> unit
+val really_input: in_channel -> bytes -> int -> int -> unit
 
 val input_char: in_channel -> char
 
@@ -50,9 +51,9 @@ let open_out fn = Gzip.open_out ~level:6 fn
 
 let output_char = Gzip.output_char
 
-let output = Gzip.output
+let output_substring = Gzip.output_substring
 
-let output_string ch s = output ch s 0 (String.length s)
+let output_string ch s = output_substring ch s 0 (String.length s)
 
 let close_out = Gzip.close_out
 

src/session/session.ml

@@ -1559,9 +1559,9 @@ exception SessionFileError of string
 module ReadShapes (C:Compress.S) = struct
 
 let shape = Buffer.create 97
-let sum = Strings.create 32
 
 let read_sum_and_shape ch =
+  let sum = Bytes.create 32 in
   let nsum = C.input ch sum 0 32 in
   if nsum = 0 then raise End_of_file;
   if nsum <> 32 then
@@ -1572,7 +1572,7 @@ let read_sum_and_shape ch =
         raise
           (ShapesFileError
              ("shapes files corrupted (checksum '" ^
-                 (String.sub sum 0 nsum) ^
+                 (Bytes.sub_string sum 0 nsum) ^
                  "' too short), ignored"))
     end;
   if try C.input_char ch <> ' ' with End_of_file -> true then
@@ -1588,7 +1588,7 @@ let read_sum_and_shape ch =
     with
       | End_of_file ->
         raise (ShapesFileError "shapes files corrupted (premature end of file), ignored");
-      | Exit -> Strings.copy sum, Buffer.contents shape
+      | Exit -> Bytes.unsafe_to_string sum, Buffer.contents shape
 
 
   let use_shapes = ref true

src/util/cmdline.ml

@@ -43,10 +43,7 @@ let cmdline_split s =
     | '\\' -> cstate := Escape
     | c when is_blank c ->
         let n = Queue.length cur_arg in
-        let s = Strings.create n in
-        for i = 0 to pred n do
-          Strings.set s i (Queue.take cur_arg)
-        done;
+        let s = String.init n (fun _ -> Queue.take cur_arg) in
         argv := s :: !argv;
         cstate := Blank
     | c -> Queue.add c cur_arg

src/util/lexlib.mll

@@ -98,10 +98,10 @@ and string = parse
         let nb = ref 0 in
         String.iter (fun c -> if c = '_' then incr nb) s;
         !nb in
-      let t = Strings.create (String.length s - count) in
+      let t = Bytes.create (String.length s - count) in
       let i = ref 0 in
-      String.iter (fun c -> if c <> '_' then (Strings.set t !i c; incr i)) s;
-      t
+      String.iter (fun c -> if c <> '_' then (Bytes.set t !i c; incr i)) s;
+      Bytes.unsafe_to_string t
     end else s
 
 }

src/util/number.ml

@@ -156,9 +156,11 @@ let force_support support do_it v =
 let simplify_max_int = BigInt.of_string "2147483646"
 
 let remove_minus e =
-  if e.[0] = '-' then
-    (let e' = Strings.copy e in Strings.set e' 0 'm'; e')
-  else e
+  if e.[0] = '-' then begin
+    let e = Bytes.of_string e in
+    Bytes.set e 0 'm';
+    Bytes.unsafe_to_string e
+  end else e
 
 let print_dec_int support fmt i =
   let fallback i =

src/util/rc.mll

@@ -64,20 +64,20 @@ let escape_string s =
          | _ -> 1)
   done;
   if !n = String.length s then s else begin
-    let s' = Strings.create !n in
+    let s' = Bytes.create !n in
     n := 0;
     for i = 0 to String.length s - 1 do
       let c = String.unsafe_get s i in
       begin match c with
         | ('"' | '\\' | '\n' | '\r' | '\t') ->
-          Strings.set s' !n '\\'; incr n
+          Bytes.set s' !n '\\'; incr n
         | _ -> ()
       end;
-      Strings.set s' !n
+      Bytes.set s' !n
         (match c with '\n' -> 'n' | '\r' -> 'r' | '\t' -> 't' | _ -> c);
       incr n
     done;
-    s'
+    Bytes.unsafe_to_string s'
   end
 
 let print_rc_value fmt = function

src/util/strings.ml

@@ -9,11 +9,6 @@
 (*                                                                  *)
 (********************************************************************)
 
-
-let create = String.create
-let copy = String.copy
-let set = String.set
-
 let capitalize = String.capitalize
 let uncapitalize = String.uncapitalize
 
@@ -58,10 +53,10 @@ let ends_with s suf =
 let pad_right c s i =
   let sl = String.length s in
   if sl < i then
-    let p = create i in
-    String.blit s 0 p 0 sl;
-    String.fill p sl (i-sl) c;
-    p
+    let p = Bytes.create i in
+    Bytes.blit_string s 0 p 0 sl;
+    Bytes.fill p sl (i-sl) c;
+    Bytes.unsafe_to_string p
   else if sl > i
   then String.sub s 0 i
   else s

src/util/strings.mli

@@ -13,10 +13,6 @@
 
 (** {2 Wrappers for deprecated string functions of OCaml stdlib} *)
 
-val create : int -> string
-val copy : string -> string
-val set : string -> int -> char -> unit
-
 val capitalize : string -> string
 val uncapitalize : string -> string
 

src/util/sysutil.ml

@@ -17,22 +17,22 @@ let backup_file f =
   end
 
 let channel_contents_fmt cin fmt =
-  let buff = String.make 1024 ' ' in
+  let buff = Bytes.create 1024 in
   let n = ref 0 in
   while n := input cin buff 0 1024; !n <> 0 do
     Format.pp_print_string fmt
       (if !n = 1024 then
-         buff
+         Bytes.unsafe_to_string buff
        else
-         String.sub buff 0 !n)
+         Bytes.sub_string buff 0 !n)
   done
 
 let channel_contents_buf cin =
-  let buf = Buffer.create 1024
-  and buff = String.make 1024 ' ' in
+  let buf = Buffer.create 1024 in
+  let buff = Bytes.create 1024 in
   let n = ref 0 in
   while n := input cin buff 0 1024; !n <> 0 do
-    Buffer.add_substring buf buff 0 !n
+    Buffer.add_subbytes buf buff 0 !n
   done;
   buf
 
@@ -78,7 +78,7 @@ let open_temp_file ?(debug=false) filesuffix usefile =
 let copy_file from to_ =
   let cin = open_in from in
   let cout = open_out to_ in
-  let buff = String.make 1024 ' ' in
+  let buff = Bytes.create 1024 in
   let n = ref 0 in
   while n := input cin buff 0 1024; !n <> 0 do
     output cout buff 0 !n

src/why3session/why3session_lib.ml

@@ -249,7 +249,7 @@ let rec ask_yn () =
 
 let ask_yn_nonblock ~callback =
   let b = Buffer.create 3 in
-  let s = Strings.create 1 in
+  let s = Bytes.create 1 in
   Format.printf "(y/n)@.";
   fun () ->
     match Unix.select [Unix.stdin] [] [] 0. with
@@ -258,8 +258,9 @@ let ask_yn_nonblock ~callback =
       if Unix.read Unix.stdin s 1 0 = 0 then
         begin (* EndOfFile *) callback false; false end
       else begin
-        if s.[0] <> '\n'
-        then (Buffer.add_char b s.[0]; true)
+        let c = Bytes.get s 0 in
+        if c <> '\n'
+        then (Buffer.add_char b c; true)
         else
           match Buffer.contents b with
           | "y" -> callback true; false