Can I make a not-always-satisfied assert fail immediately?

Nov 9, 2009 at 9:43 AM

Hello list,

The default behavior of assert is:

#include "vcc.h"
void test(unsigned int i) {
        assert( i == 0 );
        assert( i == 1 );
}

$ vcc /v assert.c

Verification of test failed.
p:\tool\vcc\sandbox\assert.c(3,12) : error VC9500: Assertion 'i == 0' did not verify.
p:\tool\vcc\sandbox\assert.c(4,12) : error VC9500: Assertion 'i == 1' did not verify.
Exiting with 3 (1 error(s).)

Now I would prefer VCC to stop after it cannot assert the first assertion (in line 3) instead of trying out the assertion at line 4. The motivation is that in non-trivial examples I don't have to wait long to see whether the whole function verifies or not once I have seen an assert fail. I am aware of enforcing the desired behavior by inserting an "assert(false)" (non-satisfiable asserts trigger immediate stop) but then one has to remember to insert that. So is there a switch of setting for forcing an immediate stop not only after non-satisfiable asserts (false) but also after not-always-satisfied asserts (like, in the above case, i==0)?

Thanks, Holger

Coordinator
Nov 9, 2009 at 10:24 AM

Hi Holger,

  VCC does not distinguish between "non-satisfiable asserts" or "not-always-satisfied asserts". The reason why assert(false) seems to stop VCC afterwards, is, because the assertion is directly assumed afterwards, i.e., in this case you get to assume(false) which makes the rest of the proof trivial.

  You can tell VCC (or Boogie rather) via the /b:/errorLimit:X option to stop after X verification errors; if you start VCC on your above example with /b:/errorLimit:1, VCC will stop after the first assertion.

  Hope that helps, Mark

Nov 9, 2009 at 11:14 AM

Hi Mark,

perfect - exactly what I have been looking for :-)

Thanks, Holger