diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2015-01-25 19:06:23 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-01-25 19:06:23 +0000 |
| commit | 458be604ebe9f9ed93a2b8af4c424493f119cd8c (patch) | |
| tree | 0bbe880c9657b6ef8cf40ab2eb0015d46ebb521e /Source | |
| parent | 5a92b5242c4febbf32371919845eadc22d405fad (diff) | |
Change the return type of StandardVisitor.VisitBvConcatExpr() from
BvConcatExpr to Expr. Enforcing the return type be BvConcatExpr is
too restrictive. For example it prevents anyone from implementing
a visitor that does constant folding of an Expr tree.
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.
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 6cce0aac..c0303cb3 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -944,7 +944,7 @@ namespace Microsoft.Boogie.AbstractInterpretation // don't recurse on subexpression
return node;
}
- public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {
+ public override Expr VisitBvConcatExpr(BvConcatExpr node) {
// don't recurse on subexpression
return node;
}
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 32eb2480..fbe36feb 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -77,7 +77,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Block>() != null);
return base.VisitBlock((Block) node.Clone());
}
- public override BvConcatExpr VisitBvConcatExpr (BvConcatExpr node) {
+ public override Expr VisitBvConcatExpr (BvConcatExpr node) {
Contract.Ensures(Contract.Result<BvConcatExpr>() != null);
return base.VisitBvConcatExpr((BvConcatExpr) node.Clone());
}
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index f7538b53..4c167953 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -103,7 +103,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Type>() != null);
return this.VisitType(node);
}
- public virtual BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {
+ public virtual Expr VisitBvConcatExpr(BvConcatExpr node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<BvConcatExpr>() != null);
node.E0 = this.VisitExpr(node.E0);
@@ -679,7 +679,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Type>() == node);
return this.VisitType(node);
}
- public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node)
+ public override Expr VisitBvConcatExpr(BvConcatExpr node)
{
Contract.Ensures(Contract.Result<BvConcatExpr>() == node);
this.VisitExpr(node.E0);
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 91c17b23..3e78bb4b 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -574,7 +574,7 @@ namespace Microsoft.Boogie.VCExprAST { ///////////////////////////////////////////////////////////////////////////////////
- public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {
+ public override Expr VisitBvConcatExpr(BvConcatExpr node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<BvConcatExpr>() != null);
Push(TranslateBvConcatExpr(node));
|