summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Source/Core/Absy.cs3
-rw-r--r--Test/extractloops/detLoopExtractNested.bpl23
-rw-r--r--Test/extractloops/detLoopExtractNested.bpl.expect19
3 files changed, 44 insertions, 1 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 8c04007b..d2243085 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -991,7 +991,8 @@ namespace Microsoft.Boogie {
//BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode
var loopNodes = GetBlocksInAllNaturalLoops(header, g); //var loopNodes = g.NaturalLoops(header, source);
foreach(var bl in auxGotoCmd.labelTargets) {
- if (!loopNodes.Contains(bl)) {
+ if (g.Nodes.Contains(bl) && //newly created blocks are not present in NaturalLoop(header, xx, g)
+ !loopNodes.Contains(bl)) {
Block auxNewBlock = new Block();
auxNewBlock.Label = ((Block)bl).Label;
//these blocks may have read/write locals that are not present in naturalLoops
diff --git a/Test/extractloops/detLoopExtractNested.bpl b/Test/extractloops/detLoopExtractNested.bpl
new file mode 100644
index 00000000..65de20c1
--- /dev/null
+++ b/Test/extractloops/detLoopExtractNested.bpl
@@ -0,0 +1,23 @@
+// RUN: %boogie -nologo -stratifiedInline:1 -extractLoops -deterministicExtractLoops -recursionBound:100 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+//This example checks the bug fix in the loop extract for http://symdiff.codeplex.com/workitem/1
+
+var t: int;
+procedure {:entrypoint} NestedLoops()
+modifies t;
+//ensures t == 6;
+{
+ var i:int, j:int;
+ i, j, t := 0, 0, 0;
+ while(i < 2) {
+ j := 0;
+ while (j < 3) {
+ t := t + 1;
+ j := j + 1;
+ }
+ i := i + 1;
+ }
+ assume true; //would be provable (!true) wihtout the fix
+}
+
diff --git a/Test/extractloops/detLoopExtractNested.bpl.expect b/Test/extractloops/detLoopExtractNested.bpl.expect
new file mode 100644
index 00000000..f4932ede
--- /dev/null
+++ b/Test/extractloops/detLoopExtractNested.bpl.expect
@@ -0,0 +1,19 @@
+(0,0): Error BP5001: This assertion might not hold.
+Execution trace:
+ detLoopExtractNested.bpl(12,12): anon0
+ detLoopExtractNested.bpl(14,8): anon5_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(15,6): anon6_LoopDone
+ detLoopExtractNested.bpl(15,6): anon6_LoopDone
+ detLoopExtractNested.bpl(14,8): anon5_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(16,10): anon6_LoopBody
+ detLoopExtractNested.bpl(15,6): anon6_LoopDone
+ detLoopExtractNested.bpl(15,6): anon6_LoopDone
+ detLoopExtractNested.bpl(13,4): anon5_LoopDone
+ detLoopExtractNested.bpl(13,4): anon5_LoopDone
+
+Boogie program verifier finished with 0 verified, 1 error