fix(cfg-builder): caching of integers

This fixes issue #91

lib/Clam/CfgBuilderLit.cc

@@ -122,7 +122,14 @@ crab_lit_ref_t crabLitFactoryImpl::getLit(const Value &v, bool IntCstAsSigned) {
     if (lit.hasValue()) {
       crab_lit_ref_t ref = std::static_pointer_cast<crabLit>(
           std::make_shared<crabIntLit>(lit.getValue()));
-      m_lit_cache.insert({&v, ref});
+      if (IntCstAsSigned) {
+	// We only cache an integer constant if it is
+	// signed. Otherwise, we can get an inconsistent integer if we
+	// cached a signed one and then we ask for an unsigned (or
+	// vice-versa). A better solution is to have two caches one
+	// for signed and one for unsigned.
+	m_lit_cache.insert({&v, ref});
+      }
       return ref;
     }
   } else if (t.isPointerTy()) {

tests/simple/test-unsigned-cmp-5.c

@@ -0,0 +1,24 @@
+// RUN: %clam --crab-dom=int --crab-lower-unsigned-icmp --crab-check=assert %s 2>&1 | OutputCheck %s
+// RUN: %clam --crab-dom=int --lower-unsigned-icmp --crab-check=assert %s 2>&1 | OutputCheck %s
+// CHECK: ^1  Number of total safe checks$
+// CHECK: ^0  Number of total error checks$
+// CHECK: ^0  Number of total warning checks$
+
+
+extern void __CRAB_assume(int cond);
+extern int __CRAB_nd(void);
+extern void __CRAB_assert(int);
+
+int N;
+
+int main() {
+  N = __CRAB_nd();
+
+  __CRAB_assume(N != -2147483648 && N != 2147483647);
+
+  for (int i = 0; i < N; i++) {
+    __CRAB_assert(N >= -1);
+  }
+
+  return 0;
+}