diff options
| author |  Rustan Leino <unknown> | 2014-02-10 17:16:56 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-10 17:16:56 -0800 |
| commit | d52d16b298f3c2bc2e114ef712e7664534493a1d (patch) | |
| tree | 9d511d722c65942fbc9ffd940471b0d99364da51 /Test/test2 | |
| parent | 9a8cb7e40a8bde05f53e616a9b47f06fe57bcaed (diff) | |
Fixed bug in handling of break statements
Diffstat (limited to 'Test/test2')
| -rw-r--r-- | Test/test2/Answer | 2 | ||||
| -rw-r--r-- | Test/test2/Structured.bpl | 17 |
2 files changed, 18 insertions, 1 deletions
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);
|