diff options
| author |  Ally Donaldson <unknown> | 2013-07-22 21:17:07 +0100 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2013-07-22 21:17:07 +0100 |
| commit | 12f3c4d7f530265c966bc72764d17e08a47aa4c0 (patch) | |
| tree | 8d9f4c144e88ebe5c748042fcb07b0474a64d1f2 /Source/Predication | |
| parent | 42bf19b1e4fdde3d3a936a11d2e9eeb95ddd43dd (diff) | |
Started to remove ...Seq classes
Diffstat (limited to 'Source/Predication')
| -rw-r--r-- | Source/Predication/BlockPredicator.cs | 6 | ||||
| -rw-r--r-- | Source/Predication/SmartBlockPredicator.cs | 4 |
2 files changed, 5 insertions, 5 deletions
diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs index eac60511..c655175a 100644 --- a/Source/Predication/BlockPredicator.cs +++ b/Source/Predication/BlockPredicator.cs @@ -108,7 +108,7 @@ public class BlockPredicator { new IdentifierExpr(Token.NoToken, havocVar);
}
cmdSeq.Add(new HavocCmd(Token.NoToken,
- new IdentifierExprSeq(havocTempExpr)));
+ new List<IdentifierExpr> { havocTempExpr }));
cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
new NAryExpr(Token.NoToken,
new IfThenElse(Token.NoToken),
@@ -145,7 +145,7 @@ public class BlockPredicator { PredicateCmd(cmdSeq, Cmd.SimpleAssign(Token.NoToken, cur, targets[0]));
} else {
PredicateCmd(cmdSeq, new HavocCmd(Token.NoToken,
- new IdentifierExprSeq(cur)));
+ new List<IdentifierExpr> { cur }));
PredicateCmd(cmdSeq, new AssumeCmd(Token.NoToken,
targets.Select(t => (Expr)Expr.Eq(cur, t)).Aggregate(Expr.Or)));
}
@@ -305,7 +305,7 @@ public class BlockPredicator { new TypedIdent(Token.NoToken, "_P",
Microsoft.Boogie.Type.Bool),
/*incoming=*/true);
- dwf.InParams = new VariableSeq(
+ dwf.InParams = new List<Variable>(
(new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
.ToArray());
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index 9dc10d02..484a866d 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -115,7 +115,7 @@ public class SmartBlockPredicator { new IdentifierExpr(Token.NoToken, havocVar);
}
cmdSeq.Add(new HavocCmd(Token.NoToken,
- new IdentifierExprSeq(havocTempExpr)));
+ new List<IdentifierExpr>(havocTempExpr)));
cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
new NAryExpr(Token.NoToken,
new IfThenElse(Token.NoToken),
@@ -501,7 +501,7 @@ public class SmartBlockPredicator { new TypedIdent(Token.NoToken, "_P",
Microsoft.Boogie.Type.Bool),
/*incoming=*/true);
- dwf.InParams = new VariableSeq(
+ dwf.InParams = new List<Variable>(
(new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
.ToArray());
|