diff --git a/lib/Clam/CfgBuilderLit.cc b/lib/Clam/CfgBuilderLit.cc index d1d1e677..351203d4 100644 --- a/lib/Clam/CfgBuilderLit.cc +++ b/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( std::make_shared(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()) { diff --git a/tests/simple/test-unsigned-cmp-5.c b/tests/simple/test-unsigned-cmp-5.c new file mode 100644 index 00000000..5d5dc243 --- /dev/null +++ b/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; +}