1

Closed

Boogie verification Condition

description

Hi,

I was trying to generate verification condition from boogie code. I have used the on-line compiler version and Boogie2 version installed Ubuntu 16.04.

The following code was given:

// RUN: %boogie -noVerify "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
procedure Dup(y: int)
{
X:
X: // error: duplicate label
while (y < 100)
{
Y:
}
while (y < 1000)
{
Y:  // error: duplicate label (labels must be unique in entire procedure body)
}
}


I got the output as:

Boogie program verifier finished with 1 verified, 0 errors

Question:
  • How will I generate a verification condition for such a code.
  • How can I generate a counter example from this.
  • Is there any command for generating verification condition and counter example in Ubuntu terminal.
Closed Feb 21 at 8:49 AM by danliew
Codeplex is no longer used.

comments

danliew wrote Feb 21 at 8:49 AM

Boogie is no longer developed here. Please visit https://github.com/boogie-org/boogie