diff options
| author |  Shuvendu Lahiri <shuvendu@microsoft.com> | 2015-10-27 17:40:33 -0700 |
|---|---|---|
| committer | Shuvendu Lahiri <shuvendu@microsoft.com> | 2015-10-27 17:40:33 -0700 |
| commit | 02f5c060ca5ce6bff003034ed634c114d5592398 (patch) | |
| tree | 272d491b09fc5606928de9325803b4345843c5d3 | |
| parent | e037ca99cdc163ca43690aaef3c380ebc1ce1962 (diff) | |
fix for deterministicExtractLoops for nested loops
| -rw-r--r-- | Source/Core/Absy.cs | 3 | ||||
| -rw-r--r-- | Test/extractloops/detLoopExtractNested.bpl | 23 | ||||
| -rw-r--r-- | Test/extractloops/detLoopExtractNested.bpl.expect | 19 |
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 |