Marek Chalupa

> I cannot understand the original witness that was posted here. It seems to end at the statement tmp___0 == 2 which is clearly not related to an invalid memory...

To me, the benchmark looks like assuming that the values of the array `v` are non-deterministic rather than 0 (which would happen if the declaration would be moved outside the...

Exactly the same issues (and some more), can be found in these benchmarks: * https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ntdrivers/diskperf_true-unreach-call_true-valid-memsafety.i.cil.c * https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ntdrivers/floppy2_true-unreach-call_true-valid-memsafety.i.cil.c * https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ntdrivers/parport_false-unreach-call_true-valid-memsafety.i.cil.c. I tried to fix them, but I haven't succeeded. And I'm...

> @mchalupa is there any way to convince the slicer to preserve the llvm.dbg.* instructions? Not a one that is implemented, but there is a way: we may set `llvm.dbg.*`...

or use KLEE's posix staff

Check e.g., https://github.com/klee/klee-uclibc (you can always compile the C code to LLVM).

@tareq97 Sure, any PRs are welcome ;) The `archive` option creates a .zip file with compiled Symbiotic using `git archive` command on the contents of `install` folder (which is under...

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

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

There's probably nothing we can do about it. Clang drops the dereference during the compilation and the empty program is generated. ``` warning: expression result unused [-Wunused-value] int main(void) {...