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 assert(false) 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 known(...) macro.

For example:

#include <vcc.h>

int bar(int i);

void foo(int i, int j)
  _(requires i)
  int x = i || bar(j);              // smoke test error here
  int y = known(i, true) || bar(j); // defused smoke test error

Last edited May 2, 2012 at 7:44 PM by erniecohen, version 6


holgerblasum Mar 11, 2011 at 1:59 PM 
On the scope of smoke tests and controlling it with /b:/smokeTimeout see discussion