diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2015-01-25 19:06:23 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-01-25 19:06:23 +0000 |
| commit | 458be604ebe9f9ed93a2b8af4c424493f119cd8c (patch) | |
| tree | 0bbe880c9657b6ef8cf40ab2eb0015d46ebb521e /Source/VCExpr | |
| parent | 5a92b5242c4febbf32371919845eadc22d405fad (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/VCExpr')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 2 |
1 files changed, 1 insertions, 1 deletions
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));
|