diff options
| author |  Ally Donaldson <unknown> | 2013-07-22 22:51:04 +0100 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2013-07-22 22:51:04 +0100 |
| commit | 07e15dce2315f99bcbc7b3aa558653feec9de906 (patch) | |
| tree | 0dc266c3c2cef8ff33764401fb33b6540ee54ffa /Source/Predication | |
| parent | 793c0c0ded44401a1d6ef1bf494dd0a3d0b8dc43 (diff) | |
ExprSeq: farewell
Diffstat (limited to 'Source/Predication')
| -rw-r--r-- | Source/Predication/BlockPredicator.cs | 6 | ||||
| -rw-r--r-- | Source/Predication/SmartBlockPredicator.cs | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs index 2174c150..507aaf61 100644 --- a/Source/Predication/BlockPredicator.cs +++ b/Source/Predication/BlockPredicator.cs @@ -68,7 +68,7 @@ public class BlockPredicator { new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
new NAryExpr(Token.NoToken,
new IfThenElse(Token.NoToken),
- new ExprSeq(p, rhs, lhs.AsExpr))))));
+ new List<Expr> { p, rhs, lhs.AsExpr })))));
} else if (cmd is AssertCmd) {
var aCmd = (AssertCmd)cmd;
if (cmdSeq.Last() is AssignCmd &&
@@ -112,7 +112,7 @@ public class BlockPredicator { cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
new NAryExpr(Token.NoToken,
new IfThenElse(Token.NoToken),
- new ExprSeq(p, havocTempExpr, v))));
+ new List<Expr> { p, havocTempExpr, v })));
}
} else if (cmd is CallCmd) {
Debug.Assert(useProcedurePredicates);
@@ -261,7 +261,7 @@ public class BlockPredicator { if (useProcedurePredicates) {
return new NAryExpr(Token.NoToken,
new IfThenElse(Token.NoToken),
- new ExprSeq(fp, then, eElse));
+ new List<Expr>{ fp, then, eElse });
} else {
return then;
}
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index 8e1b960b..5222061f 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -86,7 +86,7 @@ public class SmartBlockPredicator { new List<Expr>(aCmd.Lhss.Zip(aCmd.Rhss, (lhs, rhs) =>
new NAryExpr(Token.NoToken,
new IfThenElse(Token.NoToken),
- new ExprSeq(p, rhs, lhs.AsExpr))))));
+ new List<Expr> { p, rhs, lhs.AsExpr })))));
} else if (cmd is AssertCmd) {
var aCmd = (AssertCmd)cmd;
Expr newExpr = new EnabledReplacementVisitor(p).VisitExpr(aCmd.Expr);
@@ -119,7 +119,7 @@ public class SmartBlockPredicator { cmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, v,
new NAryExpr(Token.NoToken,
new IfThenElse(Token.NoToken),
- new ExprSeq(p, havocTempExpr, v))));
+ new List<Expr> { p, havocTempExpr, v })));
}
} else if (cmd is CommentCmd) {
// skip
@@ -470,7 +470,7 @@ public class SmartBlockPredicator { if (myUseProcedurePredicates) {
return new NAryExpr(Token.NoToken,
new IfThenElse(Token.NoToken),
- new ExprSeq(fp, then, eElse));
+ new List<Expr> { fp, then, eElse });
} else {
return then;
}
|