diff options
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 4 | ||||
| -rw-r--r-- | Test/test2/Answer | 2 | ||||
| -rw-r--r-- | Test/test2/Structured.bpl | 17 |
3 files changed, 20 insertions, 3 deletions
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 66e9d4a6..b84770e3 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -38,7 +38,7 @@ namespace Microsoft.Boogie { public StructuredCmd ec;
public TransferCmd tc;
- public BigBlock successorBigBlock; // null if successor is end of procedure body (or if field has not yet been initialized)
+ public BigBlock successorBigBlock; // semantic successor (may be a back-edge, pointing back to enclosing while statement); null if successor is end of procedure body (or if field has not yet been initialized)
public BigBlock(IToken tok, string labelName, [Captured] List<Cmd> simpleCmds, StructuredCmd ec, TransferCmd tc) {
Contract.Requires(simpleCmds != null);
@@ -434,7 +434,7 @@ namespace Microsoft.Boogie { if (big.ec is WhileCmd) {
WhileCmd wcmd = (WhileCmd)big.ec;
- RecordSuccessors(wcmd.Body, successor);
+ RecordSuccessors(wcmd.Body, big);
} else {
for (IfCmd ifcmd = big.ec as IfCmd; ifcmd != null; ifcmd = ifcmd.elseIf) {
RecordSuccessors(ifcmd.thn, successor);
diff --git a/Test/test2/Answer b/Test/test2/Answer index a88587e2..609cf1ed 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -237,7 +237,7 @@ Execution trace: Structured.bpl(308,3): anon1_Then
Structured.bpl(309,5): A
-Boogie program verifier finished with 15 verified, 3 errors
+Boogie program verifier finished with 16 verified, 3 errors
-------------------- Where.bpl --------------------
Where.bpl(8,3): Error BP5001: This assertion might not hold.
diff --git a/Test/test2/Structured.bpl b/Test/test2/Structured.bpl index 69ea2576..d5ce8cf4 100644 --- a/Test/test2/Structured.bpl +++ b/Test/test2/Structured.bpl @@ -325,3 +325,20 @@ procedure Q2() returns (x: int) }
}
}
+
+// There was once a bug in Boogie's handling of the following break statement.
+procedure BreakIssue(x: int) returns (curr: int)
+ ensures x == 18 || curr == 100; // holds, because the procedure doesn't
+ // actually ever terminate if x != 18
+{
+ while (x != 18) {
+ while (x != 19) {
+ call curr := Read();
+ if (curr == 0) {
+ break;
+ }
+ }
+ }
+}
+
+procedure Read() returns (val: int);
|