Skip to content

Commit

Permalink
fix for deterministicExtractLoops for nested loops
Browse files Browse the repository at this point in the history
  • Loading branch information
shuvendu-lahiri committed Oct 28, 2015
1 parent e037ca9 commit 02f5c06
Show file tree
Hide file tree
Showing 3 changed files with 44 additions and 1 deletion.
3 changes: 2 additions & 1 deletion Source/Core/Absy.cs
Original file line number Diff line number Diff line change
Expand Up @@ -991,7 +991,8 @@ void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g,
//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
Expand Down
23 changes: 23 additions & 0 deletions Test/extractloops/detLoopExtractNested.bpl
Original file line number Diff line number Diff line change
@@ -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
}

19 changes: 19 additions & 0 deletions Test/extractloops/detLoopExtractNested.bpl.expect
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 02f5c06

Please sign in to comment.