CmdSeq: farewell

4 files changed, 39 insertions, 39 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 6137678b..43627c5f 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -690,10 +690,10 @@ namespace VC {
       return;

     }

 

-    private static void AddAsPrefix(Block b, CmdSeq cs) {

+    private static void AddAsPrefix(Block b, List<Cmd> cs) {

       Contract.Requires(b != null);

       Contract.Requires(cs != null);

-      CmdSeq newCommands = new CmdSeq();

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

       newCommands.AddRange(cs);

       newCommands.AddRange(b.Cmds);

       b.Cmds = newCommands;

@@ -707,7 +707,7 @@ namespace VC {
     /// </summary>

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

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

-    protected static void InjectPreconditions(Implementation impl, [Captured] CmdSeq startCmds) {

+    protected static void InjectPreconditions(Implementation impl, [Captured] List<Cmd> startCmds) {

       Contract.Requires(impl != null);

       Contract.Requires(startCmds != null);

       Contract.Requires(impl.Proc != null);

@@ -802,7 +802,7 @@ namespace VC {
             // Here goes:  First, create the new block, which will become the new insertion

             // point and which will serve as a target for the CodeExpr.  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);

+            Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new List<Cmd>(), insertionPoint.TransferCmd);

             k++;

             // Second, append the CodeExpr blocks to the implementation's blocks

             ThreadInCodeExpr(impl, nextIP, be, true, debugWriter);

@@ -827,10 +827,10 @@ namespace VC {
     /// Get the pre-condition of an implementation, including the where clauses from the in-parameters.

     /// </summary>

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

-    protected static CmdSeq GetPre(Implementation impl) {

+    protected static List<Cmd> GetPre(Implementation impl) {

       Contract.Requires(impl != null);

       Contract.Requires(impl.Proc != null);

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

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

 

 

       TokenTextWriter debugWriter = null;

@@ -840,7 +840,7 @@ namespace VC {
       }

 

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

-      CmdSeq pre = new CmdSeq();

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

 

       // (free and checked) requires clauses

       foreach (Requires req in impl.Proc.Requires) {

@@ -867,19 +867,19 @@ namespace VC {
     /// Get the post-condition of an implementation.

     /// </summary>

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

-    protected static CmdSeq GetPost(Implementation impl) {

+    protected static List<Cmd> GetPost(Implementation impl) {

 

 

       Contract.Requires(impl != null);

       Contract.Requires(impl.Proc != null);

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

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

       if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

         Console.WriteLine("Effective postcondition:");

       }

 

       // Construct an Expr for the post-condition

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

-      CmdSeq post = new CmdSeq();

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

       foreach (Ensures ens in impl.Proc.Ensures) {

         Contract.Assert(ens != null);

         if (!ens.Free) {

@@ -910,10 +910,10 @@ namespace VC {
     /// As a side effect, this method adds these where clauses to the out parameters.

     /// </summary>

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

-    protected static CmdSeq GetParamWhereClauses(Implementation impl) {

+    protected static List<Cmd> GetParamWhereClauses(Implementation impl) {

       Contract.Requires(impl != null);

       Contract.Requires(impl.Proc != null);

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

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

       TokenTextWriter debugWriter = null;

       if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

         debugWriter = new TokenTextWriter("<console>", Console.Out, false);

@@ -921,7 +921,7 @@ namespace VC {
       }

 

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

-      CmdSeq whereClauses = new CmdSeq();

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

 

       // where clauses of in-parameters

       foreach (Formal f in impl.Proc.InParams) {

@@ -1104,7 +1104,7 @@ namespace VC {
         }

         if (returnBlocks > 1) {

           string unifiedExitLabel = "GeneratedUnifiedExit";

-          Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new CmdSeq(), new ReturnCmd(Token.NoToken));

+          Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(Token.NoToken));

           Contract.Assert(unifiedExit != null);

           foreach (Block b in impl.Blocks) {

             if (b.TransferCmd is ReturnCmd) {

@@ -1289,7 +1289,7 @@ namespace VC {
       Contract.Requires(oldFrameSubst != null);

       #region Walk forward over the commands in this block and convert them to passive commands

 

-      CmdSeq passiveCmds = new CmdSeq();

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

       foreach (Cmd c in b.Cmds) {

         Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction

         TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);

@@ -1413,7 +1413,7 @@ namespace VC {
     /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc

     /// Meanwhile, record any information needed to later reconstruct a model view.

     /// </summary>

-    protected void TurnIntoPassiveCmd(Cmd c, Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) {

+    protected void TurnIntoPassiveCmd(Cmd c, Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst, List<Cmd> passiveCmds, ModelViewInfo mvInfo) {

       Contract.Requires(c != null);

       Contract.Requires(incarnationMap != null);

       Contract.Requires(oldFrameSubst != null);

@@ -1627,7 +1627,7 @@ namespace VC {
       Block newBlock = new Block(

           new Token(-17, -4),

           newBlockLabel,

-          new CmdSeq(),

+          new List<Cmd>(),

           new GotoCmd(Token.NoToken, ls, bs)

           );

 

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 59e2ca9e..5a6ae6d3 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -242,7 +242,7 @@ namespace Microsoft.Boogie
 

             Expr invarExpr = new NAryExpr(Token.NoToken, new FunctionCall(function), exprs);

             var invarAssertion = new AssertCmd(Token.NoToken, invarExpr);

-            CmdSeq newCmds = new CmdSeq();

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

             newCmds.Add(invarAssertion);

 

             // make a record in annotationInfo;

@@ -1176,7 +1176,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--)

                         {

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

 

 

-                CmdSeq cmds = b.Cmds;

+                List<Cmd> cmds = b.Cmds;

                 TransferCmd transferCmd = cce.NonNull(b.TransferCmd);

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

                 {

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index d1a83827..f29a1b80 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -359,7 +359,7 @@ namespace VC {
     public void InstrumentCallSites(Implementation implementation) {

       var callSiteId = 0;

       foreach (Block block in implementation.Blocks) {

-        CmdSeq newCmds = new CmdSeq();

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

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

           Cmd cmd = block.Cmds[i];

           newCmds.Add(cmd);

@@ -2582,7 +2582,7 @@ namespace VC {
         Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));

         // After translation, all potential errors come from asserts.

         while (true) {

-          CmdSeq cmds = b.Cmds;

+          List<Cmd> cmds = b.Cmds;

           TransferCmd transferCmd = cce.NonNull(b.TransferCmd);

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

             Cmd cmd = cce.NonNull(cmds[i]);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 491c7eae..96cf5486 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -134,7 +134,7 @@ namespace VC {
         if (copies.TryGetValue(b, out fake_res)) {

           return cce.NonNull(fake_res);

         }

-        Block res = new Block(b.tok, b.Label, new CmdSeq(b.Cmds), null);

+        Block res = new Block(b.tok, b.Label, new List<Cmd>(b.Cmds), null);

         copies[b] = res;

         if (b.TransferCmd is GotoCmd) {

           foreach (Block ch in cce.NonNull((GotoCmd)b.TransferCmd).labelTargets) {

@@ -160,7 +160,7 @@ namespace VC {
           return cce.NonNull(fake_res);

         }

         Block res;

-        CmdSeq seq = new CmdSeq();

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

         foreach (Cmd c in b.Cmds) {

           Contract.Assert(c != null);

           AssertCmd turn = c as AssertCmd;

@@ -252,7 +252,7 @@ namespace VC {
         return BooleanEval(e, ref val) && !val;

       }

 

-      bool CheckUnreachable(Block cur, CmdSeq seq)

+      bool CheckUnreachable(Block cur, List<Cmd> seq)

       {

         Contract.Requires(cur != null);

         Contract.Requires(seq != null);

@@ -369,7 +369,7 @@ namespace VC {
           return;

         visited.Add(cur);

 

-        CmdSeq seq = new CmdSeq();

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

         foreach (Cmd cmd_ in cur.Cmds) {

           Cmd cmd = cmd_;

           Contract.Assert(cmd != null);

@@ -902,15 +902,15 @@ namespace VC {
         return cost;

       }

 

-      CmdSeq SliceCmds(Block b) {

+      List<Cmd> SliceCmds(Block b) {

         Contract.Requires(b != null);

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

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

 

-        CmdSeq seq = b.Cmds;

+        List<Cmd> seq = b.Cmds;

         Contract.Assert(seq != null);

         if (!doing_slice && !ShouldAssumize(b))

           return seq;

-        CmdSeq res = new CmdSeq();

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

         foreach (Cmd c in seq) {

           Contract.Assert(c != null);

           AssertCmd a = c as AssertCmd;

@@ -1882,7 +1882,7 @@ namespace VC {
 

       // Recompute the predecessors, but first insert a dummy start node that is sure not to be the target of any goto (because the cutting of back edges

       // below assumes that the start node has no predecessor)

-      impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new CmdSeq(), new GotoCmd(Token.NoToken, new StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0]))));

+      impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0]))));

       ResetPredecessors(impl.Blocks);

       

       #region Convert program CFG into a DAG

@@ -1911,8 +1911,8 @@ namespace VC {
         foreach (Block b in cce.NonNull( g.BackEdgeNodes(header))) {Contract.Assert(b != null); backEdgeNodes.Add(b, null); }

       

         #region Find the (possibly empty) prefix of assert commands in the header, replace each assert with an assume of the same condition

-        CmdSeq prefixOfPredicateCmdsInit = new CmdSeq();

-        CmdSeq prefixOfPredicateCmdsMaintained = new CmdSeq();

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

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

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

         {

           PredicateCmd a = header.Cmds[i] as PredicateCmd;

@@ -2056,7 +2056,7 @@ namespace VC {
         // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct

         // the source location for this later on

         HavocCmd hc = new HavocCmd(header.tok,havocExprs);

-        CmdSeq newCmds = new CmdSeq();

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

         newCmds.Add(hc);

         foreach ( Cmd c in header.Cmds )

         {

@@ -2079,7 +2079,7 @@ namespace VC {
 

     public void DesugarCalls(Implementation impl) {

       foreach (Block block in impl.Blocks) {

-        CmdSeq newCmds = new CmdSeq();

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

         foreach (Cmd cmd in block.Cmds) {

           SugaredCmd sugaredCmd = cmd as SugaredCmd;

           if (sugaredCmd != null) {

@@ -2116,7 +2116,7 @@ namespace VC {
 

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

       {

-        CmdSeq cc = new CmdSeq();

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

         // where clauses of global variables

         lock (program.TopLevelDeclarations)

         {

@@ -2207,7 +2207,7 @@ namespace VC {
         }

 

         if (axioms.Count > 0) {

-          CmdSeq cmds = new CmdSeq();

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

           foreach (Expr ax in axioms) {

             Contract.Assert(ax != null);

             cmds.Add(new AssumeCmd(ax.tok, ax));

@@ -2273,7 +2273,7 @@ namespace VC {
 

         foreach (var b in impl.Blocks) {

           if (blocksToCheck.Contains(b)) continue;

-          var newCmds = new CmdSeq();

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

           var copyMode = false;

           foreach (Cmd c in b.Cmds) {

             var p = c as PredicateCmd;

@@ -2460,7 +2460,7 @@ namespace VC {
       Contract.Requires(context != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));

       // After translation, all potential errors come from asserts.

-      CmdSeq cmds = b.Cmds;

+      List<Cmd> cmds = b.Cmds;

       Contract.Assert(cmds != null);

       TransferCmd transferCmd = cce.NonNull(b.TransferCmd);

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