From ffcf2c27da335ff452a0c2388c33195ff59c8550 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 25 Jan 2015 20:51:44 +0000 Subject: Change the return type of StandardVisitor.VisitExistsExpr() from ExistsExpr to Expr. Enforcing the return type be ExistsExpr 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/Duplicator.cs | 2 +- Source/Core/StandardVisitor.cs | 4 ++-- Source/VCExpr/Boogie2VCExpr.cs | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 6164c23b..759077b5 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -204,7 +204,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result>() != null); return base.VisitEnsuresSeq(new List(ensuresSeq)); } - public override ExistsExpr VisitExistsExpr(ExistsExpr node) { + public override Expr VisitExistsExpr(ExistsExpr node) { //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); return base.VisitExistsExpr((ExistsExpr)node.Clone()); diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index a19bf78b..963f3ec6 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -239,7 +239,7 @@ namespace Microsoft.Boogie { node.OutParams = this.VisitVariableSeq(node.OutParams); return node; } - public virtual ExistsExpr VisitExistsExpr(ExistsExpr node) { + public virtual Expr VisitExistsExpr(ExistsExpr node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); node = (ExistsExpr)this.VisitQuantifierExpr(node); @@ -805,7 +805,7 @@ namespace Microsoft.Boogie { this.VisitVariableSeq(node.OutParams); return node; } - public override ExistsExpr VisitExistsExpr(ExistsExpr node) + public override Expr VisitExistsExpr(ExistsExpr node) { Contract.Ensures(Contract.Result() == node); return (ExistsExpr)this.VisitQuantifierExpr(node); diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index f261553b..7cd3d240 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -454,7 +454,7 @@ namespace Microsoft.Boogie.VCExprAST { return node; } - public override ExistsExpr VisitExistsExpr(ExistsExpr node) { + public override Expr VisitExistsExpr(ExistsExpr node) { //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); node = (ExistsExpr)this.VisitQuantifierExpr(node); -- cgit v1.2.3