ExprSeq: farewell

3 files changed, 7 insertions, 7 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 93de935d..36b8fbe5 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -1431,7 +1431,7 @@ namespace VC {
         if (CommandLineOptions.Clo.ModelViewFile != null && pc is AssumeCmd) {

           string description = QKeyValue.FindStringAttribute(pc.Attributes, "captureState");

           if (description != null) {

-            Expr mv = new NAryExpr(pc.tok, new FunctionCall(ModelViewInfo.MVState_FunctionDef), new ExprSeq(Bpl.Expr.Ident(ModelViewInfo.MVState_ConstantDef), Bpl.Expr.Literal(mvInfo.CapturePoints.Count)));

+            Expr mv = new NAryExpr(pc.tok, new FunctionCall(ModelViewInfo.MVState_FunctionDef), new List<Expr> { Bpl.Expr.Ident(ModelViewInfo.MVState_ConstantDef), Bpl.Expr.Literal(mvInfo.CapturePoints.Count) });

             copy = Bpl.Expr.And(mv, copy);

             mvInfo.CapturePoints.Add(new ModelViewInfo.Mapping(description, new Dictionary<Variable, Expr>(incarnationMap)));

           }

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 3fe3910e..330ffe49 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -177,7 +177,7 @@ namespace Microsoft.Boogie
                 return;

 

             // collect the variables needed in the invariant

-            ExprSeq exprs = new ExprSeq();

+            List<Expr> exprs = new List<Expr>();

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

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

 

@@ -283,7 +283,7 @@ namespace Microsoft.Boogie
             CurrentLocalVariables = impl.LocVars;

 

             // collect the variables needed in the invariant

-            ExprSeq exprs = new ExprSeq();

+            List<Expr> exprs = new List<Expr>();

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

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

 

@@ -590,7 +590,7 @@ namespace Microsoft.Boogie
                     implName2StratifiedInliningInfo[impl.Name] = info;

                     // We don't need controlFlowVariable for stratified Inlining

                     //impl.LocVars.Add(info.controlFlowVariable);

-                    ExprSeq exprs = new ExprSeq();

+                    List<Expr> exprs = new List<Expr>();

 

                     if (mode != Mode.Boogie && QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))

                     {

@@ -660,7 +660,7 @@ namespace Microsoft.Boogie
                 var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

                 boogieContext.DeclareFunction(recordFunc, "");

 

-                var exprs = new ExprSeq();

+                var exprs = new List<Expr>();

                 exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));

 

                 Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index ef2cd1d1..7f5b3779 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -213,7 +213,7 @@ namespace VC {
       function = new Function(Token.NoToken, impl.Name, functionInterfaceVars, returnVar);

       vcgen.prover.Context.DeclareFunction(function, "");

 

-      ExprSeq exprs = new ExprSeq();

+      List<Expr> exprs = new List<Expr>();

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

         Contract.Assert(v != null);

         exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

@@ -343,7 +343,7 @@ namespace VC {
         var recordFunc = new Function(Token.NoToken, proc.Name, ins, returnVar);

         prover.Context.DeclareFunction(recordFunc, "");

 

-        var exprs = new ExprSeq();

+        var exprs = new List<Expr>();

         exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0]));

 

         Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordFunc), exprs);