diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2015-01-25 20:58:15 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-01-25 20:58:15 +0000 |
| commit | ca82edae68c55548b70530f02a7d346870aece04 (patch) | |
| tree | 88c4424976b90bba1ee90324978a0b0c99485b2b /Source | |
| parent | ffcf2c27da335ff452a0c2388c33195ff59c8550 (diff) | |
Change the return type of StandardVisitor.VisitLiteralExpr() from
LiteralExpr to Expr. Enforcing the return type be LiteralExpr is
too restrictive.
There is precedence for this. For example VisitNAryExpr() returns
an Expr not an NAryExpr.
Unfortunately this a breaking API change so anyone who subclasses
the StandardVisitor (or one of its sub classes) and overrides this
method will get compilation errors until they change the return type.
a visitor that does constant folding of an Expr tree
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 2 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 2 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 4 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 5a4c606f..1ac80970 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -659,7 +659,7 @@ namespace Microsoft.Boogie.AbstractInterpretation Lo = Hi = null;
return base.VisitExpr(node);
}
- public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ public override Expr VisitLiteralExpr(LiteralExpr node) {
if (node.Val is BigNum) {
var n = ((BigNum)node.Val).ToBigInteger;
Lo = n;
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 759077b5..4350571a 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -290,7 +290,7 @@ namespace Microsoft.Boogie { return impl;
}
- public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ public override Expr VisitLiteralExpr(LiteralExpr node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return base.VisitLiteralExpr((LiteralExpr)node.Clone());
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 963f3ec6..82cd5025 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -359,7 +359,7 @@ namespace Microsoft.Boogie { node = (Implementation)this.VisitDeclWithFormals(node); // do this first or last?
return node;
}
- public virtual LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ public virtual Expr VisitLiteralExpr(LiteralExpr node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return node;
@@ -915,7 +915,7 @@ namespace Microsoft.Boogie { this.VisitProcedure(cce.NonNull(node.Proc));
return (Implementation)this.VisitDeclWithFormals(node); // do this first or last?
}
- public override LiteralExpr VisitLiteralExpr(LiteralExpr node)
+ public override Expr VisitLiteralExpr(LiteralExpr node)
{
Contract.Ensures(Contract.Result<LiteralExpr>() == node);
return node;
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 7cd3d240..49dbb7c8 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -314,7 +314,7 @@ namespace Microsoft.Boogie.VCExprAST { ///////////////////////////////////////////////////////////////////////////////////
- public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ public override Expr VisitLiteralExpr(LiteralExpr node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
Push(TranslateLiteralExpr(node));
|