search

smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
432 stars 82 forks source link

All programs verify when SMT solver (Z3) is not present #796

Open rakamaric opened 1 year ago

rakamaric commented 1 year ago

Currently all programs vacuously verify when an SMT solver is not present/installed. Here is the example output when running Corral:

Running corral /local/home/zvorak/smack/src/test/c/basic/a-kem0fn3_.bpl /tryCTrace /noTraceOnDisk /printDataValues:1 /k:1 /useProverEvaluate /timeLimit:1200 /cex:1 /maxStaticLoopBound:1 /recursionBound:1 /bopt:proverOpt:O:smt.qi.eager_threshold=100 /bopt:proverOpt:O:smt.arith.solver=2
Corral program verifier version 1.1.8.0
Single threaded program detected
LB: Took 0.00 s
Verifying program while tracking: {assertsPassed}
Error: ProverException: Cannot find any prover executable
Program has no bugs

Boogie verification time: 0.00 s
Time spent reading-writing programs: 0.35 s

Time spent checking a program (1): 0.14 s
Time spent checking a path (0): 0.00 s

Number of procedures inlined: 0
Number of variables tracked: 1
Total Time: 0.9166774 s
Total User CPU time: 1.05 s
SMACK found no errors with unroll bound 1.

We should address this and report an error instead.

rakamaric commented 1 year ago

I would say that this issue is in fact in Corral. Corral reports "Program has no bugs" even when this ProverException is generated. So it should probably be first fixed on the Corral side.