Camlcoq.ml: interpret Caml's int32 as unsigned when converting to Integers.int

Cil2Csyntax.ml: terminating NUL character in strings within initialized data


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 8 insertions, 5 deletions

diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml
index d60e0222..e9089cf3 100644
--- a/caml/Camlcoq.ml
+++ b/caml/Camlcoq.ml
@@ -51,7 +51,9 @@ let z_of_camlint n =
   if n > 0l then Zpos (positive_of_camlint n)
   else Zneg (positive_of_camlint (Int32.neg n))
 
-let coqint_of_camlint : int32 -> Integers.int = z_of_camlint
+let coqint_of_camlint (n: int32) : Integers.int = 
+  (* Interpret n as unsigned so that resulting Z is in range *)
+  if n = 0l then Z0 else Zpos (positive_of_camlint n)
 
 (* Atoms (positive integers representing strings) *)
 
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index 554715fc..17bcb262 100644
--- a/caml/Cil2Csyntax.ml
+++ b/caml/Cil2Csyntax.ml
@@ -806,10 +806,11 @@ let rec extract_constant e =
 
 let init_data_of_string s =
   let id = ref CList.Coq_nil in
-  for i = String.length s - 1 downto 0 do
-    let n = coqint_of_camlint(Int32.of_int(Char.code s.[i])) in
-    id := CList.Coq_cons(Init_int8 n, !id)
-  done;
+  let enter_char c =
+    let n = coqint_of_camlint(Int32.of_int(Char.code c)) in
+    id := CList.Coq_cons(Init_int8 n, !id) in
+  enter_char '\000';
+  for i = String.length s - 1 downto 0 do enter_char s.[i] done;
   !id
 
 let convertInit init =