search

esbmc / esbmc

The efficient SMT-based context-bounded model checker (ESBMC)
http://esbmc.org/
Other
297 stars 98 forks source link

incorrect true in the inductive step for linear search #306

Open lucasccordeiro opened 3 years ago

lucasccordeiro commented 3 years ago

./esbmc-wrapper.py -p ../../sv-benchmarks/c/properties/unreach-call.prp -s kinduction --arch 32 ../../sv-benchmarks/c/loops/linear_search.c

Verifying with ESBMC Command: ./esbmc --no-div-by-zero-check --force-malloc-success --state-hashing --no-align-check --k-step 2 --floatbv --unlimited-k-steps --no-por --context-bound-step 5 --max-context-bound 15 --incremental-cb ../../sv-benchmarks/c/loops/linear_search.c --32 --witness-output linear_search.c.graphml --k-induction --max-inductive-step 3 --no-pointer-check --no-bounds-check --interval-analysis ESBMC version 6.4.0 64-bit x86_64 linux file ../../sv-benchmarks/c/loops/linear_search.c: Parsing Converting Generating GOTO Program GOTO program creation time: 0.061s GOTO program processing time: 0.000s

Iteration number 1 *** Checking base case

Context bound number 2 Starting Bounded Model Checking Not unwinding loop 1 iteration 1 file linear_search.c line 17 function linear_search Symex completed in: 0.037s (45 assignments) Slicing time: 0.000s (removed 29 assignments) Generated 1 VCC(s), 1 remaining after simplification (16 assignments) Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.000s Solving with solver Boolector 3.2.0 Encoding to solver time: 0.000s Runtime decision procedure: 0.000s BMC program time: 0.037s No bug has been found in the base case

Context bound number 7 Starting Bounded Model Checking Thread interleavings 2 Not unwinding loop 1 iteration 1 file linear_search.c line 17 function linear_search Symex completed in: 0.002s (45 assignments) Slicing time: 0.000s (removed 29 assignments) Generated 1 VCC(s), 1 remaining after simplification (16 assignments) Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.000s Solving with solver Boolector 3.2.0 Encoding to solver time: 0.000s Runtime decision procedure: 0.000s BMC program time: 0.002s No bug has been found in the base case

Context bound number 12 Starting Bounded Model Checking Thread interleavings 3 Not unwinding loop 1 iteration 1 file linear_search.c line 17 function linear_search Symex completed in: 0.001s (45 assignments) Slicing time: 0.000s (removed 29 assignments) Generated 1 VCC(s), 1 remaining after simplification (16 assignments) Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.000s Solving with solver Boolector 3.2.0 Encoding to solver time: 0.000s Runtime decision procedure: 0.000s BMC program time: 0.002s No bug has been found in the base case *** Checking forward condition Starting Bounded Model Checking Not unwinding loop 1 iteration 1 file linear_search.c line 17 function linear_search Symex completed in: 0.001s (44 assignments) Slicing time: 0.000s (removed 29 assignments) Generated 1 VCC(s), 1 remaining after simplification (15 assignments) Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.000s Solving with solver Boolector 3.2.0 Encoding to solver time: 0.000s Runtime decision procedure: 0.003s The forward condition is unable to prove the property

Iteration number 3 *** Checking base case

Context bound number 2 Starting Bounded Model Checking Unwinding loop 1 iteration 1 file linear_search.c line 17 function linear_search Unwinding loop 1 iteration 2 file linear_search.c line 17 function linear_search Not unwinding loop 1 iteration 3 file linear_search.c line 17 function linear_search Symex completed in: 0.002s (51 assignments) Slicing time: 0.000s (removed 31 assignments) Generated 1 VCC(s), 1 remaining after simplification (20 assignments) Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.001s Solving with solver Boolector 3.2.0 Encoding to solver time: 0.001s Runtime decision procedure: 0.003s BMC program time: 0.006s No bug has been found in the base case

Context bound number 7 Starting Bounded Model Checking Thread interleavings 2 Unwinding loop 1 iteration 1 file linear_search.c line 17 function linear_search Unwinding loop 1 iteration 2 file linear_search.c line 17 function linear_search Not unwinding loop 1 iteration 3 file linear_search.c line 17 function linear_search Symex completed in: 0.001s (51 assignments) Slicing time: 0.000s (removed 31 assignments) Generated 1 VCC(s), 1 remaining after simplification (20 assignments) Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.000s Solving with solver Boolector 3.2.0 Encoding to solver time: 0.000s Runtime decision procedure: 0.004s BMC program time: 0.006s No bug has been found in the base case

Context bound number 12 Starting Bounded Model Checking Thread interleavings 3 Unwinding loop 1 iteration 1 file linear_search.c line 17 function linear_search Unwinding loop 1 iteration 2 file linear_search.c line 17 function linear_search Not unwinding loop 1 iteration 3 file linear_search.c line 17 function linear_search Symex completed in: 0.001s (51 assignments) Slicing time: 0.000s (removed 31 assignments) Generated 1 VCC(s), 1 remaining after simplification (20 assignments) Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.000s Solving with solver Boolector 3.2.0 Encoding to solver time: 0.000s Runtime decision procedure: 0.004s BMC program time: 0.006s No bug has been found in the base case Checking forward condition Starting Bounded Model Checking Unwinding loop 1 iteration 1 file linear_search.c line 17 function linear_search Unwinding loop 1 iteration 2 file linear_search.c line 17 function linear_search Not unwinding loop 1 iteration 3 file linear_search.c line 17 function linear_search Symex completed in: 0.002s (50 assignments) Slicing time: 0.000s (removed 31 assignments) Generated 1 VCC(s), 1 remaining after simplification (19 assignments) Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.000s Solving with solver Boolector 3.2.0 Encoding to solver time: 0.000s Runtime decision procedure: 0.007s The forward condition is unable to prove the property Checking inductive step Starting Bounded Model Checking Unwinding loop 1 iteration 1 file linear_search.c line 17 function linear_search Unwinding loop 1 iteration 2 file linear_search.c line 17 function linear_search Not unwinding loop 1 iteration 3 file linear_search.c line 17 function linear_search Symex completed in: 0.002s (77 assignments) Slicing time: 0.000s (removed 30 assignments) Generated 1 VCC(s), 1 remaining after simplification (47 assignments) Encoding remaining VCC(s) using bit-vector/floating-point arithmetic Encoding to solver time: 0.000s Solving with solver Boolector 3.2.0 Encoding to solver time: 0.000s Runtime decision procedure: 0.003s BMC program time: 0.006s Building successful trace

VERIFICATION SUCCESSFUL

Solution found by the inductive step (k = 3)

github-actions[bot] commented 3 years ago

Stale issue message

lucasccordeiro commented 3 years ago

ESBMC produces incorrect TRUE here because of the option --interval-analysis. If we remove this option from our SV-COMP script, then the k-induction proof rule corrects checks this program.