CmdSeq: farewell

12 files changed, 103 insertions, 114 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 8654af37..8d68102a 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -604,19 +604,19 @@ namespace Microsoft.Boogie {
             }

           }

 

-          CmdSeq cmdSeq;

+          List<Cmd> cmdSeq;

           if (headRecursion)

-              cmdSeq = new CmdSeq();

+              cmdSeq = new List<Cmd>();

           else

           {

               CallCmd callCmd = (CallCmd)(loopHeaderToCallCmd2[header]).Clone();

               addUniqueCallAttr(si_unique_loc, callCmd);

               si_unique_loc++;

-              cmdSeq = new CmdSeq(callCmd);

+              cmdSeq = new List<Cmd> { callCmd };

           }

 

           Block/*!*/ block1 = new Block(Token.NoToken, source.Label + "_dummy",

-                              new CmdSeq(new AssumeCmd(Token.NoToken, Expr.False)), new ReturnCmd(Token.NoToken));

+                              new List<Cmd>{ new AssumeCmd(Token.NoToken, Expr.False) }, new ReturnCmd(Token.NoToken));

           Block/*!*/ block2 = new Block(Token.NoToken, block1.Label,

                               cmdSeq, new ReturnCmd(Token.NoToken));

           impl.Blocks.Add(block1);

@@ -639,7 +639,7 @@ namespace Microsoft.Boogie {
           blockMap[block1] = block2;

         }

         List<Block/*!*/>/*!*/ blocks = new List<Block/*!*/>();

-        Block exit = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken));

+        Block exit = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));

         GotoCmd cmd = new GotoCmd(Token.NoToken,

                                     new StringSeq(cce.NonNull(blockMap[header]).Label, exit.Label),

                                     new BlockSeq(blockMap[header], exit));

@@ -650,7 +650,7 @@ namespace Microsoft.Boogie {
                                     new BlockSeq(blockMap[header]));

 

         Block entry;

-        CmdSeq initCmds = new CmdSeq();

+        List<Cmd> initCmds = new List<Cmd>();

         if (loopHeaderToAssignCmd.ContainsKey(header)) {

             AssignCmd assignCmd = loopHeaderToAssignCmd[header];

             initCmds.Add(assignCmd);

@@ -700,7 +700,7 @@ namespace Microsoft.Boogie {
         string lastIterBlockName = header.Label + "_last";

         Block lastIterBlock = new Block(Token.NoToken, lastIterBlockName, header.Cmds, header.TransferCmd);

         newBlocksCreated[header] = lastIterBlock;

-        header.Cmds = new CmdSeq(loopHeaderToCallCmd1[header]);

+        header.Cmds = new List<Cmd> { loopHeaderToCallCmd1[header] };

         header.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(lastIterBlockName), new BlockSeq(lastIterBlock));

         impl.Blocks.Add(lastIterBlock);

         blockMap[origHeader] = blockMap[header];

@@ -821,7 +821,7 @@ namespace Microsoft.Boogie {
           gotoCmd.labelTargets.Remove(splitCandidate);

 

           CodeCopier codeCopier = new CodeCopier(new Hashtable(), new Hashtable());

-          CmdSeq newCmdSeq = codeCopier.CopyCmdSeq(splitCandidate.Cmds);

+          List<Cmd> newCmdSeq = codeCopier.CopyCmdSeq(splitCandidate.Cmds);

           TransferCmd newTransferCmd;

           GotoCmd splitGotoCmd = splitCandidate.TransferCmd as GotoCmd;

           if (splitGotoCmd == null) {

@@ -3234,17 +3234,6 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class CmdSeq : List<Cmd> {

-    public CmdSeq(params Cmd[]/*!*/ args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-    public CmdSeq(CmdSeq/*!*/ cmdSeq)

-      : base(cmdSeq) {

-      Contract.Requires(cmdSeq != null);

-    }

-  }

-

   public sealed class ExprSeq : List<Expr> {

     public ExprSeq(params Expr[]/*!*/ args)

       : base(args) {

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index ace4e7b6..a11d53a2 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -34,13 +34,13 @@ namespace Microsoft.Boogie {
     public readonly bool Anonymous;

 

     [Rep]

-    public CmdSeq/*!*/ simpleCmds;

+    public List<Cmd>/*!*/ simpleCmds;

     public StructuredCmd ec;

     public TransferCmd tc;

 

     public BigBlock successorBigBlock;  // null if successor is end of procedure body (or if field has not yet been initialized)

 

-    public BigBlock(IToken tok, string labelName, [Captured] CmdSeq simpleCmds, StructuredCmd ec, TransferCmd tc) {

+    public BigBlock(IToken tok, string labelName, [Captured] List<Cmd> simpleCmds, StructuredCmd ec, TransferCmd tc) {

       Contract.Requires(simpleCmds != null);

       Contract.Requires(tok != null);

       Contract.Requires(ec == null || tc == null);

@@ -75,7 +75,7 @@ namespace Microsoft.Boogie {
   public class StmtList {

     [Rep]

     public readonly List<BigBlock/*!*/>/*!*/ BigBlocks;

-    public CmdSeq PrefixCommands;

+    public List<Cmd> PrefixCommands;

     public readonly IToken/*!*/ EndCurly;

     public StmtList ParentContext;

     public BigBlock ParentBigBlock;

@@ -122,7 +122,7 @@ namespace Microsoft.Boogie {
     /// Note, to be conservative (that is, ignoring the possible optimization that this

     /// method enables), this method can do nothing and return false.

     /// </summary>

-    public bool PrefixFirstBlock([Captured] CmdSeq prefixCmds, ref string suggestedLabel) {

+    public bool PrefixFirstBlock([Captured] List<Cmd> prefixCmds, ref string suggestedLabel) {

       Contract.Requires(suggestedLabel != null);

       Contract.Requires(prefixCmds != null);

       Contract.Ensures(Contract.Result<bool>() || cce.Owner.None(prefixCmds));  // "prefixCmds" is captured only on success

@@ -162,7 +162,7 @@ namespace Microsoft.Boogie {
   public class StmtListBuilder {

     List<BigBlock/*!*/>/*!*/ bigBlocks = new List<BigBlock/*!*/>();

     string label;

-    CmdSeq simpleCmds;

+    List<Cmd> simpleCmds;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(bigBlocks));

@@ -175,7 +175,7 @@ namespace Microsoft.Boogie {
         // nothing to do

       } else {

         if (simpleCmds == null) {

-          simpleCmds = new CmdSeq();

+          simpleCmds = new List<Cmd>();

         }

         bigBlocks.Add(new BigBlock(Token.NoToken, label, simpleCmds, scmd, tcmd));

         label = null;

@@ -192,7 +192,7 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<StmtList>() != null);

       Dump(null, null);

       if (bigBlocks.Count == 0) {

-        simpleCmds = new CmdSeq();  // the StmtList constructor doesn't like an empty list of BigBlock's

+        simpleCmds = new List<Cmd>();  // the StmtList constructor doesn't like an empty list of BigBlock's

         Dump(null, null);

       }

       return new StmtList(bigBlocks, endCurlyBrace);

@@ -201,7 +201,7 @@ namespace Microsoft.Boogie {
     public void Add(Cmd cmd) {

       Contract.Requires(cmd != null);

       if (simpleCmds == null) {

-        simpleCmds = new CmdSeq();

+        simpleCmds = new List<Cmd>();

       }

       simpleCmds.Add(cmd);

     }

@@ -453,17 +453,17 @@ namespace Microsoft.Boogie {
     void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) {

       Contract.Requires(stmtList != null);

       Contract.Requires(blocks != null);

-      CmdSeq cmdPrefixToApply = stmtList.PrefixCommands;

+      List<Cmd> cmdPrefixToApply = stmtList.PrefixCommands;

 

       int n = stmtList.BigBlocks.Count;

       foreach (BigBlock b in stmtList.BigBlocks) {

         n--;

         Contract.Assert(b.LabelName != null);

-        CmdSeq theSimpleCmds;

+        List<Cmd> theSimpleCmds;

         if (cmdPrefixToApply == null) {

           theSimpleCmds = b.simpleCmds;

         } else {

-          theSimpleCmds = new CmdSeq();

+          theSimpleCmds = new List<Cmd>();

           theSimpleCmds.AddRange(cmdPrefixToApply);

           theSimpleCmds.AddRange(b.simpleCmds);

           cmdPrefixToApply = null;  // now, we've used 'em up

@@ -499,8 +499,8 @@ namespace Microsoft.Boogie {
           string loopDoneLabel = prefix + anon + "_LoopDone";

           anon++;

 

-          CmdSeq ssBody = new CmdSeq();

-          CmdSeq ssDone = new CmdSeq();

+          List<Cmd> ssBody = new List<Cmd>();

+          List<Cmd> ssDone = new List<Cmd>();

           if (wcmd.Guard != null) {

             var ac = new AssumeCmd(wcmd.tok, wcmd.Guard);

             ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List<object>(), null);

@@ -519,7 +519,7 @@ namespace Microsoft.Boogie {
           blocks.Add(block);

 

           // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody;

-          CmdSeq ssHead = new CmdSeq();

+          List<Cmd> ssHead = new List<Cmd>();

           foreach (PredicateCmd inv in wcmd.Invariants) {

             ssHead.Add(inv);

           }

@@ -549,7 +549,7 @@ namespace Microsoft.Boogie {
         } else {

           IfCmd ifcmd = (IfCmd)b.ec;

           string predLabel = b.LabelName;

-          CmdSeq predCmds = theSimpleCmds;

+          List<Cmd> predCmds = theSimpleCmds;

 

           for (; ifcmd != null; ifcmd = ifcmd.elseIf) {

             string thenLabel = prefix + anon + "_Then";

@@ -558,8 +558,8 @@ namespace Microsoft.Boogie {
             Contract.Assert(elseLabel != null);

             anon++;

 

-            CmdSeq ssThen = new CmdSeq();

-            CmdSeq ssElse = new CmdSeq();

+            List<Cmd> ssThen = new List<Cmd>();

+            List<Cmd> ssElse = new List<Cmd>();

             if (ifcmd.Guard != null) {

               var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard);

               ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);

@@ -605,7 +605,7 @@ namespace Microsoft.Boogie {
             } else if (ifcmd.elseIf != null) {

               // this is an "else if"

               predLabel = elseLabel;

-              predCmds = new CmdSeq();

+              predCmds = new List<Cmd>();

               if (ifcmd.Guard != null) {

                 var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard));

                 ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);

@@ -796,7 +796,7 @@ namespace Microsoft.Boogie {
     public string/*!*/ Label;  // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal

     [Rep]

     [ElementsPeer]

-    public CmdSeq/*!*/ Cmds;

+    public List<Cmd>/*!*/ Cmds;

     [Rep]  //PM: needed to verify Traverse.Visit

     public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)

 

@@ -837,11 +837,11 @@ namespace Microsoft.Boogie {
     }

 

     public Block()

-      : this(Token.NoToken, "", new CmdSeq(), new ReturnCmd(Token.NoToken)) {

+      : this(Token.NoToken, "", new List<Cmd>(), new ReturnCmd(Token.NoToken)) {

 

     }

 

-    public Block(IToken tok, string/*!*/ label, CmdSeq/*!*/ cmds, TransferCmd transferCmd)

+    public Block(IToken tok, string/*!*/ label, List<Cmd>/*!*/ cmds, TransferCmd transferCmd)

       : base(tok) {

       Contract.Requires(label != null);

       Contract.Requires(cmds != null);

@@ -1536,9 +1536,9 @@ namespace Microsoft.Boogie {
     }

 

     public /*readonly, except for the StandardVisitor*/ List<Variable>/*!*/ Locals;

-    public /*readonly, except for the StandardVisitor*/ CmdSeq/*!*/ Cmds;

+    public /*readonly, except for the StandardVisitor*/ List<Cmd>/*!*/ Cmds;

 

-    public StateCmd(IToken tok, List<Variable>/*!*/ locals, CmdSeq/*!*/ cmds)

+    public StateCmd(IToken tok, List<Variable>/*!*/ locals, List<Cmd>/*!*/ cmds)

       : base(tok) {

       Contract.Requires(locals != null);

       Contract.Requires(cmds != null);

@@ -2033,7 +2033,7 @@ namespace Microsoft.Boogie {
 

     protected override Cmd ComputeDesugaring() {

       Contract.Ensures(Contract.Result<Cmd>() != null);

-      CmdSeq newBlockBody = new CmdSeq();

+      List<Cmd> newBlockBody = new List<Cmd>();

       Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();

       Dictionary<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>();

       Dictionary<Variable, Expr> substMapBound = new Dictionary<Variable, Expr>();

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index 4b20e4a7..a8a03567 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -84,7 +84,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)
   Pgm = new Program();

   dummyExpr = new LiteralExpr(Token.NoToken, false);

   dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);

-  dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(), new ReturnCmd(Token.NoToken));

+  dummyBlock = new Block(Token.NoToken, "dummyBlock", new List<Cmd>(), new ReturnCmd(Token.NoToken));

   dummyType = new BasicType(Token.NoToken, SimpleType.Bool);

   dummyExprSeq = new ExprSeq ();

   dummyTransferCmd = new ReturnCmd(Token.NoToken);

@@ -681,7 +681,7 @@ StmtList<out StmtList/*!*/ stmtList>
 = (. Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); List<BigBlock/*!*/> bigblocks = new List<BigBlock/*!*/>();

      /* built-up state for the current BigBlock: */

      IToken startToken = null;  string currentLabel = null;

-     CmdSeq cs = null;  /* invariant: startToken != null ==> cs != null */

+     List<Cmd> cs = null;  /* invariant: startToken != null ==> cs != null */

      /* temporary variables: */

      IToken label;  Cmd c;  BigBlock b;

      StructuredCmd ec = null;  StructuredCmd/*!*/ ecn;

@@ -693,7 +693,7 @@ StmtList<out StmtList/*!*/ stmtList>
     (. if (c != null) {

          // LabelOrCmd read a Cmd

          Contract.Assert(label == null);

-         if (startToken == null) { startToken = c.tok;  cs = new CmdSeq(); }

+         if (startToken == null) { startToken = c.tok;  cs = new List<Cmd>(); }

          Contract.Assert(cs != null);

          cs.Add(c);

        } else {

@@ -708,13 +708,13 @@ StmtList<out StmtList/*!*/ stmtList>
          }

          startToken = label;

          currentLabel = label.val;

-         cs = new CmdSeq();

+         cs = new List<Cmd>();

        }

     .)

 

   | StructuredCmd<out ecn>

     (. ec = ecn;

-       if (startToken == null) { startToken = ec.tok;  cs = new CmdSeq(); }

+       if (startToken == null) { startToken = ec.tok;  cs = new List<Cmd>(); }

        Contract.Assert(cs != null);

        b = new BigBlock(startToken, currentLabel, cs, ec, null);

        bigblocks.Add(b);

@@ -723,7 +723,7 @@ StmtList<out StmtList/*!*/ stmtList>
 

   | TransferCmd<out tcn>

     (. tc = tcn;

-       if (startToken == null) { startToken = tc.tok;  cs = new CmdSeq(); }

+       if (startToken == null) { startToken = tc.tok;  cs = new List<Cmd>(); }

        Contract.Assert(cs != null);

        b = new BigBlock(startToken, currentLabel, cs, null, tc);

        bigblocks.Add(b);

@@ -735,7 +735,7 @@ StmtList<out StmtList/*!*/ stmtList>
   "}"

   (. IToken/*!*/ endCurly = t;

      if (startToken == null && bigblocks.Count == 0) {

-       startToken = t;  cs = new CmdSeq();

+       startToken = t;  cs = new List<Cmd>();

      }

      if (startToken != null) {

        Contract.Assert(cs != null);

@@ -1314,7 +1314,7 @@ CodeExpression<.out List<Variable>/*!*/ locals, out List<Block/*!*/>/*!*/ blocks
 SpecBlock<out Block/*!*/ b>

 = (. Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y;

      Cmd c;  IToken label;

-     CmdSeq cs = new CmdSeq();

+     List<Cmd> cs = new List<Cmd>();

      List<IToken>/*!*/ xs;

      StringSeq ss = new StringSeq();

      b = dummyBlock;

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 62dfa03f..356ff272 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -388,7 +388,7 @@ namespace Microsoft.Boogie {
           }

         }

 

-        CmdSeq cmds = block.Cmds;

+        List<Cmd> cmds = block.Cmds;

         int len = cmds.Count;

         for (int i = len - 1; i >= 0; i--) {

           if (cmds[i] is CallCmd) {

@@ -469,7 +469,7 @@ namespace Microsoft.Boogie {
         Propagate(sugCmd.Desugaring, liveSet);

       } else if (cmd is StateCmd) {

         StateCmd/*!*/ stCmd = (StateCmd)cce.NonNull(cmd);

-        CmdSeq/*!*/ cmds = cce.NonNull(stCmd.Cmds);

+        List<Cmd>/*!*/ cmds = cce.NonNull(stCmd.Cmds);

         int len = cmds.Count;

         for (int i = len - 1; i >= 0; i--) {

           Propagate(cmds[i], liveSet);

@@ -1461,7 +1461,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
       } else if (cmd is StateCmd) {

         StateCmd/*!*/ stCmd = (StateCmd)cmd;

         Contract.Assert(stCmd != null);

-        CmdSeq/*!*/ cmds = stCmd.Cmds;

+        List<Cmd>/*!*/ cmds = stCmd.Cmds;

         Contract.Assert(cmds != null);

         int len = cmds.Count;

         ret = GenKillWeight.one();

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 019711e7..e59dd27e 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -118,9 +118,9 @@ namespace Microsoft.Boogie {
       Contract.Ensures(Contract.Result<Choice>() != null);

       return base.VisitChoice((Choice)node.Clone());

     }

-    public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {

+    public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {

       //Contract.Requires(cmdSeq != null);

-      Contract.Ensures(Contract.Result<CmdSeq>() != null);

+      Contract.Ensures(Contract.Result<List<Cmd>>() != null);

       return base.VisitCmdSeq(cmdSeq);

     }

     public override Constant VisitConstant(Constant node) {

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 07c44bac..0d412fbc 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -220,8 +220,8 @@ namespace Microsoft.Boogie {
       

       foreach (Block block in blocks) {

         TransferCmd/*!*/ transferCmd = cce.NonNull(block.TransferCmd);

-        CmdSeq cmds = block.Cmds;

-        CmdSeq newCmds = new CmdSeq();

+        List<Cmd> cmds = block.Cmds;

+        List<Cmd> newCmds = new List<Cmd>();

         Block newBlock;

         string label = block.Label;

         int lblCount = 0;

@@ -296,7 +296,7 @@ namespace Microsoft.Boogie {
               newBlocks.AddRange(inlinedBlocks);

 

               lblCount = nextlblCount;

-              newCmds = new CmdSeq();

+              newCmds = new List<Cmd>();

             } else if (inline == 0) {

               inlinedSomething = true;

               if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) {

@@ -413,8 +413,8 @@ namespace Microsoft.Boogie {
       }

     }

 

-    private CmdSeq RemoveAsserts(CmdSeq cmds) {

-      CmdSeq newCmdSeq = new CmdSeq();

+    private List<Cmd> RemoveAsserts(List<Cmd> cmds) {

+      List<Cmd> newCmdSeq = new List<Cmd>();

       for (int i = 0; i < cmds.Count; i++) {

         Cmd cmd = cmds[i];

         if (cmd is AssertCmd) continue;

@@ -442,7 +442,7 @@ namespace Microsoft.Boogie {
       List<Block/*!*/>/*!*/ inlinedBlocks = new List<Block/*!*/>();

 

       // create in block

-      CmdSeq inCmds = new CmdSeq();

+      List<Cmd> inCmds = new List<Cmd>();

 

       // assign in parameters

       for (int i = 0; i < impl.InParams.Count; ++i) {

@@ -516,7 +516,7 @@ namespace Microsoft.Boogie {
       // inject the blocks of the implementation

       Block intBlock;

       foreach (Block block in implBlocks) {

-        CmdSeq copyCmds = codeCopier.CopyCmdSeq(block.Cmds);

+        List<Cmd> copyCmds = codeCopier.CopyCmdSeq(block.Cmds);

         if (0 <= inlineDepth) {

           copyCmds = RemoveAsserts(copyCmds);

         }

@@ -526,7 +526,7 @@ namespace Microsoft.Boogie {
       }

 

       // create out block

-      CmdSeq outCmds = new CmdSeq();

+      List<Cmd> outCmds = new List<Cmd>();

 

       // inject ensures

       for (int i = 0; i < proc.Ensures.Count; i++) {

@@ -603,10 +603,10 @@ namespace Microsoft.Boogie {
     public CodeCopier() {

     }

 

-    public CmdSeq CopyCmdSeq(CmdSeq cmds) {

+    public List<Cmd> CopyCmdSeq(List<Cmd> cmds) {

       Contract.Requires(cmds != null);

-      Contract.Ensures(Contract.Result<CmdSeq>() != null);

-      CmdSeq newCmds = new CmdSeq();

+      Contract.Ensures(Contract.Result<List<Cmd>>() != null);

+      List<Cmd> newCmds = new List<Cmd>();

       foreach (Cmd/*!*/ cmd in cmds) {

         Contract.Assert(cmd != null);

         newCmds.Add(CopyCmd(cmd));

diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs
index e103c628..eb34065f 100644
--- a/Source/Core/InterProceduralReachabilityGraph.cs
+++ b/Source/Core/InterProceduralReachabilityGraph.cs
@@ -122,7 +122,7 @@ namespace Microsoft.Boogie
       {

         if (!newProcedureEntryNodes.ContainsKey(proc.Name))

         {

-          Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new CmdSeq(), new GotoCmd(Token.NoToken, new BlockSeq()));

+          Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new List<Cmd>(), new GotoCmd(Token.NoToken, new BlockSeq()));

           nodes.Add(newBlock);

           newProcedureEntryNodes[proc.Name] = newBlock;

           newProcedureExitNodes[proc.Name] = newBlock;

@@ -137,7 +137,7 @@ namespace Microsoft.Boogie
       foreach (var impl in prog.TopLevelDeclarations.OfType<Implementation>())

       {

         string exitLabel = "__" + impl.Name + "_newExit";

-        Block newExit = new Block(Token.NoToken, exitLabel, new CmdSeq(), new GotoCmd(Token.NoToken, new BlockSeq()));

+        Block newExit = new Block(Token.NoToken, exitLabel, new List<Cmd>(), new GotoCmd(Token.NoToken, new BlockSeq()));

         nodes.Add(newExit);

         newProcedureExitNodes[impl.Name] = newExit;

         foreach (Block b in impl.Blocks)

@@ -150,7 +150,7 @@ namespace Microsoft.Boogie
             Block newBlock;

             if (prev == null)

             {

-              newBlock = new Block(b.tok, "__" + impl.Name + "_" + b.Label, new CmdSeq(cmds.ToArray()), null);

+              newBlock = new Block(b.tok, "__" + impl.Name + "_" + b.Label, new List<Cmd>(cmds.ToArray()), null);

               nodes.Add(newBlock);

               originalToNew[b] = newBlock;

               if (impl.Blocks[0] == b)

@@ -161,7 +161,7 @@ namespace Microsoft.Boogie
             else

             {

               string label = "__" + impl.Name + "_" + b.Label + "_call_" + i;

-              newBlock = new Block(b.tok, label, new CmdSeq(cmds.ToArray()), null);

+              newBlock = new Block(b.tok, label, new List<Cmd>(cmds.ToArray()), null);

               nodes.Add(newBlock);

               originalToNew[newBlock] = newBlock;

               prev.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq { label }, new BlockSeq { newBlock });

@@ -190,7 +190,7 @@ namespace Microsoft.Boogie
       #endregion

     }

 

-    private List<List<Cmd>> PartitionCmds(CmdSeq cmds) {

+    private List<List<Cmd>> PartitionCmds(List<Cmd> cmds) {

       List<List<Cmd>> result = new List<List<Cmd>>();

       List<Cmd> current = new List<Cmd>();

       result.Add(current);

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index 957718fa..00caea52 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -365,7 +365,7 @@ namespace Microsoft.Boogie
             return base.VisitCallCmd(node);

         }

 

-        private void AddDisjointnessExpr(CmdSeq newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)

+        private void AddDisjointnessExpr(List<Cmd> newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)

         {

             Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();

             foreach (var domainName in linearDomains.Keys)

@@ -412,7 +412,7 @@ namespace Microsoft.Boogie
 

                 foreach (Block b in impl.Blocks)

                 {

-                    CmdSeq newCmds = new CmdSeq();

+                    List<Cmd> newCmds = new List<Cmd>();

                     for (int i = 0; i < b.Cmds.Count; i++)

                     {

                         Cmd cmd = b.Cmds[i];

@@ -478,7 +478,7 @@ namespace Microsoft.Boogie
                     {

                         foreach (Block header in g.Headers)

                         {

-                            CmdSeq newCmds = new CmdSeq();

+                            List<Cmd> newCmds = new List<Cmd>();

                             AddDisjointnessExpr(newCmds, header, domainNameToInputVar);

                             newCmds.AddRange(header.Cmds);

                             header.Cmds = newCmds;

diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs
index 249e4249..a67f23f7 100644
--- a/Source/Core/LoopUnroll.cs
+++ b/Source/Core/LoopUnroll.cs
@@ -70,7 +70,7 @@ namespace Microsoft.Boogie {
 

     class GraphNode {

       public readonly Block/*!*/ Block;

-      public readonly CmdSeq/*!*/ Body;

+      public readonly List<Cmd>/*!*/ Body;

       [ContractInvariantMethod]

       void ObjectInvariant() {

         Contract.Invariant(Block != null);

@@ -94,16 +94,16 @@ namespace Microsoft.Boogie {
       [Rep]

       public readonly List<GraphNode/*!*/>/*!*/ Predecessors = new List<GraphNode/*!*/>();

 

-      GraphNode(Block b, CmdSeq body) {

+      GraphNode(Block b, List<Cmd> body) {

         Contract.Requires(body != null);

         Contract.Requires(b != null);

         this.Block = b;

         this.Body = body;

       }

 

-      static CmdSeq GetOptimizedBody(CmdSeq cmds) {

+      static List<Cmd> GetOptimizedBody(List<Cmd> cmds) {

         Contract.Requires(cmds != null);

-        Contract.Ensures(Contract.Result<CmdSeq>() != null);

+        Contract.Ensures(Contract.Result<List<Cmd>>() != null);

         int n = 0;

         foreach (Cmd c in cmds) {

           n++;

@@ -114,7 +114,7 @@ namespace Microsoft.Boogie {
             for (int i = 0; i < n; i++) {

               s[i] = cmds[i];

             }

-            return new CmdSeq(s);

+            return new List<Cmd>(s);

           }

         }

         return cmds;

@@ -140,7 +140,7 @@ namespace Microsoft.Boogie {
           }

 

         } else {

-          CmdSeq body = GetOptimizedBody(b.Cmds);

+          List<Cmd> body = GetOptimizedBody(b.Cmds);

           g = new GraphNode(b, body);

           gd.Add(b, g);

           if (from != null) {

@@ -224,13 +224,13 @@ namespace Microsoft.Boogie {
         Contract.Assert(nw != null);

 

       } else {

-        CmdSeq body;

+        List<Cmd> body;

         TransferCmd tcmd;

         Contract.Assert(orig.TransferCmd != null);

 

         if (next == null && node.IsCutPoint) {

           // as the body, use the assert/assume commands that make up the loop invariant

-          body = new CmdSeq();

+          body = new List<Cmd>();

           foreach (Cmd/*!*/ c in node.Body) {

             Contract.Assert(c != null);

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

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index cbaff3ef..1d0eb0fd 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -180,7 +180,7 @@ namespace Microsoft.Boogie
             yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));

         }

 

-        private void AddCallToYieldProc(CmdSeq newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)

+        private void AddCallToYieldProc(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)

         {

             ExprSeq exprSeq = new ExprSeq();

             foreach (string domainName in linearTypechecker.linearDomains.Keys)

@@ -213,7 +213,7 @@ namespace Microsoft.Boogie
             return domainNameToExpr;

         }

 

-        private void AddUpdatesToOldGlobalVars(CmdSeq newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<string, Expr> domainNameToExpr)

+        private void AddUpdatesToOldGlobalVars(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<string, Expr> domainNameToExpr)

         {

             List<AssignLhs> lhss = new List<AssignLhs>();

             List<Expr> rhss = new List<Expr>();

@@ -233,7 +233,7 @@ namespace Microsoft.Boogie
             }

         }

 

-        private void DesugarYield(YieldCmd yieldCmd, CmdSeq cmds, CmdSeq newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)

+        private void DesugarYield(YieldCmd yieldCmd, List<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)

         {

             AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);

 

@@ -317,7 +317,7 @@ namespace Microsoft.Boogie
             return proc;

         }

 

-        private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, Dictionary<Variable, Expr> map)

+        private void CreateYieldCheckerImpl(DeclWithFormals decl, List<List<Cmd>> yields, Dictionary<Variable, Expr> map)

         {

             if (yields.Count == 0) return;

 

@@ -373,15 +373,15 @@ namespace Microsoft.Boogie
             List<Block> yieldCheckerBlocks = new List<Block>();

             StringSeq labels = new StringSeq();

             BlockSeq labelTargets = new BlockSeq();

-            Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken));

+            Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));

             labels.Add(yieldCheckerBlock.Label);

             labelTargets.Add(yieldCheckerBlock);

             yieldCheckerBlocks.Add(yieldCheckerBlock);

             int yieldCount = 0;

-            foreach (CmdSeq cs in yields)

+            foreach (List<Cmd> cs in yields)

             {

                 var linearDomains = linearTypechecker.linearDomains;

-                CmdSeq newCmds = new CmdSeq();

+                List<Cmd> newCmds = new List<Cmd>();

                 foreach (Cmd cmd in cs)

                 {

                     PredicateCmd predCmd = (PredicateCmd)cmd;

@@ -402,7 +402,7 @@ namespace Microsoft.Boogie
                 labelTargets.Add(yieldCheckerBlock);

                 yieldCheckerBlocks.Add(yieldCheckerBlock);

             }

-            yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), new GotoCmd(Token.NoToken, labels, labelTargets)));

+            yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets)));

 

             // Create the yield checker procedure

             var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name);

@@ -452,12 +452,12 @@ namespace Microsoft.Boogie
             }

 

             // Collect the yield predicates and desugar yields

-            List<CmdSeq> yields = new List<CmdSeq>();

-            CmdSeq cmds = new CmdSeq();

+            List<List<Cmd>> yields = new List<List<Cmd>>();

+            List<Cmd> cmds = new List<Cmd>();

             foreach (Block b in impl.Blocks)

             {

                 YieldCmd yieldCmd = null;

-                CmdSeq newCmds = new CmdSeq();

+                List<Cmd> newCmds = new List<Cmd>();

                 for (int i = 0; i < b.Cmds.Count; i++)

                 {

                     Cmd cmd = b.Cmds[i];

@@ -475,7 +475,7 @@ namespace Microsoft.Boogie
                             if (cmds.Count > 0)

                             {

                                 yields.Add(cmds);

-                                cmds = new CmdSeq();

+                                cmds = new List<Cmd>();

                             }

                             yieldCmd = null;

                         }

@@ -538,7 +538,7 @@ namespace Microsoft.Boogie
                     if (cmds.Count > 0)

                     {

                         yields.Add(cmds);

-                        cmds = new CmdSeq();

+                        cmds = new List<Cmd>();

                     }

                 }

                 if (b.TransferCmd is ReturnCmd && (!info.isAtomic || info.isEntrypoint || info.isThreadStart))

@@ -565,7 +565,7 @@ namespace Microsoft.Boogie
                             AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);

                             AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

                         }

-                        CmdSeq newCmds = new CmdSeq();

+                        List<Cmd> newCmds = new List<Cmd>();

                         foreach (string domainName in linearTypechecker.linearDomains.Keys)

                         {

                             newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));

@@ -611,7 +611,7 @@ namespace Microsoft.Boogie
                 } 

                 if (lhss.Count > 0)

                 {

-                    Block initBlock = new Block(Token.NoToken, "og_init", new CmdSeq(new AssignCmd(Token.NoToken, lhss, rhss)), new GotoCmd(Token.NoToken, new StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0])));

+                    Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0])));

                     impl.Blocks.Insert(0, initBlock);

                 }

             }

@@ -637,8 +637,8 @@ namespace Microsoft.Boogie
             }

 

             // Collect the yield predicates and desugar yields

-            List<CmdSeq> yields = new List<CmdSeq>();

-            CmdSeq cmds = new CmdSeq();

+            List<List<Cmd>> yields = new List<List<Cmd>>();

+            List<Cmd> cmds = new List<Cmd>();

             if (proc.Requires.Count > 0)

             {

                 Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();

@@ -676,7 +676,7 @@ namespace Microsoft.Boogie
                     }

                 }

                 yields.Add(cmds);

-                cmds = new CmdSeq();

+                cmds = new List<Cmd>();

             }

             if (info.inParallelCall && proc.Ensures.Count > 0)

             {

@@ -715,7 +715,7 @@ namespace Microsoft.Boogie
                     }

                 }

                 yields.Add(cmds);

-                cmds = new CmdSeq();

+                cmds = new List<Cmd>();

             }

             CreateYieldCheckerImpl(proc, yields, new Dictionary<Variable, Expr>());

         }

@@ -752,14 +752,14 @@ namespace Microsoft.Boogie
                     CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List<IdentifierExpr>());

                     callCmd.Proc = proc;

                     string label = string.Format("L_{0}", labelCount++);

-                    Block block = new Block(Token.NoToken, label, new CmdSeq(callCmd), new ReturnCmd(Token.NoToken));

+                    Block block = new Block(Token.NoToken, label, new List<Cmd> { callCmd }, new ReturnCmd(Token.NoToken));

                     labelTargets.Add(label);

                     blockTargets.Add(block);

                     blocks.Add(block);

                 }

                 transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets);

             }

-            blocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), transferCmd));

+            blocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), transferCmd));

             

             var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new TypeVariableSeq(), inputs, new List<Variable>(), new List<Variable>(), blocks);

             yieldImpl.Proc = yieldProc;

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index b0ce346a..bcdd01d8 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -104,7 +104,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation)
   Pgm = new Program();

   dummyExpr = new LiteralExpr(Token.NoToken, false);

   dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);

-  dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(), new ReturnCmd(Token.NoToken));

+  dummyBlock = new Block(Token.NoToken, "dummyBlock", new List<Cmd>(), new ReturnCmd(Token.NoToken));

   dummyType = new BasicType(Token.NoToken, SimpleType.Bool);

   dummyExprSeq = new ExprSeq ();

   dummyTransferCmd = new ReturnCmd(Token.NoToken);

@@ -924,7 +924,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); List<BigBlock/*!*/> bigblocks = new List<BigBlock/*!*/>();

 		/* built-up state for the current BigBlock: */

 		IToken startToken = null;  string currentLabel = null;

-		CmdSeq cs = null;  /* invariant: startToken != null ==> cs != null */

+		List<Cmd> cs = null;  /* invariant: startToken != null ==> cs != null */

 		/* temporary variables: */

 		IToken label;  Cmd c;  BigBlock b;

 		StructuredCmd ec = null;  StructuredCmd/*!*/ ecn;

@@ -936,7 +936,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 				if (c != null) {

 				 // LabelOrCmd read a Cmd

 				 Contract.Assert(label == null);

-				 if (startToken == null) { startToken = c.tok;  cs = new CmdSeq(); }

+				 if (startToken == null) { startToken = c.tok;  cs = new List<Cmd>(); }

 				 Contract.Assert(cs != null);

 				 cs.Add(c);

 				} else {

@@ -951,13 +951,13 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 				 }

 				 startToken = label;

 				 currentLabel = label.val;

-				 cs = new CmdSeq();

+				 cs = new List<Cmd>();

 				}

 				

 			} else if (la.kind == 40 || la.kind == 42 || la.kind == 45) {

 				StructuredCmd(out ecn);

 				ec = ecn;

-				if (startToken == null) { startToken = ec.tok;  cs = new CmdSeq(); }

+				if (startToken == null) { startToken = ec.tok;  cs = new List<Cmd>(); }

 				Contract.Assert(cs != null);

 				b = new BigBlock(startToken, currentLabel, cs, ec, null);

 				bigblocks.Add(b);

@@ -966,7 +966,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 			} else {

 				TransferCmd(out tcn);

 				tc = tcn;

-				if (startToken == null) { startToken = tc.tok;  cs = new CmdSeq(); }

+				if (startToken == null) { startToken = tc.tok;  cs = new List<Cmd>(); }

 				Contract.Assert(cs != null);

 				b = new BigBlock(startToken, currentLabel, cs, null, tc);

 				bigblocks.Add(b);

@@ -977,7 +977,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 		Expect(28);

 		IToken/*!*/ endCurly = t;

 		if (startToken == null && bigblocks.Count == 0) {

-		 startToken = t;  cs = new CmdSeq();

+		 startToken = t;  cs = new List<Cmd>();

 		}

 		if (startToken != null) {

 		 Contract.Assert(cs != null);

@@ -1924,7 +1924,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 	void SpecBlock(out Block/*!*/ b) {

 		Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y;

 		Cmd c;  IToken label;

-		CmdSeq cs = new CmdSeq();

+		List<Cmd> cs = new List<Cmd>();

 		List<IToken>/*!*/ xs;

 		StringSeq ss = new StringSeq();

 		b = dummyBlock;

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 8f5cf64b..987eadb8 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -168,9 +168,9 @@ namespace Microsoft.Boogie {
           node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(node.Outs[i]));

       return node;

     }

-    public virtual CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {

+    public virtual List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {

       Contract.Requires(cmdSeq != null);

-      Contract.Ensures(Contract.Result<CmdSeq>() != null);

+      Contract.Ensures(Contract.Result<List<Cmd>>() != null);

       for (int i = 0, n = cmdSeq.Count; i < n; i++)

         cmdSeq[i] = (Cmd)this.Visit(cce.NonNull(cmdSeq[i])); // call general Visit so subtypes of Cmd get visited by their particular visitor

       return cmdSeq;