Undetected leaks in plain {m,c,re}allocs

[lzaoral]

Hi, Symbiotic does not detect any leaks in the following piece(s) of code. Thanks!

#include <stdlib.h>
int main(void)
{
    malloc(1); // same result with calloc(1, 1) or realloc(NULL, 1)
}

Output:

symbiotic --prp=memsafety malloc-leak-simple.c 
7.0.0-dev-llvm-9.0.1-symbiotic:d26ef236-dg:e89761ff-sbt-slicer:fff6245c-sbt-instrumentation:2f9be629-klee:59f3e288
INFO: Starting instrumentation
wrapper: `which slllvm` failed with error code 1

INFO: Instrumentation time: 0.05478835105895996
INFO: Optimizations time: 0.03318643569946289
INFO: Starting slicing
INFO: Total slicing time: 0.015712261199951172
INFO: Optimizations time: 0.025635957717895508
INFO: After-slicing optimizations and transformations time: 3.409385681152344e-05
INFO: Starting verification
INFO: Verification time: 0.04804825782775879
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.6929895877838135

EDIT: realloc(1, NULL) -> realloc(NULL, 1)

[mchalupa]

Hmm, yes, this problem is present when slicing is enabled, which points either to slicing or instrumentation. Checking the log shows:

Info:   0 of __INSTR_mark_allocation (blocked 1)
Info:   0 of __INSTR_mark_exit (blocked 1)

So the problem is that the instrumentation does not mark the malloc() as possibly leaked and it gets sliced away.

[mchalupa]

The problem here is that the result of malloc is not stored into a variable, therefore our check of possibly leaked memory (which searches the values stored into memory) does not see this call to malloc. For fixing this, we'll probably need to wait until https://github.com/mchalupa/dg/issues/249 is resolved.