*NULL undetected

[lzaoral]

Hi, Symbiotic fails to find a property violation in the following piece of code:

#include <stddef.h>
int main(void) { *NULL; }

Output:

$ symbiotic --prp=memsafety null.c
7.0.0-dev-llvm-9.0.1-symbiotic:03f217bf-dg:e89761ff-sbt-slicer:fff6245c-sbt-instrumentation:34bbe496-klee:e773a1f8
INFO: Starting instrumentation
wrapper: `which slllvm` failed with error code 1

INFO: Instrumentation time: 0.051297664642333984
INFO: Optimizations time: 0.036144256591796875
INFO: Starting slicing
INFO: Total slicing time: 0.01163029670715332
INFO: Optimizations time: 0.030501365661621094
INFO: After-slicing optimizations and transformations time: 2.3603439331054688e-05
INFO: Starting verification
INFO: Verification time: 0.04517221450805664
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.548166036605835

[mchalupa]

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) { *NULL; }

Although there are some switches that can disable LLVM optimizations, I am not aware of any switches that could force clang emitting this expression.

[lzaoral]

As long as clang emits the mentioned warning it's not a big problem. Anyway, thanks for the swift reply!