summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-01-25 19:06:23 +0000
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-01-25 19:06:23 +0000
commit458be604ebe9f9ed93a2b8af4c424493f119cd8c (patch)
tree0bbe880c9657b6ef8cf40ab2eb0015d46ebb521e /Source
parent5a92b5242c4febbf32371919845eadc22d405fad (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.cs2
-rw-r--r--Source/Core/Duplicator.cs2
-rw-r--r--Source/Core/StandardVisitor.cs4
-rw-r--r--Source/VCExpr/Boogie2VCExpr.cs2
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));