Consecutive malloc allocations are not modelled correctly #204
Description
The following piece of code contains an error but Symbiotic does not see it:
#include <assert.h> #include <stdlib.h> int main(void) { void* a = malloc(sizeof(int)); void* b = malloc(sizeof(int)); if (a != NULL && b != NULL) assert(a != b); free(b); void* c = malloc(sizeof(int)); if (a != NULL && c != NULL) assert(a != c); assert(b != c); /* can fail */ }Output:
$ symbiotic symbiotic-mallocs.c 8.0.0-pre-llvm-12.0.1-symbiotic:13ca9347-dg:0b1ada38-sbt-slicer:b0864a5b-sbt-instrumentation:648fabcc-klee:6ecf91e2 INFO: Looking for reachability of calls to __assert_fail,__VERIFIER_error INFO: Optimizations time: 0.01961374282836914 INFO: Starting slicing INFO: Total slicing time: 0.02277660369873047 INFO: Optimizations time: 0.020235300064086914 INFO: After-slicing optimizations and transformations time: 2.1457672119140625e-05 INFO: Starting verification KLEE: WARNING: undefined reference to function: klee_make_nondet KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8. No error found. NOTE: In the future, the result is going to be reported in SV-COMP format only with --report=sv-comp switch RESULT: true INFO: Total time elapsed: 0.3934328556060791My machine:
$ cc symbiotic-mallocs.c && ./a.out a.out: symbiotic-mallocs.c:17: main: Assertion `b != c' failed.