diff options
author | Rustan Leino <unknown> | 2013-05-29 18:24:12 -0700 |
---|---|---|
committer | Rustan Leino <unknown> | 2013-05-29 18:24:12 -0700 |
commit | 2c9905f46791fed75c10fc8c8bc144fb8fa461f3 (patch) | |
tree | c24ded5b64ff2e9fc0766e13721bd849e453def6 /Test/test2 | |
parent | a9107b72346424a3e6486622cad8284ef731ada9 (diff) |
Fixed bug in the cutting of back edges (that manifested itself whenever the first block in a procedure was the target of a back edge)
Diffstat (limited to 'Test/test2')
-rw-r--r-- | Test/test2/Answer | 9 | ||||
-rw-r--r-- | Test/test2/CutBackEdge.bpl | 26 |
2 files changed, 34 insertions, 1 deletions
diff --git a/Test/test2/Answer b/Test/test2/Answer index 4a7fd32f..b936ef87 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -153,8 +153,15 @@ CutBackEdge.bpl(10,5): Error BP5005: This loop invariant might not be maintained Execution trace:
CutBackEdge.bpl(5,3): entry
CutBackEdge.bpl(9,3): block850
+CutBackEdge.bpl(20,5): Error BP5004: This loop invariant might not hold on entry.
+Execution trace:
+CutBackEdge.bpl(26,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ CutBackEdge.bpl(25,3): L
+CutBackEdge.bpl(38,5): Error BP5004: This loop invariant might not hold on entry.
+Execution trace:
-Boogie program verifier finished with 0 verified, 1 error
+Boogie program verifier finished with 1 verified, 4 errors
-------------------- False.bpl --------------------
diff --git a/Test/test2/CutBackEdge.bpl b/Test/test2/CutBackEdge.bpl index 934974aa..7294d0f9 100644 --- a/Test/test2/CutBackEdge.bpl +++ b/Test/test2/CutBackEdge.bpl @@ -12,3 +12,29 @@ procedure Test() goto block850;
}
+
+// The following procedure once exhibited a bug in Boogie's DAG manipulations
+procedure TightLoop0()
+{
+ L:
+ assert !true; // error
+ goto L;
+}
+procedure TightLoop1()
+{
+ L:
+ assert false; // error
+ goto L;
+}
+procedure TightLoop2()
+{
+ L:
+ assert true; // cool
+ goto L;
+}
+procedure TightLoop3(b: bool)
+{
+ L:
+ assert b; // error
+ goto L;
+}
|