Fix reading reals from strings in C lib

3 files changed, 6 insertions, 19 deletions

diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml
index 2e6e1e29..139763b1 100644
--- a/src/bytecode_util.ml
+++ b/src/bytecode_util.ml
@@ -135,14 +135,14 @@ let rec frag_rename from_id to_id = function
 (**************************************************************************)
 
 let string_of_value = function
-  | V_bits bs -> Sail2_values.show_bitlist bs ^ "ul"
+  | V_bits bs -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
   | V_int i -> Big_int.to_string i ^ "l"
   | V_bool true -> "true"
   | V_bool false -> "false"
   | V_null -> "NULL"
   | V_unit -> "UNIT"
-  | V_bit Sail2_values.B0 -> "0ul"
-  | V_bit Sail2_values.B1 -> "1ul"
+  | V_bit Sail2_values.B0 -> "UINT64_C(0)"
+  | V_bit Sail2_values.B1 -> "UINT64_C(1)"
   | V_string str -> "\"" ^ str ^ "\""
   | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str
   | _ -> failwith "Cannot convert value to string"
diff --git a/src/c_backend.ml b/src/c_backend.ml
index ef2d9a58..c2c1fd39 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -273,8 +273,8 @@ let mask m =
   if Big_int.less_equal m (Big_int.of_int 64) then
     let n = Big_int.to_int m in
     if n mod 4 == 0
-    then "0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ "ul"
-    else "0b" ^ String.make (64 - n) '0' ^ String.make n '1' ^ "ul"
+    then "UINT64_C(0x" ^ String.make (16 - n / 4) '0' ^ String.make (n / 4) 'F' ^ ")"
+    else "UINT64_C(" ^ String.make (64 - n) '0' ^ String.make n '1' ^ ")"
   else
     failwith "Tried to create a mask literal for a vector greater than 64 bits."
 
@@ -1872,7 +1872,7 @@ let sgen_cval_param (frag, ctyp) =
   | CT_bits direction ->
      string_of_fragment frag ^ ", " ^ string_of_bool direction
   | CT_bits64 (len, direction) ->
-     string_of_fragment frag ^ ", " ^ string_of_int len ^ "ul , " ^ string_of_bool direction
+     string_of_fragment frag ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction
   | _ ->
      string_of_fragment frag
 
diff --git a/src/value2.lem b/src/value2.lem
index d14dd87d..33416503 100644
--- a/src/value2.lem
+++ b/src/value2.lem
@@ -70,19 +70,6 @@ type vl =
   | V_record of list (string * vl)
   | V_null (* Used for unitialized values and null pointers in C compilation *)
 
-let string_of_value = function
-  | V_bits bs -> show_bitlist bs ^ "ul"
-  | V_int i -> show i ^ "l"
-  | V_bool true -> "true"
-  | V_bool false -> "false"
-  | V_null -> "NULL"
-  | V_unit -> "UNIT"
-  | V_bit B0 -> "0ul"
-  | V_bit B1 -> "1ul"
-  | V_string str -> "\"" ^ str ^ "\""
-  | _ -> failwith "Cannot convert value to string"
-end
-
 let primops extern args =
   match (extern, args) with
   | ("and_bool", [V_bool b1; V_bool b2]) -> V_bool (b1 && b2)