CmdSeq: farewell

3 files changed, 23 insertions, 23 deletions

diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs
index c655175a..771d403b 100644
--- a/Source/Predication/BlockPredicator.cs
+++ b/Source/Predication/BlockPredicator.cs
@@ -61,7 +61,7 @@ public class BlockPredicator {
     }

   }

 

-  void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) {

+  void PredicateCmd(List<Cmd> cmdSeq, Cmd cmd) {

     if (cmd is AssignCmd) {

       var aCmd = (AssignCmd)cmd;

       cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,

@@ -125,7 +125,7 @@ public class BlockPredicator {
     }

     else if (cmd is StateCmd) {

       var sCmd = (StateCmd)cmd;

-      var newCmdSeq = new CmdSeq();

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

       foreach (Cmd c in sCmd.Cmds)

         PredicateCmd(newCmdSeq, c);

       sCmd.Cmds = newCmdSeq;

@@ -136,7 +136,7 @@ public class BlockPredicator {
     }

   }

 

-  void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) {

+  void PredicateTransferCmd(List<Cmd> cmdSeq, TransferCmd cmd) {

     if (cmd is GotoCmd) {

       var gCmd = (GotoCmd)cmd;

       var targets = new List<Expr>(

@@ -161,7 +161,7 @@ public class BlockPredicator {
                                          aCmd.Expr)));

               }

               b.Cmds =

-                new CmdSeq(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray());

+                new List<Cmd>(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray());

             }

           }

         }

@@ -201,9 +201,9 @@ public class BlockPredicator {
 

     Block entryBlock = new Block();

     entryBlock.Label = "entry";

-    entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur,

+    entryBlock.Cmds = new List<Cmd> { Cmd.SimpleAssign(Token.NoToken, cur,

                         CreateIfFPThenElse(blockIds[sortedBlocks[0].Item1],

-                                           returnBlockId)));

+                                           returnBlockId)) };

     newBlocks.Add(entryBlock);

 

     var prevBlock = entryBlock;

@@ -213,9 +213,9 @@ public class BlockPredicator {
         newBlocks.Add(backedgeBlock);

 

         backedgeBlock.Label = n.Item1.Label + ".backedge";

-        backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,

+        backedgeBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken,

           Expr.Eq(cur, blockIds[n.Item1]),

-          new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));

+          new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)) };

         backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,

                                                 new BlockSeq(n.Item1));

 

@@ -223,8 +223,8 @@ public class BlockPredicator {
         newBlocks.Add(tailBlock);

 

         tailBlock.Label = n.Item1.Label + ".tail";

-        tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,

-                                             Expr.Neq(cur, blockIds[n.Item1])));

+        tailBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken,

+                                             Expr.Neq(cur, blockIds[n.Item1])) };

 

         prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

                                         new BlockSeq(backedgeBlock, tailBlock));

@@ -232,7 +232,7 @@ public class BlockPredicator {
       } else {

         var runBlock = n.Item1;

         var oldCmdSeq = runBlock.Cmds;

-        runBlock.Cmds = new CmdSeq();

+        runBlock.Cmds = new List<Cmd>();

         newBlocks.Add(runBlock);

         prevBlock.TransferCmd = new GotoCmd(Token.NoToken,

                                             new BlockSeq(runBlock));

@@ -267,13 +267,13 @@ public class BlockPredicator {
     }

   }

 

-  private void AddUniformCandidateInvariant(CmdSeq cs, Block header) {

+  private void AddUniformCandidateInvariant(List<Cmd> cs, Block header) {

     cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur,

                CreateIfFPThenElse(blockIds[header], returnBlockId)),

              "uniform loop"));

   }

 

-  private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) {

+  private void AddNonUniformCandidateInvariant(List<Cmd> cs, Block header) {

     var loopNodes = new HashSet<Block>();

     foreach (var b in blockGraph.BackEdgeNodes(header))

       loopNodes.UnionWith(blockGraph.NaturalLoops(header, b));

diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs
index 28005186..94b47f5e 100644
--- a/Source/Predication/SmartBlockPredicator.cs
+++ b/Source/Predication/SmartBlockPredicator.cs
@@ -72,7 +72,7 @@ public class SmartBlockPredicator {
     }

   }

 

-  void PredicateCmd(Expr p, CmdSeq cmdSeq, Cmd cmd) {

+  void PredicateCmd(Expr p, List<Cmd> cmdSeq, Cmd cmd) {

     if (cmd is CallCmd) {

       var cCmd = (CallCmd)cmd;

       Debug.Assert(useProcedurePredicates(cCmd.Proc));

@@ -125,7 +125,7 @@ public class SmartBlockPredicator {
       // skip

     } else if (cmd is StateCmd) {

       var sCmd = (StateCmd)cmd;

-      var newCmdSeq = new CmdSeq();

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

       foreach (Cmd c in sCmd.Cmds)

         PredicateCmd(p, newCmdSeq, c);

       sCmd.Cmds = newCmdSeq;

@@ -137,7 +137,7 @@ public class SmartBlockPredicator {
 

   // hasPredicatedRegion is true iff the block or its targets are predicated

   // (i.e. we enter, stay within or exit a predicated region).

-  void PredicateTransferCmd(Expr p, Block src, CmdSeq cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) {

+  void PredicateTransferCmd(Expr p, Block src, List<Cmd> cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) {

     hasPredicatedRegion = predMap.ContainsKey(src);

 

     if (cmd is GotoCmd) {

@@ -347,7 +347,7 @@ public class SmartBlockPredicator {
       if (parts.Count() > 0) {

         pred = parts.Select(a => ((AssumeCmd)a).Expr).Aggregate(Expr.And);

         block.Cmds =

-          new CmdSeq(block.Cmds.Cast<Cmd>().Skip(parts.Count()).ToArray());

+          new List<Cmd>(block.Cmds.Cast<Cmd>().Skip(parts.Count()).ToArray());

       } else {

         continue;

       }

@@ -386,8 +386,8 @@ public class SmartBlockPredicator {
           newBlocks.Add(backedgeBlock);

 

           backedgeBlock.Label = n.Item1.Label + ".backedge";

-          backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, pExpr,

-            new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));

+          backedgeBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken, pExpr,

+            new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)) };

           backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,

                                                   new BlockSeq(n.Item1));

 

@@ -395,8 +395,8 @@ public class SmartBlockPredicator {
           newBlocks.Add(tailBlock);

 

           tailBlock.Label = n.Item1.Label + ".tail";

-          tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,

-                                               Expr.Not(pExpr)));

+          tailBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken,

+                                               Expr.Not(pExpr)) };

 

           if (uni != null && !uni.IsUniform(impl.Name, n.Item1)) {

             uni.AddNonUniform(impl.Name, backedgeBlock);

@@ -427,7 +427,7 @@ public class SmartBlockPredicator {
     var firstBlock = block;

 

     var oldCmdSeq = block.Cmds;

-    block.Cmds = new CmdSeq();

+    block.Cmds = new List<Cmd>();

     newBlocks.Add(block);

     if (prevBlock != null) {

       prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(block));

diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs
index a6287db5..3c8f4cd9 100644
--- a/Source/Predication/UniformityAnalyser.cs
+++ b/Source/Predication/UniformityAnalyser.cs
@@ -292,7 +292,7 @@ namespace Microsoft.Boogie
             return null;

         }

 

-        private bool Analyse(Implementation impl, CmdSeq cmdSeq, bool ControlFlowIsUniform)

+        private bool Analyse(Implementation impl, List<Cmd> cmdSeq, bool ControlFlowIsUniform)

         {

             foreach (Cmd c in cmdSeq)

             {