Benchmark: ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i

[marek-trtik]

Current false(valid-deref); last year true; should be true.

[marek-trtik]

Log from last year:

./cbmc --graphml-witness witness.graphml --32 --propertyfile ../../sv-benchmarks/c/MemSafety.prp ../../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i

--------------------------------------------------------------------------------

Unwind: 2
CBMC version 5.6 64-bit x86_64 linux
Parsing ../../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i
Converting
Type-checking test-bitfields-1_true-valid-memsafety
Generating GOTO Program
Adding CPROVER library (x86_64)
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 198 steps
simple slicing removed 1 assignments
Generated 68 VCC(s), 19 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with Glucose Syrup with simplifier
777 variables, 449 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 0.001s
VERIFICATION SUCCESSFUL
EC=0
TRUE

[marek-trtik]

Log from this year:

./xtest --graphml-witness witness.graphml --32 --propertyfile ../sv-benchmarks/c/MemSafety.prp ../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i

--------------------------------------------------------------------------------

./xtest-binary --graphml-witness /tmp/BenchExec_run_6a0rm5by/tmp/xtest-log.lSMqzi.witness --unwind 2 --stop-on-fail --32 --pointer-check --memory-leak-check --bounds-check --no-assertions --function main ../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i
Unwind: 2
CBMC version 5.8 64-bit x86_64 linux
Parsing ../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i
Converting
Type-checking test-bitfields-1_true-valid-memsafety
Generating GOTO Program
Adding CPROVER library (x86_64)
file <command-line> line 0: <command-line>:0:0: warning: "__STDC_VERSION__" redefined
<built-in>: note: this is the location of the previous definition
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
size of program expression: 208 steps
simple slicing removed 1 assignments
Generated 68 VCC(s), 19 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with Glucose Syrup with simplifier
307 variables, 210 clauses
SAT checker: instance is SATISFIABLE
Runtime decision procedure: 0s
Building error trace
Counterexample:

State 18 file ../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i line 22 function main thread 0
----------------------------------------------------
  p=((struct A *)NULL) (00000000000000000000000000000000)

State 22 file ../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i line 23 function main thread 0
----------------------------------------------------
  malloc_size=2u (00000000000000000000000000000010)

State 40 file ../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i line 23 function main thread 0
----------------------------------------------------
  p=dynamic_object1 (00000010000000000000000000000000)

State 42 file ../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i line 24 function main thread 0
----------------------------------------------------
  dynamic_object1={ 1, 0 } ({ 00000001, 00000000 })

State 47 file ../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i line 28 function main thread 0
----------------------------------------------------
  dynamic_object1={ 1, 2 } ({ 00000001, 00000010 })

Violated property:
  file ../sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i line 32 function main
  dereference failure: pointer outside dynamic object bounds in *p
  !(POINTER_OBJECT(p) == POINTER_OBJECT(__CPROVER_malloc_object)) || POINTER_OFFSET(p) + 2 >= 0 && __CPROVER_malloc_size >= (unsigned int)POINTER_OFFSET(p) + 3u

VERIFICATION FAILED
EC=10
FALSE(valid-deref)

[marek-trtik]

The cause is here: https://github.com/marek-trtik/cbmc/blob/sv-comp-2018-patches/src/analyses/goto_check.cpp#L1071

[marek-trtik]

I made another duplicate issue. This time of #2.