Started to remove ...Seq classes

6 files changed, 18 insertions, 18 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 01366633..6137678b 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -576,7 +576,7 @@ namespace VC {
 

     private bool _disposed;

 

-    protected VariableSeq CurrentLocalVariables = null;

+    protected List<Variable> CurrentLocalVariables = null;

 

     // shared across each implementation; created anew for each implementation

     protected Dictionary<Variable, int> variable2SequenceNumber;

@@ -1323,7 +1323,7 @@ namespace VC {
       return r;

     }

 

-    protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies, ModelViewInfo mvInfo) {

+    protected Dictionary<Variable, Expr> ConvertBlocks2PassiveCmd(List<Block> blocks, List<IdentifierExpr> modifies, ModelViewInfo mvInfo) {

       Contract.Requires(blocks != null);

       Contract.Requires(modifies != null);

       Contract.Requires(mvInfo != null);

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

     /// Compute the substitution for old expressions.

     /// </summary>

-    protected static Substitution ComputeOldExpressionSubstitution(IdentifierExprSeq modifies)

+    protected static Substitution ComputeOldExpressionSubstitution(List<IdentifierExpr> modifies)

     {

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

       foreach (IdentifierExpr ie in modifies)

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

         HavocCmd hc = (HavocCmd)c;

         Contract.Assert(c != null);

-        IdentifierExprSeq havocVars = hc.Vars;

+        List<IdentifierExpr> havocVars = hc.Vars;

         // First, compute the new incarnations

         foreach (IdentifierExpr ie in havocVars) {

           Contract.Assert(ie != null);

@@ -1703,8 +1703,8 @@ namespace VC {
     public readonly List<Variable> AllVariables = new List<Variable>();

     public readonly List<Mapping> CapturePoints = new List<Mapping>();

     public static readonly Function MVState_FunctionDef = new Function(Token.NoToken, "$mv_state",

-      new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true),

-                      new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true)),

+      new List<Variable> { new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true),

+                           new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Int), true) },

       new Formal(Token.NoToken, new TypedIdent(Token.NoToken, TypedIdent.NoName, Bpl.Type.Bool), false));

     public static readonly Constant MVState_ConstantDef = new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "$mv_state_const", Bpl.Type.Int));

 

diff --git a/Source/VCGeneration/ExprExtensions.cs b/Source/VCGeneration/ExprExtensions.cs
index 7ebba061..2bdb4af7 100644
--- a/Source/VCGeneration/ExprExtensions.cs
+++ b/Source/VCGeneration/ExprExtensions.cs
@@ -159,7 +159,7 @@ namespace Microsoft.Boogie.ExprExtensions
 

         public FuncDecl MkFuncDecl(string name, Sort rng)

         {

-            Function g = new Function(Token.NoToken, name, new VariableSeq(), new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "dummy",rng)));

+            Function g = new Function(Token.NoToken, name, new List<Variable>(), new Constant(Token.NoToken, new TypedIdent(Token.NoToken, "dummy",rng)));

             return BoogieFunctionOp(g);

         }

 

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

             // collect the variables needed in the invariant

             ExprSeq exprs = new ExprSeq();

-            VariableSeq vars = new VariableSeq();

+            List<Variable> vars = new List<Variable>();

             List<string> names = new List<string>();

 

             if (style == AnnotationStyle.Flat)

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

             // collect the variables needed in the invariant

             ExprSeq exprs = new ExprSeq();

-            VariableSeq vars = new VariableSeq();

+            List<Variable> vars = new List<Variable>();

             List<string> names = new List<string>();

 

                 foreach (Variable v in program.GlobalVariables())

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

                 this.interfaceVars = interfaceVars;

                 this.assertExpr = Expr.Not(assertExpr);

-                VariableSeq functionInterfaceVars = new VariableSeq();

+                List<Variable> functionInterfaceVars = new List<Variable>();

                 foreach (Variable v in interfaceVars)

                 {

                     Contract.Assert(v != null);

@@ -654,7 +654,7 @@ namespace Microsoft.Boogie
                 // Get record type

                 var argtype = proc.InParams[0].TypedIdent.Type;

 

-                var ins = new VariableSeq();

+                var ins = new List<Variable>();

                 ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));

 

                 var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

diff --git a/Source/VCGeneration/OrderingAxioms.cs b/Source/VCGeneration/OrderingAxioms.cs
index 4fbc80da..1e7615cb 100644
--- a/Source/VCGeneration/OrderingAxioms.cs
+++ b/Source/VCGeneration/OrderingAxioms.cs
@@ -91,7 +91,7 @@ namespace Microsoft.Boogie {
 

       Function res;

       if (!OneStepFuns.TryGetValue(t, out res)) {

-        VariableSeq args = new VariableSeq();

+        List<Variable> args = new List<Variable>();

         args.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "arg0", t), true));

         args.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "arg1", t), true));

         Formal result = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "res", t), false);

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 5848e63b..d1a83827 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -195,7 +195,7 @@ namespace VC {
       vcgen = stratifiedVcGen;

       impl = implementation;

 

-      VariableSeq functionInterfaceVars = new VariableSeq();

+      List<Variable> functionInterfaceVars = new List<Variable>();

       foreach (Variable v in vcgen.program.GlobalVariables()) {

         functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", v.TypedIdent.Type), true));

       }

@@ -337,7 +337,7 @@ namespace VC {
         // Get record type

         var argtype = proc.InParams[0].TypedIdent.Type;

 

-        var ins = new VariableSeq();

+        var ins = new List<Variable>();

         ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", argtype), true));

 

         var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

@@ -430,7 +430,7 @@ namespace VC {
     public Macro CreateNewMacro() {

       string newName = "StratifiedInliningMacro@" + macroCountForStratifiedInlining.ToString();

       macroCountForStratifiedInlining++;

-      return new Macro(Token.NoToken, newName, new VariableSeq(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool), false));

+      return new Macro(Token.NoToken, newName, new List<Variable>(), new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool), false));

     }

     private int varCountForStratifiedInlining = 0;

     public VCExprVar CreateNewVar(Microsoft.Boogie.Type type) {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 19e28099..491c7eae 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1235,7 +1235,7 @@ namespace VC {
 

             ResetPredecessors(codeExpr.Blocks);

             vcgen.AddBlocksBetween(codeExpr.Blocks);

-            Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq(), new ModelViewInfo(codeExpr));

+            Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new List<IdentifierExpr>(), new ModelViewInfo(codeExpr));

             int ac;  // computed, but then ignored for this CodeExpr

             VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);

             VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);

@@ -2031,7 +2031,7 @@ namespace VC {
         #endregion

 

         #region Collect all variables that are assigned to in all of the natural loops for which this is the header

-        VariableSeq varsToHavoc = new VariableSeq();

+        List<Variable> varsToHavoc = new List<Variable>();

         foreach (Block backEdgeNode in cce.NonNull( g.BackEdgeNodes(header)))

         {

           Contract.Assert(backEdgeNode != null);

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

           }

         }

-        IdentifierExprSeq havocExprs = new IdentifierExprSeq();

+        List<IdentifierExpr> havocExprs = new List<IdentifierExpr>();

         foreach ( Variable v in varsToHavoc )

         {

           Contract.Assert(v != null);