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: // error: duplicate label
while (y < 100)
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
- 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.