No violation node for some benchmarks in the memory safety category

[lucasccordeiro]

Here is the fix related to the violation node for the memory safety benchmarks: https://github.com/marek-trtik/cbmc/commit/aa1aaf687f5286a04bd0ab09bcd6b0b9780b9ba0

[lucasccordeiro]

./test-gen.sh --graphml-witness witness.graphml -m32 --propertyfile ~/sv-benchmarks/c/MemSafety.prp ~/sv-benchmarks/c/heap-manipulation/tree_false-unreach-call_false-valid-deref.i

tree_false-unreach-call_false-valid-deref.i: OK FALSE(valid-deref)

[lucasccordeiro]

I have tried to remove as much information as I could from the witnesses, but they do not get confirmed by the witness checkers (CPAchecker and FShell).

Find attached one example of simplified witness. I have no further idea of simplifications for this witness.

Here is the command line to produce the witness in CBMC:

./cbmc-wrapper --graphml-witness witness.graphml --32 --propertyfile ../sv-benchmarks/c/MemSafety.prp ../sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i

Here is the command-line to check with FShell:

./test-gen.sh --graphml-witness ~/cprover-sv-comp/witness.graphml -m32 --propertyfile ~/sv-benchmarks/c/MemSafety.prp  ~/sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i

Here is the command-line with CPAchecker:

scripts/cpa.sh -secureMode -timelimit 90s -heap 12000M -setprop witness.checkProgramHash=false -witnessValidation -setprop analysis.machineModel=Linux32 -spec specification0.prp -witness ~/cprover-sv-comp/witness.graphml ~/sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i

witness.graphml.zip

[lucasccordeiro]

For this witness:

./cbmc-wrapper --graphml-witness witness.graphml --32 --propertyfile ../sv-benchmarks/c/MemSafety.prp ../sv-benchmarks/c/memsafety/20020406-1_false-valid-memtrack.i

FShell returns:

Undefined symbols for architecture i386:
  "___orig__main", referenced from:
      _main in tester-c0305b.o
ld: symbol(s) not found for architecture i386
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [tester] Error 1
20020406-1_false-valid-memtrack.i: ERROR - failing memory safety violation not found
UNKNOWN

CPAchecker returns:

Error: line 1003: Unsupported feature (recursion): __CPAchecker_TMP_2 = DUPFFexgcd(gcofac, fcofac, g, f); (line was originally return DUPFFexgcd(gcofac, fcofac, g, f);) (CallstackTransferRelation.getAbstractSuccessorsForEdge, SEVERE)

Verification result: UNKNOWN, incomplete analysis.
More details about the verification run can be found in the directory "./output".
Graphical representation included in the file "./output/Report.html".