From 3a34c43569ae9fdd3b170f26cba628d3aae5e336 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 16 Apr 2008 14:03:47 +0000
Subject: 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
---
 caml/Camlcoq.ml     | 4 +++-
 caml/Cil2Csyntax.ml | 9 +++++----
 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 =
-- 
cgit