Invalid out of bound pointer error

[lzaoral]

Hi,
the following code is now in the latest commits mistakenly classified to contain an "out of bound pointer" error on line 12. This happens with following build of Symbiotic: https://copr.fedorainfracloud.org/coprs/acalabek/symbiotic/build/1129971/

Thanks!

#include <stdlib.h>

typedef void *TItem;

int main() {
    TItem *list = malloc(sizeof(TItem));
    *list = malloc(sizeof(TItem));
    *((TItem *) *list) = NULL;

    while (list) {
        TItem *item = list;
        list = (TItem *) *list;
        free(item);
    }

    return 0;
}

EDIT: The link now points to a specific build and not to the general repository.

[lzaoral]

I have tried the given code with latest symbiotic, but the issue still persists.

$ symbiotic --prp=memsafety test-0005.c
7.0.0-dev-llvm-10.0.0-symbiotic:630bd299-dg:8fd21926-sbt-slicer:ce747eca-sbt-instrumentation:ff
5d8b3f-klee:63cf2760
INFO: Looking for invalid dereferences, invalid free, memory leaks, etc.
INFO: Starting instrumentation
wrapper: `which slllvm` failed with error code 1

INFO: Instrumentation time: 0.050269126892089844
INFO: Optimizations time: 0.022818326950073242
INFO: Starting slicing
INFO: Total slicing time: 0.008790254592895508
INFO: Optimizations time: 0.020711898803710938
INFO: After-slicing optimizations and transformations time: 2.4080276489257812e-05
INFO: Starting verification
b'KLEE: WARNING: undefined reference to function: __symbiotic_keep_ptr'
b'KLEE: WARNING: undefined reference to function: klee_make_nondet'
b'KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment o
f 8.'
b'KLEE: ERROR: /home/lukas/aufover-benchmark/tests/single-c/predator/predator-regre-test-0005/t
est-0005.c:12: memory error: out of bound pointer'
b'KLEE: NOTE: now ignoring this error at this location'
INFO: Verification time: 0.03504681587219238

 --- Error trace ---

Error: memory error: out of bound pointer
File: /home/lukas/aufover-benchmark/tests/single-c/predator/predator-regre-test-0005/test-0005.
c
Line: 12
assembly.ll line: 43
Stack:
        #000000043 in main () at /home/lukas/aufover-benchmark/tests/single-c/predator/predator
-regre-test-0005/test-0005.c:12
Info:
        address: 0:12370169555311111083
        pointing to: none

 --- Sequence of non-deterministic values [function:file:line:col] ---


 --- ----------- ---
Error found.
NOTE: In the future, the result is going to be reported in SV-COMP format only with --report=sv
-comp switch
RESULT: false(valid-deref)
INFO: Total time elapsed: 0.42362046241760254

[mchalupa]

The answer is fine when --no-slice is used, which points to a bug in slicer or instrumentation.