Smoke tests try to find unreachable code. They are useful for detecting inconsistencies in your specifications, especially early in the verification/development cycle.
Smoke tests work by trying to prove program control points unreachable; the test succeeds if the proof fails or hits a (relatively short) timeout. Because this reasoning is incomplete, smoke tests do not come with any soundness guarantee, and should by used
purely as a debugging/QC tool.
Running smoke tests
To activate the smoke test, add /smoke
to the VCC command line.
Defusing smoke tests
In cases where unreachable code exists purposefully, the smoke test can be defused by placing
at the beginning of the unreachable block. Also, VCC compiles the lazy operators "&&
", and "?
" into conditional blocks. If some of these blocks are unreachable, e.g., because the first argument of an
-expression is always false, this will also trigger smoke test errors. These errors can be defused by annotating the operation using the
int bar(int i);
void foo(int i, int j)
int x = i || bar(j); // smoke test error here
int y = known(i, true) || bar(j); // defused smoke test error