summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-01-25 20:46:28 +0000
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-01-25 20:46:28 +0000
commit75a170c34ad60fda22961045cfcdb89fda3f4571 (patch)
tree5aca2937790180f264db425f065aa367e6b63264 /Source/Core
parentf11b44a267d7b77feccf33dd1d6d3a2ee712458e (diff)
Change the return type of StandardVisitor.VisitForAllExpr() from
ForAllExpr to Expr. Enforcing the return type be ForAllExpr 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. a visitor that does constant folding of an Expr tree
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/Duplicator.cs2
-rw-r--r--Source/Core/StandardVisitor.cs4
2 files changed, 3 insertions, 3 deletions
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index da2b5b95..6164c23b 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -219,7 +219,7 @@ namespace Microsoft.Boogie {
Contract.Ensures(Contract.Result<List<Expr>>() != null);
return base.VisitExprSeq(new List<Expr>(list));
}
- public override ForallExpr VisitForallExpr(ForallExpr node) {
+ public override Expr VisitForallExpr(ForallExpr node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<ForallExpr>() != null);
return base.VisitForallExpr((ForallExpr)node.Clone());
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index a50acdba..a19bf78b 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -290,7 +290,7 @@ namespace Microsoft.Boogie {
ensuresSeq[i] = this.VisitEnsures(ensuresSeq[i]);
return ensuresSeq;
}
- public virtual ForallExpr VisitForallExpr(ForallExpr node) {
+ public virtual Expr VisitForallExpr(ForallExpr node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<ForallExpr>() != null);
node = (ForallExpr)this.VisitQuantifierExpr(node);
@@ -854,7 +854,7 @@ namespace Microsoft.Boogie {
this.VisitEnsures(ensuresSeq[i]);
return ensuresSeq;
}
- public override ForallExpr VisitForallExpr(ForallExpr node)
+ public override Expr VisitForallExpr(ForallExpr node)
{
Contract.Ensures(Contract.Result<ForallExpr>() == node);
return (ForallExpr)this.VisitQuantifierExpr(node);