diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/Absy.cs | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index c2e68002..8c04007b 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -750,15 +750,28 @@ namespace Microsoft.Boogie { Contract.Assert(block != null); var auxCmd = block.TransferCmd as GotoCmd; if (auxCmd == null) continue; - foreach(var bl in auxCmd.labelTargets) + foreach (var bl in auxCmd.labelTargets) { if (loopBlocks.Contains(bl)) continue; - immSuccBlks.Add(bl); + immSuccBlks.Add(bl); } } return immSuccBlks; } + private HashSet<Block> GetBlocksInAllNaturalLoops(Block header, Graph<Block/*!*/>/*!*/ g) + { + Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option"); + var allBlocksInNaturalLoops = new HashSet<Block>(); + foreach (Block/*!*/ source in g.BackEdgeNodes(header)) + { + Contract.Assert(source != null); + g.NaturalLoops(header, source).Iter(b => allBlocksInNaturalLoops.Add(b)); + } + return allBlocksInNaturalLoops; + } + + void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g, List<Implementation/*!*/>/*!*/ loopImpls, Dictionary<string, Dictionary<string, Block>> fullMap) { @@ -975,8 +988,8 @@ namespace Microsoft.Boogie { GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd; Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null && auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1); - var blksThatBreakOut = GetBreakBlocksOfLoop(header, source, g); - var loopNodes = g.NaturalLoops(header, source); + //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)) { Block auxNewBlock = new Block(); |