summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/Absy.cs21
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();