Fix unsoundness with large 64bit unsigned constant (closes #120)

sim642 · sim642 · commit 7d0fbeefba2c · 2020-10-22T10:13:51.000+03:00
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -612,7 +612,7 @@ struct
         | Const (CChr x) -> eval_rv a gs st (Const (charConstToInt x)) (* char becomes int, see Cil doc/ISO C 6.4.4.4.10 *)
         | Const (CInt64 (num,typ,str)) ->
           (match str with Some x -> M.tracel "casto" "CInt64 (%s, %a, %s)\n" (Int64.to_string num) d_ikind typ x | None -> ());
-          `Int (ID.of_int num)
+          `Int (ID.cast_to typ (ID.of_int num))
         (* String literals *)
         | Const (CStr x) -> `Address (AD.from_string x) (* normal 8-bit strings, type: char* *)
         | Const (CWStr xs as c) -> (* wide character strings, type: wchar_t* *)
diff --git a/tests/regression/29-svcomp/04-lustre-minimal.c b/tests/regression/29-svcomp/04-lustre-minimal.c
@@ -0,0 +1,11 @@
+// PARAM: --enable ana.int.interval --enable ana.int.def_exc
+// issue #120
+#include <assert.h>
+
+int main() {
+    // should be LP64
+    unsigned long n = 16;
+    unsigned long size = 4912;
+
+    assert(!(0xffffffffffffffffUL / size < n)); // UNKNOWN (for now)
+}
