From 75a170c34ad60fda22961045cfcdb89fda3f4571 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 25 Jan 2015 20:46:28 +0000 Subject: 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 --- Source/Core/StandardVisitor.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Source/Core/StandardVisitor.cs') 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() != 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() == node); return (ForallExpr)this.VisitQuantifierExpr(node); -- cgit v1.2.3