From 2dae113e5996e050ca6595542de5030747245929 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Mon, 27 Apr 2015 05:37:19 -0600 Subject: Began adding the float type to VC expression --- Source/VCExpr/VCExprASTVisitors.cs | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) (limited to 'Source/VCExpr/VCExprASTVisitors.cs') diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index ad0c270d..1bcce113 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -77,6 +77,7 @@ namespace Microsoft.Boogie.VCExprAST { Result VisitDivOp(VCExprNAry node, Arg arg); Result VisitModOp(VCExprNAry node, Arg arg); Result VisitRealDivOp(VCExprNAry node, Arg arg); + Result VisitFloatDivOp(VCExprNAry node, Arg arg); //TODO: Add this to references from above and below Result VisitPowOp(VCExprNAry node, Arg arg); Result VisitLtOp(VCExprNAry node, Arg arg); Result VisitLeOp(VCExprNAry node, Arg arg); @@ -189,6 +190,12 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException(); } + public Result VisitFloatDivOp(VCExprNAry node, Arg arg) + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + public Result VisitPowOp(VCExprNAry node, Arg arg) { Contract.Requires(node != null); throw new NotImplementedException(); @@ -234,6 +241,12 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException(); } + public Result VisitToFloat(VCExprNAry node, Arg arg) //TODO: modify later + { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) { Contract.Requires(node != null); throw new NotImplementedException(); @@ -1482,6 +1495,11 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return StandardResult(node, arg); } + public virtual Result VisitFloatDivOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } public virtual Result VisitPowOp(VCExprNAry node, Arg arg) { //Contract.Requires(node != null); return StandardResult(node, arg); @@ -1518,6 +1536,11 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null); return StandardResult(node, arg); } + public virtual Result VisitToFloatOp(VCExprNAry node, Arg arg) + { + //Contract.Requires(node != null); + return StandardResult(node, arg); + } public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) { //Contract.Requires(node != null); return StandardResult(node, arg); -- cgit v1.2.3