ExtractLoops calls the same code for eliminating unreachable blocks that normal VCgen calls. Deleted a procedure that was not being used as a result.

Added an extra assume(false) at the end of each DispatchContinuation to help boogie vcgen.

2 files changed, 3 insertions, 40 deletions

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index 0dc7c5ab..6bc399c1 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -106,6 +106,7 @@ namespace BytecodeTranslator
           elseIfCmd = new Bpl.IfCmd(Bpl.Token.NoToken, Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Eq, labelExpr, targetExpr), TranslationHelper.BuildStmtList(gotoCmd), elseIfCmd, null);

         }

         this.StmtBuilder.Add(elseIfCmd);

+        this.StmtBuilder.Add(new Bpl.AssumeCmd(Bpl.Token.NoToken, Bpl.Expr.Literal(false)));

       }

     }

     #endregion

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 7f5642f3..3a80a2ea 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -697,52 +697,14 @@ 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>();

-        HashSet<string> visited = new HashSet<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);

+          impl.PruneUnreachableBlocks();

           Graph<Block/*!*/>/*!*/ g = GraphFromImpl(impl);

           g.ComputeLoops();

           if (!g.Reducible) {