Merge branch 'dfsg_free'

1 files changed, 154 insertions, 0 deletions

diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index fc1bdd65..a23aaf8a 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -68,6 +68,18 @@ namespace Microsoft.Boogie.VCExprAST {
     Result VisitLabelOp(VCExprNAry node, Arg arg);
     Result VisitSelectOp(VCExprNAry node, Arg arg);
     Result VisitStoreOp(VCExprNAry node, Arg arg);
+    Result VisitFloatAddOp(VCExprNAry node, Arg arg);
+    Result VisitFloatSubOp(VCExprNAry node, Arg arg);
+    Result VisitFloatMulOp(VCExprNAry node, Arg arg);
+    Result VisitFloatDivOp(VCExprNAry node, Arg arg);
+    Result VisitFloatRemOp(VCExprNAry node, Arg arg);
+    Result VisitFloatMinOp(VCExprNAry node, Arg arg);
+    Result VisitFloatMaxOp(VCExprNAry node, Arg arg);
+    Result VisitFloatLeqOp(VCExprNAry node, Arg arg);
+    Result VisitFloatLtOp(VCExprNAry node, Arg arg);
+    Result VisitFloatGeqOp(VCExprNAry node, Arg arg);
+    Result VisitFloatGtOp(VCExprNAry node, Arg arg);
+    Result VisitFloatEqOp(VCExprNAry node, Arg arg);
     Result VisitBvOp(VCExprNAry node, Arg arg);
     Result VisitBvExtractOp(VCExprNAry node, Arg arg);
     Result VisitBvConcatOp(VCExprNAry node, Arg arg);
@@ -144,6 +156,78 @@ namespace Microsoft.Boogie.VCExprAST {
       throw new NotImplementedException();
     }
 
+    public Result VisitFloatAddOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatSubOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatMulOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatDivOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatRemOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatMinOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatMaxOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatLeqOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatLtOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatGeqOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatGtOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
+    public Result VisitFloatEqOp(VCExprNAry node, Arg arg)
+    {
+      Contract.Requires(node != null);
+      throw new NotImplementedException();
+    }
+
     public Result VisitBvOp(VCExprNAry node, Arg arg) {
       Contract.Requires(node != null);
       throw new NotImplementedException();
@@ -234,6 +318,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();
@@ -1438,6 +1528,65 @@ namespace Microsoft.Boogie.VCExprAST {
       //Contract.Requires(node != null);
       return StandardResult(node, arg);
     }
+    public virtual Result VisitFloatAddOp(VCExprNAry node, Arg arg) {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatSubOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatMulOp(VCExprNAry node, Arg arg)
+    {
+      //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 VisitFloatRemOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatMinOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatMaxOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatLeqOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatLtOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatGeqOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatGtOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
+    public virtual Result VisitFloatEqOp(VCExprNAry node, Arg arg)
+    {
+      //Contract.Requires(node != null);
+      return StandardResult(node, arg);
+    }
     public virtual Result VisitBvOp(VCExprNAry node, Arg arg) {
       //Contract.Requires(node != null);
       return StandardResult(node, arg);
@@ -1518,6 +1667,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);