Check one block

Apr 4, 2011 at 2:58 PM

I see that boogie check the verification condition(vc) on the method BeginCheck (VC.cs).

If i want to check only the vc of one block can i use the same method?

And how i see if the prover failed or not?

Apr 8, 2011 at 10:24 PM

There's currently no support in Boogie for checking only one block, but that shouldn't be too difficult for you to add--if a check occurs outside the blocks to be check, treat it like an assume.  To do that, I suggest you add a command-line switch whereby a Boogie user can name which blocks to check.  Please document that switch like the others from the /help switch (see CommandLineOptions.cs).  You would use the existing mechanism to see if the prover failed or not.