Boogie:

* Bug fix:  Changed checking of postconditions to follow the order in which ensures clauses are given (not reverse order, as was previously the case)
* Added command-line option (/instrumentInfer) that decides how to instrument the Boogie program with inferred invariants.  Previously, the only option was to instrument at the beginning and end of every basic block.  The new option, which is now the default, is to instrument only at the beginning of loop heads.
* Add empty blocks between other blocks only as needed, and try a little harder to retain source information when blocks are peep-hole optimized
* Renamed flag /noRemoveEmptyBlocks to /removeEmptyBlocks:<c> where <c> is 0 or 1

Boogie refactoring:
* Removed LoopPredicate class and related classes and methods left over from when (back in the Zap 2 days) we supported loop invariants on demand
* Cleaned up some parsing of command-line options

3 files changed, 526 insertions, 494 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc
index 922ee68d..7d71f166 100644
--- a/Source/VCGeneration/ConditionGeneration.ssc
+++ b/Source/VCGeneration/ConditionGeneration.ssc
@@ -251,11 +251,13 @@ namespace VC
       

 

     /// <summary>

-    /// Modifies an implementation by inserting all preconditions

-    /// as assume statements at the beginning of the implementation

+    /// Modifies an implementation by prepending it with startCmds and then, as assume

+    /// statements, all preconditions.  Insert new blocks as needed, and adjust impl.Blocks[0]

+    /// accordingly to make it the new implementation entry block.

     /// </summary>

     /// <param name="impl"></param>

-    protected static void InjectPreconditions(Implementation! impl)

+    /// <param name="startCmds"></param>

+    protected static void InjectPreconditions(Implementation! impl, [Captured] CmdSeq! startCmds)

       requires impl.Proc != null;

     {

       TokenTextWriter debugWriter = null;

@@ -265,68 +267,65 @@ namespace VC
       }

     

       Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());

+      string LabelPrefix = "PreconditionGeneratedEntry";

+      int k = 0;

       

-      Block! originalEntryPoint = (!) impl.Blocks[0];

-      Block! currentEntryPoint = (!) impl.Blocks[0];

-      CmdSeq! currentClump = new CmdSeq(); // to hold onto contiguous "regular" preconditions

+      Block origStartBlock = impl.Blocks[0];

+      Block insertionPoint = new Block(

+        new Token(-17, -4), LabelPrefix + k, startCmds,

+        new GotoCmd(Token.NoToken, new StringSeq(origStartBlock.Label), new BlockSeq(origStartBlock)));

+      k++;

+      impl.Blocks[0] = insertionPoint;  // make insertionPoint the start block

+      impl.Blocks.Add(origStartBlock);  // and put the previous start block at the end of the list

 

       // (free and checked) requires clauses

-      for (int i = impl.Proc.Requires.Length-1; 0 <= i; i--){

-        

-        // need to process the preconditions from bottom up, because

-        // for any that are BlockExprs, we need to thread them on

-        // to the top of the implementation

-

-        Requires req = impl.Proc.Requires[i];

-        Expr! e = Substituter.Apply(formalProcImplSubst, req.Condition);

-        BlockExpr be = req.Condition as BlockExpr;

-        if (be != null){

-          if (currentClump.Length > 0){

-            AddAsPrefix(currentEntryPoint, currentClump);

-            currentClump = new CmdSeq();

-          }

-          ThreadInBlockExpr(impl,currentEntryPoint, be,false,debugWriter);

-          currentEntryPoint = (!)be.Blocks[0];

-        }else{

-          Cmd! c = new AssumeCmd(req.tok, e);

-          currentClump.Add(c);

+      foreach (Requires! req in impl.Proc.Requires)

+        // invariant:  insertionPoint.TransferCmd is "goto origStartBlock;", but origStartBlock.Predecessors has not yet been updated

+      {

+        Expr e = Substituter.Apply(formalProcImplSubst, req.Condition);

+        BlockExpr be = e as BlockExpr;

+        if (be == null) {

+          // This is the normal case, where the precondition is an ordinary expression

+          Cmd c = new AssumeCmd(req.tok, e);

+          insertionPoint.Cmds.Add(c);

           if (debugWriter != null) { c.Emit(debugWriter, 1); }

+        } else {

+          // This is a BlockExpr, so append all of its blocks (changing return expressions

+          // to assume statements), make the insertion-point block goto the head block of the

+          // BlockExpr, and create a new empty block as the current insertion point.

+          // Here goes:  First, create the new block, which will become the new insertion

+          // point and which will serve as a target for the BlockExpr.  Move the goto's from

+          // the current insertion point to this new block.

+          Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new CmdSeq(), insertionPoint.TransferCmd);

+          k++;

+          // Second, append the BlockExpr blocks to the implementation's blocks

+          ThreadInBlockExpr(impl, nextIP, be, false, debugWriter);

+          // Third, make the old insertion-point block goto the entry block of the BlockExpr

+          Block beEntry = (!)be.Blocks[0];

+          insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(beEntry.Label), new BlockSeq(beEntry));

+          beEntry.Predecessors.Add(insertionPoint);

+          // Fourth, update the insertion point

+          insertionPoint = nextIP;

         }

-        

       }

+      origStartBlock.Predecessors.Add(insertionPoint);

       

-      if (currentClump.Length > 0){

-        AddAsPrefix(currentEntryPoint, currentClump);

-      }

-      

-      if (currentEntryPoint != originalEntryPoint){

-        string EntryLabel = "PreconditionGeneratedEntry";

-        Block! newEntry = new Block(new Token(-17, -4),EntryLabel,new CmdSeq(),

-                  new GotoCmd(Token.NoToken,

-              new StringSeq(currentEntryPoint.Label),

-              new BlockSeq(currentEntryPoint)));

-        currentEntryPoint.Predecessors.Add(newEntry);

-        List<Block!> newBody = new List<Block!>();

-        newBody.Add(newEntry);

-        newBody.AddRange(impl.Blocks);

-        impl.Blocks = newBody;

-      }

-

       if (debugWriter != null) { debugWriter.WriteLine(); }

-      

-      return;

     }

     /// <summary>

     /// Modifies an implementation by inserting all postconditions

     /// as assert statements at the end of the implementation

+    /// Returns the possibly-new unified exit block of the implementation

     /// </summary>

     /// <param name="impl"></param>

     /// <param name="unifiedExitblock">The unified exit block that has

     /// already been constructed for the implementation (and so

     /// is already an element of impl.Blocks)

     /// </param>

-    protected static void InjectPostConditions(Implementation! impl, Block! unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins)

+    protected static Block! InjectPostConditions(Implementation! impl, Block! unifiedExitBlock, Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins)

       requires impl.Proc != null;

+      requires unifiedExitBlock.TransferCmd is ReturnCmd;

+      ensures result.TransferCmd is ReturnCmd;

     {

       TokenTextWriter debugWriter = null;

       if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

@@ -334,58 +333,49 @@ namespace VC
         debugWriter.WriteLine("Effective postcondition:");

       }

       

-      string ExitLabel = "ReallyLastGeneratedExit";

-      Block! newExit = new Block(new Token(-17, -4),ExitLabel,new CmdSeq(),new ReturnCmd(Token.NoToken));

-      impl.Blocks.Add(newExit);

-      Block! currentEntryPoint = newExit;

-      CmdSeq! currentClump = new CmdSeq(); // to hold onto contiguous "regular" postconditions

-

       Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());

+      Block insertionPoint = unifiedExitBlock;

+      string LabelPrefix = "ReallyLastGeneratedExit";

+      int k = 0;

 

       // (free and checked) ensures clauses

-      for (int i = impl.Proc.Ensures.Length-1; 0 <= i; i--){

-        

-        // need to process the postconditions from bottom up, because

-        // for any that are BlockExprs, we need to thread them on

-        // to the top of the implementation

-

-        Ensures ens = (impl.Proc).Ensures[i];

-        if (!ens.Free) { // free ensures aren't needed for verifying the implementation

-          Expr! e = Substituter.Apply(formalProcImplSubst, ens.Condition);

+      foreach (Ensures! ens in impl.Proc.Ensures)

+        invariant insertionPoint.TransferCmd is ReturnCmd;

+      {

+        if (!ens.Free) { // skip free ensures clauses

+          Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition);

           BlockExpr be = ens.Condition as BlockExpr;

-          if (be != null){

-            if (currentClump.Length > 0){

-              AddAsPrefix(currentEntryPoint, currentClump);

-              currentClump = new CmdSeq();

-            }

-            ThreadInBlockExpr(impl,currentEntryPoint,be,true,debugWriter);

-            currentEntryPoint = (!)be.Blocks[0];

-          }else{

-            Ensures! ensCopy = (Ensures!) ens.Clone();

+          if (be == null) {

+            // This is the normal case, where the postcondition is an ordinary expression

+            Ensures ensCopy = (Ensures!) ens.Clone();

             ensCopy.Condition = e;

-            Cmd! c = new AssertEnsuresCmd(ensCopy);

-            ((AssertEnsuresCmd) c).ErrorDataEnhanced = ensCopy.ErrorDataEnhanced;

-            currentClump.Add(c);

+            AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy);

+            c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced;

+            insertionPoint.Cmds.Add(c);

             if (debugWriter != null) { c.Emit(debugWriter, 1); }

+          } else {

+            // This is a BlockExpr, so append all of its blocks (changing return expressions

+            // to assert statements), insert a goto to its head block from the current insertion

+            // point, and create a new empty block as the current insertion point.

+            // Here goes:  First, create the new block, which will become the new insertion

+            // point and which will serve as a target for the BlockExpr.  Steal the TransferCmd

+            // from insertionPoint, since insertionPoint's TransferCmd will soon be replaced anyhow.

+            Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new CmdSeq(), insertionPoint.TransferCmd);

+            k++;

+            // Second, append the BlockExpr blocks to the implementation's blocks

+            ThreadInBlockExpr(impl, nextIP, be, true, debugWriter);

+            // Third, make the old insertion-point block goto the entry block of the BlockExpr

+            Block beEntry = (!)be.Blocks[0];

+            insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(beEntry.Label), new BlockSeq(beEntry));

+            beEntry.Predecessors.Add(insertionPoint);

+            // Fourth, update the insertion point

+            insertionPoint = nextIP;

           }

         }

-          

-      }

-      

-      if (currentClump.Length > 0){

-        AddAsPrefix(currentEntryPoint, currentClump);

       }

       

-      GotoCmd gtc = new GotoCmd(Token.NoToken,

-            new StringSeq(currentEntryPoint.Label),

-            new BlockSeq(currentEntryPoint));

-      gotoCmdOrigins[gtc] = unifiedExitBlock.TransferCmd;

-      unifiedExitBlock.TransferCmd = gtc;

-      currentEntryPoint.Predecessors.Add(unifiedExitBlock);

-      

       if (debugWriter != null) { debugWriter.WriteLine(); }

-      

-      return;

+      return insertionPoint;

     }

 

 

@@ -558,6 +548,7 @@ namespace VC
 

 

     protected Block! GenerateUnifiedExit(Implementation! impl, Hashtable! gotoCmdOrigins)

+      ensures result.TransferCmd is ReturnCmd;

     {

       Block/*?*/ exitBlock = null;

       #region Create a unified exit block, if there's more than one

@@ -659,7 +650,7 @@ namespace VC
         -1;

       Variable v = new Incarnation(x,currentIncarnationNumber + 1);

       variable2SequenceNumber[x] = currentIncarnationNumber + 1;

-      Debug.Assert(current_impl != null, "The field current_impl wasn't set.");

+      assert current_impl != null;  // otherwise, the field current_impl wasn't set

       current_impl.LocVars.Add(v);

       incarnationOriginMap.Add((Incarnation) v, a);

       return v;

@@ -691,7 +682,7 @@ namespace VC
       Set /*Variable*/ fixUps = new Set /*Variable*/ ();

       foreach (Block! pred in b.Predecessors)

       {

-        Debug.Assert(block2Incarnation.Contains(pred), "Passive Transformation found a block whose predecessors have not been processed yet.");

+        assert block2Incarnation.Contains(pred);  // otherwise, Passive Transformation found a block whose predecessors have not been processed yet

         Hashtable /*Variable -> Expr*/ predMap = (Hashtable! /*Variable -> Expr*/) block2Incarnation[pred];

         if (incarnationMap == null)

         {

@@ -818,7 +809,7 @@ namespace VC
         }

       }

       IEnumerable! sortedNodes = dag.TopologicalSort();

-      //Debug.Assert( sortedNodes != null, "Topological Sort returned null." );

+      // assume sortedNodes != null;

       #endregion

       

       // Create substitution for old expressions

@@ -835,7 +826,7 @@ namespace VC
       Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();

       foreach (Block! b in sortedNodes )

       {

-        Debug.Assert( !block2Incarnation.Contains(b) );

+        assert !block2Incarnation.Contains(b);

         Hashtable /*Variable -> Expr*/ incarnationMap = ComputeIncarnationMap(b, block2Incarnation);

         

         #region Each block's map needs to be available to successor blocks

@@ -869,17 +860,10 @@ namespace VC
         #region assert/assume P |--> assert/assume P[x := in(x)], out := in

         if ( c is PredicateCmd )

         {          

-          Debug.Assert( c is AssertCmd || c is AssumeCmd, "Internal Error: Found a PredicateCmd h is not an assert or an assume." );

+          assert c is AssertCmd || c is AssumeCmd;  // otherwise, unexpected PredicateCmd type

            

           PredicateCmd! pc = (PredicateCmd) c.Clone();

               

-          if(pc is AssumeCmd && pc.Expr is LoopPredicate   // Check if the PredicateCmd is in the form of "assume J", with J loop invariant predicate

-              && this.preHavocIncarnationMap != null)      // Furthermore, the command just before was a (list of) havoc statements 

-          {

-            LoopPredicate! lp = (LoopPredicate!) pc.Expr;

-            lp.SetPreAndPostHavocIncarnationMaps(this.preHavocIncarnationMap, (Hashtable /*Variable -> Expr*/!) incarnationMap.Clone());

-          }

-    

           Expr! copy = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, pc.Expr);

           if (pc is AssertCmd) {

             ((AssertCmd) pc).OrigExpr = pc.Expr;

@@ -1086,16 +1070,21 @@ namespace VC
      

     protected void AddBlocksBetween(Implementation! impl)

     {

-      #region Introduce empty blocks before all blocks with more than one predecessor

+      #region Introduce empty blocks between join points and their multi-successor predecessors

       List<Block!> tweens = new List<Block!>();

       foreach ( Block b in impl.Blocks )

       {

         int nPreds = b.Predecessors.Length;

         if ( nPreds > 1 ) 

         {

+          // b is a join point (i.e., it has more than one predecessor)

           for (int i = 0; i < nPreds; i++ ) 

           {

-            tweens.Add(CreateBlockBetween(i, b));

+            GotoCmd gotocmd = (GotoCmd!)((!)b.Predecessors[i]).TransferCmd;

+            if (gotocmd.labelNames != null && gotocmd.labelNames.Length > 1)

+            {

+              tweens.Add(CreateBlockBetween(i, b));

+            }

           }

         }

       }

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index cdc6dde2..7f890826 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -1575,10 +1575,10 @@ namespace VC
         {

           Block! pred = (!)header.Predecessors[predIndex];

           

-          // Create a block between header and pred for the predicate commands if header has more than one successor 

-          // or if pred is a back edge node

-          GotoCmd gotocmd = pred.TransferCmd as GotoCmd;

-          if ((backEdgeNodes.ContainsKey(pred)) || (gotocmd != null && gotocmd.labelNames != null && gotocmd.labelNames.Length > 1))

+          // Create a block between header and pred for the predicate commands if pred has more than one successor 

+          GotoCmd gotocmd = (GotoCmd!)pred.TransferCmd;

+          assert gotocmd.labelNames != null;  // if "pred" is really a predecessor, it may be a GotoCmd with at least one label

+          if (gotocmd.labelNames.Length > 1)

           {

             Block! newBlock = CreateBlockBetween(predIndex, header);

             impl.Blocks.Add(newBlock);

@@ -1691,7 +1691,7 @@ namespace VC
     protected Hashtable/*TransferCmd->ReturnCmd*/! PassifyImpl(Implementation! impl, Program! program)

     {

       Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = new Hashtable/*TransferCmd->ReturnCmd*/();

-      Block/*?*/ exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);

+      Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);

       

       #region Debug Tracing

       if (CommandLineOptions.Clo.TraceVerify) 

@@ -1722,16 +1722,11 @@ namespace VC
           }

         }

 

-        InjectPreconditions(impl);

-        //cc.AddRange(GetPre(impl));

+        // add cc and the preconditions to new blocks preceding impl.Blocks[0]

+        InjectPreconditions(impl, cc);

 

-        Block! entryBlock = (!) impl.Blocks[0];

-        cc.AddRange(entryBlock.Cmds);

-        entryBlock.Cmds = cc;

-          

-        InjectPostConditions(impl,exitBlock,gotoCmdOrigins);

-        //CmdSeq! post = GetPost(impl);

-        //exitBlock.Cmds.AddRange(post);

+        // append postconditions, starting in exitBlock and continuing into other blocks, if needed

+        exitBlock = InjectPostConditions(impl, exitBlock, gotoCmdOrigins);

       }

       #endregion

       

@@ -1748,21 +1743,21 @@ namespace VC
       #region Debug Tracing

       if (CommandLineOptions.Clo.TraceVerify) 

       {

-        Console.WriteLine("after adding empty blocks before all blocks with more than one predecessor");

+        Console.WriteLine("after adding empty blocks as needed to catch join assumptions");

         EmitImpl(impl, true);

       }

       #endregion

     

       if (CommandLineOptions.Clo.LiveVariableAnalysis) {

-	    Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);

-	  }

-	  

+        Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);

+      }

+      

       Convert2PassiveCmd(impl);

       

       if (CommandLineOptions.Clo.LiveVariableAnalysis) {

-	    Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);

-	  }

-	  

+        Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);

+      }

+      

       #region Peep-hole optimizations

       if (CommandLineOptions.Clo.RemoveEmptyBlocks){

         #region Get rid of empty blocks

@@ -2867,49 +2862,110 @@ namespace VC
     static BlockSeq! RemoveEmptyBlocks(Block! b)

     {

       assert b.TraversingStatus == Block.VisitState.ToVisit;

-      BlockSeq retVal = removeEmptyBlocksWorker(b, true);

+      Block renameInfo;

+      BlockSeq retVal = removeEmptyBlocksWorker(b, true, out renameInfo);

+      if (renameInfo != null && !b.tok.IsValid) {

+        bool onlyAssumes = true;

+        foreach (Cmd c in b.Cmds) {

+          if (!(c is AssumeCmd)) {

+            onlyAssumes = false;

+            break;

+          }

+        }

+        if (onlyAssumes) {

+          b.tok = renameInfo.tok;

+          b.Label = renameInfo.Label;

+        }

+      }

       return retVal;

     }

 

-    private static BlockSeq! removeEmptyBlocksWorker(Block! b, bool startNode)

+    /// <summary>

+    /// For every not-yet-visited block n reachable from b, change n's successors to skip empty nodes.

+    /// Return the *set* of blocks reachable from b without passing through a nonempty block.

+    /// The target of any backedge is counted as a nonempty block.

+    /// If renameInfoForStartBlock is non-null, it denotes an empty block with location information, and that

+    /// information would be appropriate to display

+    /// </summary>

+    private static BlockSeq! removeEmptyBlocksWorker(Block! b, bool startNode, out Block renameInfoForStartBlock)

+      ensures renameInfoForStartBlock != null ==> renameInfoForStartBlock.tok.IsValid;

+      // ensures: b in result ==> renameInfoForStartBlock == null;

     {

+      renameInfoForStartBlock = null;

       BlockSeq bs = new BlockSeq();

       GotoCmd gtc = b.TransferCmd as GotoCmd;

 

       // b has no successors

       if (gtc == null || gtc.labelTargets == null || gtc.labelTargets.Length == 0) 

-      {        

+      {

         if (b.Cmds.Length != 0){ // only empty blocks are removed...

           bs.Add(b);

+        } else if (b.tok.IsValid) {

+          renameInfoForStartBlock = b;

         }

         return bs;

       }

-      else if(b.TraversingStatus == Block.VisitState.ToVisit)  // if b has some successors and we have not seen it so far...

+      else if (b.TraversingStatus == Block.VisitState.ToVisit)  // if b has some successors and we have not seen it so far...

       { 

         b.TraversingStatus = Block.VisitState.BeingVisited;

 

+        // Before recursing down to successors, make a sobering observation:

+        // If b has no commands and is not the start node, then it will see

+        // extinction (because it will not be included in the "return setOfSuccessors"

+        // statement below).  In that case, if b has a location, then the location

+        // information would be lost.  Hence, make an attempt to save the location

+        // by pushing the location onto b's successor.  This can be done if (0) b has

+        // exactly one successor, (1) that successor has no location of its own, and

+        // (2) that successor has no other predecessors.

+        if (b.Cmds.Length == 0 && !startNode) {

+          // b is about to become extinct; try to save its name and location, if possible

+          if (b.tok.IsValid && gtc.labelTargets.Length == 1) {

+            Block succ = (!)gtc.labelTargets[0];

+            if (!succ.tok.IsValid && succ.Predecessors.Length == 1) {

+              succ.tok = b.tok;

+              succ.Label = b.Label;

+            }

+          }

+        }

+

         // recursively call this method on each successor

         // merge result into a *set* of blocks

         Dictionary<Block,bool> mergedSuccessors = new Dictionary<Block,bool>();

+        int m = 0;  // in the following loop, set renameInfoForStartBlock to the value that all recursive calls agree on, if possible; otherwise, null

         foreach (Block! dest in gtc.labelTargets){

-          BlockSeq! ys = removeEmptyBlocksWorker(dest, false);

+          Block renameInfo;

+          BlockSeq! ys = removeEmptyBlocksWorker(dest, false, out renameInfo);

+          if (m == 0) {

+            renameInfoForStartBlock = renameInfo;

+          } else if (renameInfoForStartBlock != renameInfo) {

+            renameInfoForStartBlock = null;

+          }

           foreach (Block successor in ys){

             if (!mergedSuccessors.ContainsKey(successor))

               mergedSuccessors.Add(successor,true);

           }

+          m++;

         }

         b.TraversingStatus = Block.VisitState.AlreadyVisited;

 

         BlockSeq setOfSuccessors = new BlockSeq();

         foreach (Block d in mergedSuccessors.Keys)

           setOfSuccessors.Add(d);

-        if (b.Cmds.Length == 0 && !startNode)

+        if (b.Cmds.Length == 0 && !startNode) {

+          // b is about to become extinct

+          if (b.tok.IsValid) {

+            renameInfoForStartBlock = b;

+          }

           return setOfSuccessors;

+        }

         // otherwise, update the list of successors of b to be the blocks in setOfSuccessors

         gtc.labelTargets = setOfSuccessors;

         gtc.labelNames = new StringSeq();

         foreach (Block! d in setOfSuccessors)

           gtc.labelNames.Add(d.Label);

+        if (!startNode) {

+          renameInfoForStartBlock = null;

+        }

         return new BlockSeq(b);

       }

       else // b has some successors, but we are already visiting it, or we have already visited it...

diff --git a/Source/VCGeneration/VCDoomed.ssc b/Source/VCGeneration/VCDoomed.ssc
index f1487fad..f3720e7f 100644
--- a/Source/VCGeneration/VCDoomed.ssc
+++ b/Source/VCGeneration/VCDoomed.ssc
@@ -634,13 +634,13 @@ namespace VC
             out Dictionary<Block!, Block!> copiedblocks)

       {

         Block! start = impl.Blocks[0];

-		Dictionary<Block,GraphNode!> gd = new Dictionary<Block,GraphNode!>();

-		Set/*Block*/! beingVisited = new Set/*Block*/();

-		GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited);

+        Dictionary<Block,GraphNode!> gd = new Dictionary<Block,GraphNode!>();

+        Set/*Block*/! beingVisited = new Set/*Block*/();

+        GraphNode gStart = GraphNode.ComputeGraphInfo(null, start, gd, beingVisited);

       

         DCProgramTransformer pt = new DCProgramTransformer(checkableBlocks);

-  		pt.LoopUnrolling(gStart, new Dictionary<GraphNode, Block!>(), true, "");	

-	  	pt.Blocks.Reverse();

+          pt.LoopUnrolling(gStart, new Dictionary<GraphNode, Block!>(), true, "");    

+          pt.Blocks.Reverse();

         copiedblocks = pt.m_copyMap;

         return pt.Blocks;

       }

@@ -655,262 +655,262 @@ namespace VC
 

 #region Loop Unrolling Methods

     

-		private Block! LoopUnrolling(GraphNode! node, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)

-		{

-			Block newb;

-			if (visited.TryGetValue(node, out newb)) 

-			{

-				assert newb!=null;

-				return newb;

-			} else 

-			{

-				if (node.IsCutPoint)

-				{

-					// compute the loop body and the blocks leaving the loop

-					

-					List<GraphNode!>! loopNodes = new List<GraphNode!>();

-					GatherLoopBodyNodes(node, node, loopNodes);

+        private Block! LoopUnrolling(GraphNode! node, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)

+        {

+            Block newb;

+            if (visited.TryGetValue(node, out newb)) 

+            {

+                assert newb!=null;

+                return newb;

+            } else 

+            {

+                if (node.IsCutPoint)

+                {

+                    // compute the loop body and the blocks leaving the loop

+                    

+                    List<GraphNode!>! loopNodes = new List<GraphNode!>();

+                    GatherLoopBodyNodes(node, node, loopNodes);

 

-					List<GraphNode!>! exitNodes = GatherLoopExitNodes(loopNodes);

-					

-					// Continue Unrolling after the current loop

-					Dictionary<GraphNode, Block!>! _visited = new Dictionary<GraphNode, Block!>();

-					foreach (GraphNode! g in exitNodes)

-					{					

-						Block b = LoopUnrolling(g, visited, unrollable, prefix);

-						_visited.Add(g,b);

-					}

-					newb = UnrollCurrentLoop(node, _visited, loopNodes,unrollable, prefix);

-					visited.Add(node,newb);

-				} else

-				{

-					BlockSeq! newSuccs = new BlockSeq();

-					foreach(GraphNode! g in node.Succecessors)

-					{

-						newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );

-					}

-					newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);

+                    List<GraphNode!>! exitNodes = GatherLoopExitNodes(loopNodes);

+                    

+                    // Continue Unrolling after the current loop

+                    Dictionary<GraphNode, Block!>! _visited = new Dictionary<GraphNode, Block!>();

+                    foreach (GraphNode! g in exitNodes)

+                    {                    

+                        Block b = LoopUnrolling(g, visited, unrollable, prefix);

+                        _visited.Add(g,b);

+                    }

+                    newb = UnrollCurrentLoop(node, _visited, loopNodes,unrollable, prefix);

+                    visited.Add(node,newb);

+                } else

+                {

+                    BlockSeq! newSuccs = new BlockSeq();

+                    foreach(GraphNode! g in node.Succecessors)

+                    {

+                        newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );

+                    }

+                    newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd);

                     Block b;

-			        if (m_copyMap.TryGetValue(node.Block, out b) ) {

-			            assert b!=null;

-			            m_copyMap.Add(newb, b);

-			        } else {

-			            m_copyMap.Add(newb, node.Block);

-			        }

-					

-					

-					assert newb!=null; assert newb.TransferCmd!=null;					

-					if (newSuccs.Length == 0) 

-						newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);

-					else 

-						newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);

-										

-					visited.Add(node, newb);

-					Blocks.Add(newb);

-					if (unrollable) 

-					{					  

-					  m_checkableBlocks.Add(newb);

-					}

-				}	

-			}

-			assert newb!=null;

-			//newb.checkable = unrollable;

-			return newb;				

-		}

+                    if (m_copyMap.TryGetValue(node.Block, out b) ) {

+                        assert b!=null;

+                        m_copyMap.Add(newb, b);

+                    } else {

+                        m_copyMap.Add(newb, node.Block);

+                    }

+                    

+                    

+                    assert newb!=null; assert newb.TransferCmd!=null;                    

+                    if (newSuccs.Length == 0) 

+                        newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);

+                    else 

+                        newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);

+                                        

+                    visited.Add(node, newb);

+                    Blocks.Add(newb);

+                    if (unrollable) 

+                    {                      

+                      m_checkableBlocks.Add(newb);

+                    }

+                }    

+            }

+            assert newb!=null;

+            //newb.checkable = unrollable;

+            return newb;                

+        }

 

-		private Block! UnrollCurrentLoop(GraphNode! cutPoint, Dictionary<GraphNode, Block!>! visited, 

-								List<GraphNode!>! loopNodes, bool unrollable, String! prefix)

-		{

-			if (unrollable)

-			{

-				Dictionary<GraphNode, Block!>! visited1 = new Dictionary<GraphNode, Block!>(visited);

-				Dictionary<GraphNode, Block!>! visited2 = new Dictionary<GraphNode, Block!>(visited);

-				Dictionary<GraphNode, Block!>! visited3 = new Dictionary<GraphNode, Block!>(visited);

+        private Block! UnrollCurrentLoop(GraphNode! cutPoint, Dictionary<GraphNode, Block!>! visited, 

+                                List<GraphNode!>! loopNodes, bool unrollable, String! prefix)

+        {

+            if (unrollable)

+            {

+                Dictionary<GraphNode, Block!>! visited1 = new Dictionary<GraphNode, Block!>(visited);

+                Dictionary<GraphNode, Block!>! visited2 = new Dictionary<GraphNode, Block!>(visited);

+                Dictionary<GraphNode, Block!>! visited3 = new Dictionary<GraphNode, Block!>(visited);

 

-				Block! loopend = ConstructLoopExitBlock(cutPoint, loopNodes, visited, prefix+"#Last");

-			

-				Block! last = UnrollOnce(cutPoint, loopend,visited1,false, prefix+"#Last");

-				AddHavocCmd(last,loopNodes);				

-				

-				// You might use true for the unrollable flag as well. 					

-				Block! arb = UnrollOnce(cutPoint, last,visited2,false, prefix+"#Arb");

-				AddHavocCmd(arb,loopNodes);

-				

-						

-				BlockSeq! succ = new BlockSeq();

-				succ.Add(last); succ.Add(arb);

-				assert arb.TransferCmd!=null;

-				Block! tmp = new Block(arb.tok, arb.Label + prefix+"#Dummy" , new CmdSeq(), new GotoCmd(arb.TransferCmd.tok, succ));

-				Blocks.Add(tmp);

-				m_checkableBlocks.Add(tmp);

+                Block! loopend = ConstructLoopExitBlock(cutPoint, loopNodes, visited, prefix+"#Last");

+            

+                Block! last = UnrollOnce(cutPoint, loopend,visited1,false, prefix+"#Last");

+                AddHavocCmd(last,loopNodes);                

+                

+                // You might use true for the unrollable flag as well.                     

+                Block! arb = UnrollOnce(cutPoint, last,visited2,false, prefix+"#Arb");

+                AddHavocCmd(arb,loopNodes);

+                

+                        

+                BlockSeq! succ = new BlockSeq();

+                succ.Add(last); succ.Add(arb);

+                assert arb.TransferCmd!=null;

+                Block! tmp = new Block(arb.tok, arb.Label + prefix+"#Dummy" , new CmdSeq(), new GotoCmd(arb.TransferCmd.tok, succ));

+                Blocks.Add(tmp);

+                m_checkableBlocks.Add(tmp);

 

                 // check if arb is already a copy of something else

                 // if not then write to m_copyMap that tmp is a copy

                 // of arb

-				Block b = null;

-				if (m_copyMap.TryGetValue(arb,out b) ) {

-				    assert b!=null;

-				    m_copyMap.Add(tmp, b);

-				} else {

-				    m_copyMap.Add(tmp, arb);

-				}

+                Block b = null;

+                if (m_copyMap.TryGetValue(arb,out b) ) {

+                    assert b!=null;

+                    m_copyMap.Add(tmp, b);

+                } else {

+                    m_copyMap.Add(tmp, arb);

+                }

 

-				Block! first = UnrollOnce(cutPoint, tmp,visited3,false, prefix+"#First");

-				

-				return first;

+                Block! first = UnrollOnce(cutPoint, tmp,visited3,false, prefix+"#First");

+                

+                return first;

 

-			} else

-			{

-				Dictionary<GraphNode, Block!>! visited_ = new Dictionary<GraphNode, Block!>(visited);

-				Block! loopend = AbstractIteration(cutPoint, prefix+"#UR");				

-				Block! ret = UnrollOnce(cutPoint, loopend,visited_,false, prefix);

-				AddHavocCmd(ret, loopNodes);

-				return ret;			

-			}

-		}

-		

-		private Block! UnrollOnce(GraphNode! node, Block! nextIter, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)

-		{

-			visited.Add(node, nextIter);

-			Block newb,b;

-			BlockSeq! newSuccs = new BlockSeq();

-			foreach(GraphNode! g in node.Succecessors)

-			{

-				newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );

-			}

-			newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd); 

-			if (m_copyMap.TryGetValue(node.Block, out b) ) {

-			    assert b!=null;

-			    m_copyMap.Add(newb, b);

-			} else {

-			    m_copyMap.Add(newb, node.Block);

-			}

-			 

-			assert newb!=null; assert newb.TransferCmd!=null;					

-			if (newSuccs.Length == 0) 

-				newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);

-			else 

-				newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);

-											

-			Blocks.Add(newb);

-			if (unrollable) m_checkableBlocks.Add(newb);

-			return newb;

-		}

+            } else

+            {

+                Dictionary<GraphNode, Block!>! visited_ = new Dictionary<GraphNode, Block!>(visited);

+                Block! loopend = AbstractIteration(cutPoint, prefix+"#UR");                

+                Block! ret = UnrollOnce(cutPoint, loopend,visited_,false, prefix);

+                AddHavocCmd(ret, loopNodes);

+                return ret;            

+            }

+        }

+        

+        private Block! UnrollOnce(GraphNode! node, Block! nextIter, Dictionary<GraphNode, Block!>! visited, bool unrollable, String! prefix)

+        {

+            visited.Add(node, nextIter);

+            Block newb,b;

+            BlockSeq! newSuccs = new BlockSeq();

+            foreach(GraphNode! g in node.Succecessors)

+            {

+                newSuccs.Add( LoopUnrolling(g,visited,unrollable,prefix) );

+            }

+            newb = new Block(node.Block.tok, node.Block.Label + prefix , node.Body, node.Block.TransferCmd); 

+            if (m_copyMap.TryGetValue(node.Block, out b) ) {

+                assert b!=null;

+                m_copyMap.Add(newb, b);

+            } else {

+                m_copyMap.Add(newb, node.Block);

+            }

+             

+            assert newb!=null; assert newb.TransferCmd!=null;                    

+            if (newSuccs.Length == 0) 

+                newb.TransferCmd = new ReturnCmd(newb.TransferCmd.tok);

+            else 

+                newb.TransferCmd = new GotoCmd(newb.TransferCmd.tok, newSuccs);

+                                            

+            Blocks.Add(newb);

+            if (unrollable) m_checkableBlocks.Add(newb);

+            return newb;

+        }

 

-		private Block! AbstractIteration(GraphNode! node, String! prefix)

-		{

-			CmdSeq body = new CmdSeq();

-			foreach (Cmd! c in node.Body)

-			{

-				if (c is PredicateCmd || c is CommentCmd)

-					body.Add(c );

-				else

-					break;

-			}

-			body.Add(new AssumeCmd(node.Block.tok, Expr.False) );

-			TransferCmd! tcmd = new ReturnCmd(node.Block.tok);

-			Block! b = new Block(node.Block.tok, node.Block.Label + prefix, body, tcmd);

-			Blocks.Add(b);

+        private Block! AbstractIteration(GraphNode! node, String! prefix)

+        {

+            CmdSeq body = new CmdSeq();

+            foreach (Cmd! c in node.Body)

+            {

+                if (c is PredicateCmd || c is CommentCmd)

+                    body.Add(c );

+                else

+                    break;

+            }

+            body.Add(new AssumeCmd(node.Block.tok, Expr.False) );

+            TransferCmd! tcmd = new ReturnCmd(node.Block.tok);

+            Block! b = new Block(node.Block.tok, node.Block.Label + prefix, body, tcmd);

+            Blocks.Add(b);

             Block tmp; 

-			if (m_copyMap.TryGetValue(node.Block, out tmp) ) {

-			    assert tmp!=null;

-			    m_copyMap.Add(b, tmp);

-			} else {

-			    m_copyMap.Add(b, node.Block);

-			}

-			

-			return b;

-		}

+            if (m_copyMap.TryGetValue(node.Block, out tmp) ) {

+                assert tmp!=null;

+                m_copyMap.Add(b, tmp);

+            } else {

+                m_copyMap.Add(b, node.Block);

+            }

+            

+            return b;

+        }

 

-		private Block! ConstructLoopExitBlock(GraphNode! cutPoint, List<GraphNode!>! loopNodes, 

-												Dictionary<GraphNode, Block!>! visited, String! prefix)

-		{

-			BlockSeq! newSucc = new BlockSeq();

-			Block! orig = cutPoint.Block;

-			

-			// detect the block after the loop

-			// FixMe: What happens when using break commands?

-			foreach (GraphNode! g in cutPoint.Succecessors)

-			{

-				if (!loopNodes.Contains(g)) 

-				{

-					Block b;

-					if (visited.TryGetValue(g,out b) )

-						newSucc.Add(b);

-				}

-			}

-			TransferCmd tcmd;

-			assert orig.TransferCmd!=null;

-			if (newSucc.Length==0)

-				tcmd = new ReturnCmd(orig.TransferCmd.tok);

-			else

-				tcmd = new GotoCmd(orig.TransferCmd.tok, newSucc);

-			// FixMe: Genertate IToken for counterexample creation

-			Block! newb = new Block(orig.tok, orig.Label+prefix+"#Leave", orig.Cmds, tcmd);

-			Blocks.Add(newb);

-			m_checkableBlocks.Add(newb); 

-			return newb;

-		}

+        private Block! ConstructLoopExitBlock(GraphNode! cutPoint, List<GraphNode!>! loopNodes, 

+                                                Dictionary<GraphNode, Block!>! visited, String! prefix)

+        {

+            BlockSeq! newSucc = new BlockSeq();

+            Block! orig = cutPoint.Block;

+            

+            // detect the block after the loop

+            // FixMe: What happens when using break commands?

+            foreach (GraphNode! g in cutPoint.Succecessors)

+            {

+                if (!loopNodes.Contains(g)) 

+                {

+                    Block b;

+                    if (visited.TryGetValue(g,out b) )

+                        newSucc.Add(b);

+                }

+            }

+            TransferCmd tcmd;

+            assert orig.TransferCmd!=null;

+            if (newSucc.Length==0)

+                tcmd = new ReturnCmd(orig.TransferCmd.tok);

+            else

+                tcmd = new GotoCmd(orig.TransferCmd.tok, newSucc);

+            // FixMe: Genertate IToken for counterexample creation

+            Block! newb = new Block(orig.tok, orig.Label+prefix+"#Leave", orig.Cmds, tcmd);

+            Blocks.Add(newb);

+            m_checkableBlocks.Add(newb); 

+            return newb;

+        }

 

 

-		private void GatherLoopBodyNodes(GraphNode! current, GraphNode! cutPoint, List<GraphNode!>! loopNodes)

-		{

-			loopNodes.Add(current);

-			if (false) System.Diagnostics.Debugger.Break();

-			foreach (GraphNode! g in current.Predecessors)

-			{

-				if (cutPoint.firstPredecessor == g || g == cutPoint || loopNodes.Contains(g) ) continue;

-				GatherLoopBodyNodes(g, cutPoint, loopNodes);

-			}		

-		}

-		

-		private List<GraphNode!>! GatherLoopExitNodes(List<GraphNode!>! loopNodes)

-		{

-			List<GraphNode!>! exitnodes = new List<GraphNode!>();

-			

-			foreach (GraphNode! g in loopNodes)

-			{

-				foreach (GraphNode! s in g.Succecessors)

-				{

-					if (!loopNodes.Contains(s) /*&& !exitnodes.Contains(s)*/ ) exitnodes.Add(s);

-				}

-			}			

-			return exitnodes;

-		}

-		

-		private void AddHavocCmd(Block! b, List<GraphNode!>! loopNodes)

-		{

-			List<Block!>! loopBlocks = new List<Block!>();

-			foreach (GraphNode! g in loopNodes) loopBlocks.Add(g.Block);

-			HavocCmd! hcmd = HavocLoopTargets(loopBlocks,b.tok);

-			CmdSeq! body = new CmdSeq();

-			body.Add(hcmd);

-			body.AddRange(b.Cmds);

-			b.Cmds = body;

-		}

+        private void GatherLoopBodyNodes(GraphNode! current, GraphNode! cutPoint, List<GraphNode!>! loopNodes)

+        {

+            loopNodes.Add(current);

+            if (false) System.Diagnostics.Debugger.Break();

+            foreach (GraphNode! g in current.Predecessors)

+            {

+                if (cutPoint.firstPredecessor == g || g == cutPoint || loopNodes.Contains(g) ) continue;

+                GatherLoopBodyNodes(g, cutPoint, loopNodes);

+            }        

+        }

+        

+        private List<GraphNode!>! GatherLoopExitNodes(List<GraphNode!>! loopNodes)

+        {

+            List<GraphNode!>! exitnodes = new List<GraphNode!>();

+            

+            foreach (GraphNode! g in loopNodes)

+            {

+                foreach (GraphNode! s in g.Succecessors)

+                {

+                    if (!loopNodes.Contains(s) /*&& !exitnodes.Contains(s)*/ ) exitnodes.Add(s);

+                }

+            }            

+            return exitnodes;

+        }

+        

+        private void AddHavocCmd(Block! b, List<GraphNode!>! loopNodes)

+        {

+            List<Block!>! loopBlocks = new List<Block!>();

+            foreach (GraphNode! g in loopNodes) loopBlocks.Add(g.Block);

+            HavocCmd! hcmd = HavocLoopTargets(loopBlocks,b.tok);

+            CmdSeq! body = new CmdSeq();

+            body.Add(hcmd);

+            body.AddRange(b.Cmds);

+            b.Cmds = body;

+        }

 

-		private HavocCmd! HavocLoopTargets(List<Block!>! bl, IToken! tok)

-		{

-			VariableSeq varsToHavoc = new VariableSeq();

-			foreach ( Block! b in bl )

-			{

-				foreach ( Cmd! c in b.Cmds )

-				{

-					c.AddAssignedVariables(varsToHavoc);

-				}

-			}

-			IdentifierExprSeq havocExprs = new IdentifierExprSeq();

-			foreach ( Variable! v in varsToHavoc )

-			{

-				IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

-				if(!havocExprs.Has(ie))

-					havocExprs.Add(ie);

-			}

-			// pass the token of the enclosing loop header to the HavocCmd so we can reconstruct

-			// the source location for this later on

-			return new HavocCmd(tok,havocExprs);			

-		}    

-				

+        private HavocCmd! HavocLoopTargets(List<Block!>! bl, IToken! tok)

+        {

+            VariableSeq varsToHavoc = new VariableSeq();

+            foreach ( Block! b in bl )

+            {

+                foreach ( Cmd! c in b.Cmds )

+                {

+                    c.AddAssignedVariables(varsToHavoc);

+                }

+            }

+            IdentifierExprSeq havocExprs = new IdentifierExprSeq();

+            foreach ( Variable! v in varsToHavoc )

+            {

+                IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

+                if(!havocExprs.Has(ie))

+                    havocExprs.Add(ie);

+            }

+            // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct

+            // the source location for this later on

+            return new HavocCmd(tok,havocExprs);            

+        }    

+                

     #endregion

 

       

@@ -1009,7 +1009,7 @@ namespace VC
                 assume gcmd.labelTargets != null;

                 foreach (Block! succ in gcmd.labelTargets) 

                 {

-	                g.Succecessors.Add( ComputeGraphInfo(g, succ, gd, beingVisited) );

+                    g.Succecessors.Add( ComputeGraphInfo(g, succ, gd, beingVisited) );

                 }

               }

               beingVisited.Remove(b);

@@ -1020,148 +1020,135 @@ namespace VC
       }

       

     }

-    #endregion		

+    #endregion        

 

     #endregion 

      

     #region Program Passification

       private void GenerateReachVars(Implementation! impl)

       {

-	    Hashtable gotoCmdOrigins = new Hashtable();

-	    Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);

-	    AddBlocksBetween(impl);

-	    

+        Hashtable gotoCmdOrigins = new Hashtable();

+        Block! exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);

+        AddBlocksBetween(impl);

+        

         #region Insert pre- and post-conditions and where clauses as assume and assert statements

         {

-        CmdSeq cc = new CmdSeq();

-        // where clauses of global variables

-        foreach (Declaration d in program.TopLevelDeclarations) {

-          GlobalVariable gvar = d as GlobalVariable;

-          if (gvar != null && gvar.TypedIdent.WhereExpr != null) {

-            Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);

-            cc.Add(c);

+          CmdSeq cc = new CmdSeq();

+          // where clauses of global variables

+          foreach (Declaration d in program.TopLevelDeclarations) {

+            GlobalVariable gvar = d as GlobalVariable;

+            if (gvar != null && gvar.TypedIdent.WhereExpr != null) {

+              Cmd c = new AssumeCmd(gvar.tok, gvar.TypedIdent.WhereExpr);

+              cc.Add(c);

+            }

           }

-        }

-        // where clauses of in- and out-parameters

-        cc.AddRange( GetParamWhereClauses(impl));

-        // where clauses of local variables

-        foreach (Variable! lvar in impl.LocVars) {

-          if (lvar.TypedIdent.WhereExpr != null) {

-            Cmd c = new AssumeCmd(lvar.tok, lvar.TypedIdent.WhereExpr);

-            cc.Add(c);

+          // where clauses of in- and out-parameters

+          cc.AddRange( GetParamWhereClauses(impl));

+          // where clauses of local variables

+          foreach (Variable! lvar in impl.LocVars) {

+            if (lvar.TypedIdent.WhereExpr != null) {

+              Cmd c = new AssumeCmd(lvar.tok, lvar.TypedIdent.WhereExpr);

+              cc.Add(c);

+            }

           }

-        }

 

-        InjectPreconditions(impl);

-        //cc.AddRange(GetPre(impl));

+          // add cc and the preconditions to new blocks preceding impl.Blocks[0]

+          InjectPreconditions(impl, cc);

 

-        Block! entryBlock = (!) impl.Blocks[0];

-        cc.AddRange(entryBlock.Cmds);

-        entryBlock.Cmds = cc;

-          

-        InjectPostConditions(impl,exitBlock,gotoCmdOrigins);

-        //CmdSeq! post = GetPost(impl);

-        //exitBlock.Cmds.AddRange(post);

-        }

-        // Check If a new Unified Exit has been generated

-        GotoCmd gc = exitBlock.TransferCmd as GotoCmd;

-        if (gc!=null) {

-            assert gc.labelTargets !=null;

-            assert gc.labelTargets.Length==1;

-            assert gc.labelTargets[0]!=null;

-            exitBlock = (!)gc.labelTargets[0];

+          // append postconditions, starting in exitBlock and continuing into other blocks, if needed

+          exitBlock = InjectPostConditions(impl,exitBlock,gotoCmdOrigins);

         }

-        #endregion	    

-	    GenerateReachabilityPredicates(impl, exitBlock);      

+        #endregion        

+        GenerateReachabilityPredicates(impl, exitBlock);      

       }

     

     

       private Hashtable/*TransferCmd->ReturnCmd*/! PassifyProgram(Implementation! impl)

-	  {	    	    	    

-	    current_impl = impl;

-	    Convert2PassiveCmd(impl);

-	    impl = current_impl;

-	    return new Hashtable();

-	  }

+      {                        

+          current_impl = impl;

+          Convert2PassiveCmd(impl);

+          impl = current_impl;

+          return new Hashtable();

+      }

     

-    /// <summary>

-    /// Add additional variable to allow checking as described in the paper

-    /// "It's doomed; we can prove it"

-    /// </summary>

-    private void GenerateReachabilityPredicates(Implementation! impl, Block! exitBlock)

-    {

-			ExprSeq! es = new ExprSeq();

-			Cmd eblockcond = null;

-						

-			foreach (Block! b in impl.Blocks)

-			{

-				//if (b.Predecessors.Length==0) continue;

-				//if (b.Cmds.Length == 0 ) continue;

+      /// <summary>

+      /// Add additional variable to allow checking as described in the paper

+      /// "It's doomed; we can prove it"

+      /// </summary>

+      private void GenerateReachabilityPredicates(Implementation! impl, Block! exitBlock)

+      {

+          ExprSeq! es = new ExprSeq();

+          Cmd eblockcond = null;

+                      

+          foreach (Block! b in impl.Blocks)

+          {

+              //if (b.Predecessors.Length==0) continue;

+              //if (b.Cmds.Length == 0 ) continue;

 

-				Variable v_ = new LocalVariable(Token.NoToken, 

-										new TypedIdent(b.tok, b.Label+reachvarsuffix,new BasicType(SimpleType.Bool) ) );

-				

-				impl.LocVars.Add(v_);

-				

-				m_BlockReachabilityMap[b] = v_;

-				

-				IdentifierExpr! lhs =  new IdentifierExpr(b.tok, v_);

-				

-				es.Add( new IdentifierExpr(b.tok, v_) );

-				

-				List<AssignLhs!>! lhsl = new List<AssignLhs!>();

-				lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs) );

-				List<Expr!>! rhsl = new List<Expr!>();

-				rhsl.Add(Expr.True);

-				

-				if (b!=exitBlock)

-				{

-					CmdSeq cs = new CmdSeq(new AssignCmd(Token.NoToken, lhsl, rhsl));					

-					cs.AddRange(b.Cmds);

-					b.Cmds = cs;

-				} else

-				{				

-					eblockcond = new AssignCmd(Token.NoToken, lhsl, rhsl);

-				}

-				

-				//checkBlocks.Add(new CheckableBlock(v_,b));

-			}

-			if (es.Length==0) return;

+              Variable v_ = new LocalVariable(Token.NoToken, 

+                                      new TypedIdent(b.tok, b.Label+reachvarsuffix,new BasicType(SimpleType.Bool) ) );

+              

+              impl.LocVars.Add(v_);

+              

+              m_BlockReachabilityMap[b] = v_;

+              

+              IdentifierExpr! lhs =  new IdentifierExpr(b.tok, v_);

+              

+              es.Add( new IdentifierExpr(b.tok, v_) );

+              

+              List<AssignLhs!>! lhsl = new List<AssignLhs!>();

+              lhsl.Add(new SimpleAssignLhs(Token.NoToken, lhs) );

+              List<Expr!>! rhsl = new List<Expr!>();

+              rhsl.Add(Expr.True);

+              

+              if (b!=exitBlock)

+              {

+                  CmdSeq cs = new CmdSeq(new AssignCmd(Token.NoToken, lhsl, rhsl));                    

+                  cs.AddRange(b.Cmds);

+                  b.Cmds = cs;

+              } else

+              {                

+                  eblockcond = new AssignCmd(Token.NoToken, lhsl, rhsl);

+              }

+              

+              //checkBlocks.Add(new CheckableBlock(v_,b));

+          }

+          if (es.Length==0) return;

 

-			Expr aexp = null;

+          Expr aexp = null;

 

-			if (es.Length==1) 

-			{

-				aexp = es[0];			

-			} else if (es.Length==2)

-			{

-				aexp =  Expr.Binary(Token.NoToken,

-					BinaryOperator.Opcode.And,

-					(!)es[0],

-					(!)es[1]);

-			} else

-			{

-				aexp = Expr.True;

-				foreach (Expr e_ in es)

-				{

-					aexp = Expr.Binary(Token.NoToken, 

-						BinaryOperator.Opcode.And,

-						(!)e_, aexp);

-				}		

-			}

-			assert (aexp!=null);

-			assert (eblockcond!=null);

-			

-			AssumeCmd ac = new AssumeCmd(Token.NoToken, aexp);

-			

-			assert(exitBlock!=null);

+          if (es.Length==1) 

+          {

+              aexp = es[0];            

+          } else if (es.Length==2)

+          {

+              aexp =  Expr.Binary(Token.NoToken,

+                  BinaryOperator.Opcode.And,

+                  (!)es[0],

+                  (!)es[1]);

+          } else

+          {

+              aexp = Expr.True;

+              foreach (Expr e_ in es)

+              {

+                  aexp = Expr.Binary(Token.NoToken, 

+                      BinaryOperator.Opcode.And,

+                      (!)e_, aexp);

+              }        

+          }

+          assert (aexp!=null);

+          assert (eblockcond!=null);

+          

+          AssumeCmd ac = new AssumeCmd(Token.NoToken, aexp);

+          

+          assert(exitBlock!=null);

 

-			CmdSeq cseq = new CmdSeq(eblockcond);

-			cseq.AddRange(exitBlock.Cmds);		

-			cseq.Add(ac);

-			

-			exitBlock.Cmds = cseq;		      

-    }

+          CmdSeq cseq = new CmdSeq(eblockcond);

+          cseq.AddRange(exitBlock.Cmds);        

+          cseq.Add(ac);

+          

+          exitBlock.Cmds = cseq;              

+      }

     

     #endregion