Consecutive malloc allocations are not modelled correctly

[lzaoral]

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.3934328556060791

My machine:

$ cc symbiotic-mallocs.c && ./a.out
a.out: symbiotic-mallocs.c:17: main: Assertion `b != c' failed.

[kdudka]

Note that this example is very similar to issue #89.

[mchalupa]

It works without slicing, so the problem may be in the data dependence analysis.

[mchalupa]

Yep, the problem is that the slicer removes the call to free as it does not consider such a case witch comparing pointers could happen.