bfd7fd56a1
Add the -safe-string patch for building with ocaml 4.06.0. Build the Jessie plugin with -runtime-variant _pic.
67 lines
2.2 KiB
Diff
67 lines
2.2 KiB
Diff
--- jc/jc_annot_inference.ml.orig 2017-08-23 02:08:38.000000000 -0600
|
|
+++ jc/jc_annot_inference.ml 2017-12-05 21:03:16.549749880 -0700
|
|
@@ -212,14 +212,14 @@ let name_of_term t =
|
|
Format.fprintf str_formatter "%a" Jc_output.term t;
|
|
let s = Format.flush_str_formatter () in
|
|
let s = filter_alphanumeric s in
|
|
- "T" ^ unique_term_name t s
|
|
+ "T" ^ unique_term_name t (Bytes.to_string s)
|
|
|
|
let name_of_assertion a =
|
|
ignore (Format.flush_str_formatter ());
|
|
Format.fprintf str_formatter "%a" Jc_output.assertion a;
|
|
let s = Format.flush_str_formatter () in
|
|
let s = filter_alphanumeric s in
|
|
- "A" ^ unique_assertion_name a s
|
|
+ "A" ^ unique_assertion_name a (Bytes.to_string s)
|
|
|
|
(* support of <new> (Nicolas) *)
|
|
let rec destruct_alloc t =
|
|
--- jc/jc_region.ml.orig 2017-08-23 02:08:38.000000000 -0600
|
|
+++ jc/jc_region.ml 2017-12-05 21:01:36.269076188 -0700
|
|
@@ -244,8 +244,8 @@ struct
|
|
jc_reg_variable = false;
|
|
jc_reg_bitwise = false;
|
|
jc_reg_id = id;
|
|
- jc_reg_name = name;
|
|
- jc_reg_final_name = name ^ "_" ^ (string_of_int id);
|
|
+ jc_reg_name = (Bytes.to_string name);
|
|
+ jc_reg_final_name = (Bytes.to_string name) ^ "_" ^ (string_of_int id);
|
|
jc_reg_type = ty;
|
|
}
|
|
|
|
@@ -258,8 +258,8 @@ struct
|
|
jc_reg_variable = true;
|
|
jc_reg_bitwise = false;
|
|
jc_reg_id = id;
|
|
- jc_reg_name = name;
|
|
- jc_reg_final_name = name ^ "_" ^ (string_of_int id);
|
|
+ jc_reg_name = (Bytes.to_string name);
|
|
+ jc_reg_final_name = (Bytes.to_string name) ^ "_" ^ (string_of_int id);
|
|
jc_reg_type = ty;
|
|
}
|
|
|
|
--- src/lib.ml.orig 2017-08-23 02:08:38.000000000 -0600
|
|
+++ src/lib.ml 2017-12-05 20:43:07.384255238 -0700
|
|
@@ -54,7 +54,7 @@ let file_subdir ~dir ~file =
|
|
let file_copy src dest =
|
|
let cin = open_in src
|
|
and cout = open_out dest
|
|
- and buff = String.make 1024 ' '
|
|
+ and buff = Bytes.make 1024 ' '
|
|
and n = ref 0
|
|
in
|
|
while n := input cin buff 0 1024; !n <> 0 do
|
|
@@ -68,10 +68,10 @@ let file_copy_if_different src dst =
|
|
|
|
let channel_contents_buf cin =
|
|
let buf = Buffer.create 1024
|
|
- and buff = String.make 1024 ' ' in
|
|
+ and buff = Bytes.make 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
|
|
|