Feature request: Assert_fail

Sep 8, 2011 at 11:46 AM

I would quite like to be able to write:

_(assert_fail p)

in my program. At this point, VCC should try to prove

_(assert p)

and then, if that succeeds, it should report an error, and if it fails, it should skip. The intended use is to write 

_(assert_fail \false)

at various exit points of my function, to ensure that they remain reachable, and that I don't accidentally introduce contradictory assumptions while doing the verification. I realise that this is roughly the purpose of smoke; however, this approach is a little more flexible. For instance, I may not want to smoke my *whole* program, as that takes too long. Also, smoke only runs after a *successful* verification.

Sep 8, 2011 at 12:03 PM

Sounds like a good idea to me, although it possibly will require a change of Boogie as well.