diff options
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 2 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 2 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 4 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 5a4c606f..1ac80970 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -659,7 +659,7 @@ namespace Microsoft.Boogie.AbstractInterpretation Lo = Hi = null;
return base.VisitExpr(node);
}
- public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ public override Expr VisitLiteralExpr(LiteralExpr node) {
if (node.Val is BigNum) {
var n = ((BigNum)node.Val).ToBigInteger;
Lo = n;
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 759077b5..4350571a 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -290,7 +290,7 @@ namespace Microsoft.Boogie { return impl;
}
- public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ public override Expr VisitLiteralExpr(LiteralExpr node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return base.VisitLiteralExpr((LiteralExpr)node.Clone());
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 963f3ec6..82cd5025 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -359,7 +359,7 @@ namespace Microsoft.Boogie { node = (Implementation)this.VisitDeclWithFormals(node); // do this first or last?
return node;
}
- public virtual LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ public virtual Expr VisitLiteralExpr(LiteralExpr node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return node;
@@ -915,7 +915,7 @@ namespace Microsoft.Boogie { this.VisitProcedure(cce.NonNull(node.Proc));
return (Implementation)this.VisitDeclWithFormals(node); // do this first or last?
}
- public override LiteralExpr VisitLiteralExpr(LiteralExpr node)
+ public override Expr VisitLiteralExpr(LiteralExpr node)
{
Contract.Ensures(Contract.Result<LiteralExpr>() == node);
return node;
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 7cd3d240..49dbb7c8 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -314,7 +314,7 @@ namespace Microsoft.Boogie.VCExprAST { ///////////////////////////////////////////////////////////////////////////////////
- public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ public override Expr VisitLiteralExpr(LiteralExpr node) {
//Contract.Requires(node != null);
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
Push(TranslateLiteralExpr(node));
|