From 806e97ffbc0193a3539d5c0dc8902465d71fe0bd Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 14 May 2020 10:54:16 +0100
Subject: Output INT64_MIN in code generator for min 64-bit integer literal

Fixes the warning generated because in C -X where X is the minimum integer is
parsed as a positive integer which is then negated. This causes a (I
believe spurious) warning that the integer literal is too large for the type.

Also using INT64_C so we get either long or long long depending on
platform
---
 src/jib/c_backend.ml | 6 +++++-
 src/jib/c_codegen.ml | 6 +++++-
 2 files changed, 10 insertions(+), 2 deletions(-)

(limited to 'src/jib')

diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index c38749f3..5947b500 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -1212,7 +1212,11 @@ let rec sgen_value = function
   | VL_bits ([], _) -> "UINT64_C(0)"
   | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
   | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")"
-  | VL_int i -> Big_int.to_string i ^ "l"
+  | VL_int i ->
+     if Big_int.equal i (min_int 64) then
+       "INT64_MIN"
+     else
+       "INT64_C(" ^ Big_int.to_string i ^ ")"
   | VL_bool true -> "true"
   | VL_bool false -> "false"
   | VL_unit -> "UNIT"
diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml
index 80d4e847..05abfe70 100644
--- a/src/jib/c_codegen.ml
+++ b/src/jib/c_codegen.ml
@@ -322,7 +322,11 @@ let rec sgen_value = function
   | VL_bits ([], _) -> "UINT64_C(0)"
   | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
   | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")"
-  | VL_int i -> Big_int.to_string i ^ "l"
+  | VL_int i ->
+     if Big_int.equal i (min_int 64) then
+       "INT64_MIN"
+     else
+       "INT64_C(" ^ Big_int.to_string i ^ ")"
   | VL_bool true -> "true"
   | VL_bool false -> "false"
   | VL_unit -> "UNIT"
-- 
cgit v1.2.3