Merge pull request #782 from goblint/issue_769

Remove erroneous call to `truncateCilint` in `min_for`

Author: michael-schwarz

src/cdomains/intDomain.ml

@@ -393,11 +393,8 @@ module Size = struct (* size in bits as int, range as int64 *)
   open Cil open Big_int_Z
   let sign x = if BI.compare x BI.zero < 0 then `Signed else `Unsigned
 
-  let max = function
-    | `Signed -> ILongLong
-    | `Unsigned -> IULongLong
   let top_typ = TInt (ILongLong, [])
-  let min_for x = intKindForValue (fst (truncateCilint (max (sign x)) x)) (sign x = `Unsigned)
+  let min_for x = intKindForValue x (sign x = `Unsigned)
   let bit = function (* bits needed for representation *)
     | IBool -> 1
     | ik -> bytesSizeOfInt ik * 8

tests/regression/38-int-refinements/02-strange-ulong.c

@@ -0,0 +1,88 @@
+// PARAM: --enable ana.int.interval --set ana.int.refinement once
+#include <assert.h>
+
+int main();
+
+int withint() {
+  int i = 0;
+  void* bla;
+
+  while(i < 10000) {
+    i++;
+    bla = &main;
+  }
+
+  assert(1); // reachable
+  return 0;
+}
+
+int withuint() {
+  unsigned int i = 0;
+  void* bla;
+
+  while(i < 10000) {
+    i++;
+    bla = &main;
+  }
+
+  assert(1); // reachable
+  return 0;
+}
+
+int withlong() {
+  long i = 0;
+  void* bla;
+
+  while(i < 10000) {
+    i++;
+    bla = &main;
+  }
+
+  assert(1); // reachable
+  return 0;
+}
+
+int withlonglong() {
+  long long i = 0;
+  void* bla;
+
+  while(i < 10000) {
+    i++;
+    bla = &main;
+  }
+
+  assert(1); // reachable
+  return 0;
+}
+
+int withulonglong() {
+  unsigned long long i = 0;
+  void* bla;
+
+  while(i < 10000) {
+    i++;
+    bla = &main;
+  }
+
+  assert(1); // reachable
+  return 0;
+}
+
+int main() {
+  withint();
+  withuint();
+  withlong();
+  withlonglong();
+  withulonglong();
+
+  unsigned long i = 0;
+  void* bla;
+
+  while(i < 10000) {
+    i++;
+    bla = &main;
+  }
+
+  assert(1); // reachable
+  return 0;
+}