summaryrefslogtreecommitdiff
path: root/Test/test2/CutBackEdge.bpl
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2013-05-29 18:24:12 -0700
committerGravatar Rustan Leino <unknown>2013-05-29 18:24:12 -0700
commit2c9905f46791fed75c10fc8c8bc144fb8fa461f3 (patch)
treec24ded5b64ff2e9fc0766e13721bd849e453def6 /Test/test2/CutBackEdge.bpl
parenta9107b72346424a3e6486622cad8284ef731ada9 (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/CutBackEdge.bpl')
-rw-r--r--Test/test2/CutBackEdge.bpl26
1 files changed, 26 insertions, 0 deletions
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;
+}