Dead code detection with "vcc /smoke" check: scope

Mar 11, 2011 at 1:17 PM
Edited Mar 11, 2011 at 1:33 PM

Hello,

on http://vcc.codeplex.com/wikipage?title=Smoke%20Tests it says "VCC can be run in a mode where it detects unreachable code." In verification practice this feature has been very useful in the past ... Now I have been asked whether vcc is designed to detect "all unreachable" or "some unreachable" code? The question was asked purely from a design point of view (intent), not (as some sort of guarantee) whether the current implementation is bug-free. Something that VCC obviously does not complain about is "implementation-non-reachable code" such as

void test_dead(unsigned int a) /*dead code: "vcc /smoke" does not trigger*/
{
    if (0) {a = 1;}
}

 

But still this does not rule out that VCC is designed to soundly detect (except, of course, when reaching a timeout) the more interesting set of "all specification-non-reachable" code such as

 

void test(unsigned int a) /*dead code: "vcc /smoke" triggers*/
requires(a == 0)
{
    if (a) {a = 1;}
}

Of course above snippet is just one example and not a general statement whether VCC's smoke check intends to detect
all specificiation non-reachable code. Best, Holger
Coordinator
Mar 11, 2011 at 1:59 PM

Hi Holger,

  the intent is only to _try_ to detect unreachable code, I've updated the Wiki page to reflect that. By (Boogie) default, VCC only tries for 10s per location in question; /b:/smokeTimeout:<n> can be used to change that (see "boogie /help"). In the case you show, the unreachable code is however pruned by VCC purely on a syntactical basis before this analysis even starts in one of its processing stages (you can see the if statement go away in the output of "vcc /pipe:dump-all"). (Side note: one level down, Boogie does the same, no smoke is detected for "procedure a(); implementation a() { var b: bool; if (false) { } else { } }").

  Best, Mark

Mar 11, 2011 at 2:59 PM

Hi Mark, thanks. (I've added a link in the wikipage comments section backpointing to this discussion.)

Coordinator
Mar 11, 2011 at 6:31 PM

Just in case: the primary reason for the /smoke option is to look for inconsistent axioms and specifications. It’s called unreachable code, because this is how it appears to the theorem prover. The fact that we detect regular unreachable code in the implementation is just a side effect, which is why we remove some “harmless” unreachable code syntactically.

Michal