summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/FixedpointVC.cs
diff options
context:
space:
mode:
authorGravatar Ally Donaldson <unknown>2013-07-22 21:17:07 +0100
committerGravatar Ally Donaldson <unknown>2013-07-22 21:17:07 +0100
commit12f3c4d7f530265c966bc72764d17e08a47aa4c0 (patch)
tree8d9f4c144e88ebe5c748042fcb07b0474a64d1f2 /Source/VCGeneration/FixedpointVC.cs
parent42bf19b1e4fdde3d3a936a11d2e9eeb95ddd43dd (diff)
Started to remove ...Seq classes
Diffstat (limited to 'Source/VCGeneration/FixedpointVC.cs')
-rw-r--r--Source/VCGeneration/FixedpointVC.cs8
1 files changed, 4 insertions, 4 deletions
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);