From f11b44a267d7b77feccf33dd1d6d3a2ee712458e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 25 Jan 2015 20:39:09 +0000 Subject: Change the return type of StandardVisitor.VisitBvExtractExpr() from BvExtractExpr to Expr. Enforcing the return type be BvExtractExpr 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/VCExpr/Boogie2VCExpr.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Source/VCExpr/Boogie2VCExpr.cs') diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 3e78bb4b..d53a75a4 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -557,7 +557,7 @@ namespace Microsoft.Boogie.VCExprAST { /////////////////////////////////////////////////////////////////////////////////// - public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) { + public override Expr VisitBvExtractExpr(BvExtractExpr node) { //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Push(TranslateBvExtractExpr(node)); -- cgit v1.2.3