Began adding the float type to VC expression

1 files changed, 23 insertions, 0 deletions

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);