diff options
| -rw-r--r-- | Source/Core/Absy.cs | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 8daf39df..63f6d28d 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -631,6 +631,7 @@ namespace Microsoft.Boogie { Graph<Block/*!*/> g = new Graph<Block/*!*/>();
g.AddSource(impl.Blocks[0]); // there is always at least one node in the graph
+
foreach (Block b in impl.Blocks) {
Contract.Assert(b != null);
GotoCmd gtc = b.TransferCmd as GotoCmd;
@@ -644,12 +645,51 @@ namespace Microsoft.Boogie { return g;
}
+ // Delete unreachable Blocks of an Impl. This helps avoid a bug inside
+ // NewComputeDominators
+
+ public void pruneUnreachableBlocks(Implementation impl)
+ {
+ // Do a BFS to find all reachable blocks
+ List<Block> reachableBlocks = new List<Block>();
+ Set<string> visited = new Set<string>();
+ List<Block> worklist = new List<Block>();
+
+ visited.Add(impl.Blocks[0].Label);
+ worklist.Add(impl.Blocks[0]);
+
+ while (worklist.Count != 0)
+ {
+ var block = worklist[0];
+ worklist.RemoveAt(0);
+
+ reachableBlocks.Add(block);
+ GotoCmd gc = block.TransferCmd as GotoCmd;
+ if(gc == null) continue;
+
+ foreach (Block succ in gc.labelTargets)
+ {
+ if (visited.Contains(succ.Label)) continue;
+ visited.Add(succ.Label);
+ worklist.Add(succ);
+ }
+ }
+
+ // Delete unreachable blocks
+
+ // Make sure that the start block hasn't changed.
+ Contract.Assert(reachableBlocks[0] == impl.Blocks[0]);
+
+ impl.Blocks = reachableBlocks;
+ }
+
public Dictionary<string, Dictionary<string, Block>> ExtractLoops() {
List<Implementation/*!*/>/*!*/ loopImpls = new List<Implementation/*!*/>();
Dictionary<string, Dictionary<string, Block>> fullMap = new Dictionary<string, Dictionary<string, Block>>();
foreach (Declaration d in this.TopLevelDeclarations) {
Implementation impl = d as Implementation;
if (impl != null && impl.Blocks != null && impl.Blocks.Count > 0) {
+ pruneUnreachableBlocks(impl);
Graph<Block/*!*/>/*!*/ g = GraphFromImpl(impl);
g.ComputeLoops();
if (!g.Reducible) {
|