1 files changed, 38 insertions, 8 deletions

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 0c817756..1bcb6afc 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -334,7 +334,10 @@ namespace Microsoft.Boogie.VCExprAST {
         return Gen.Integer(node.asBigNum);
       } else if (node.Val is BigDec) {
         return Gen.Real(node.asBigDec);
-      } else if (node.Val is BvConst) {
+      } else if (node.Val is BigFloat) {
+        return Gen.Float(node.asBigFloat);
+      }
+      else if (node.Val is BvConst) {
         return Gen.Bitvector((BvConst)node.Val);
       } else {
         System.Diagnostics.Debug.Assert(false, "unknown kind of literal " + node.tok.ToString());
@@ -1002,9 +1005,12 @@ namespace Microsoft.Boogie.VCExprAST {
         if (cce.NonNull(e.Type).IsInt) {
           return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e);
         }
-        else {
+        else {// if (cce.NonNull(e.Type).IsReal) {
           return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e);
         }
+        //else  {//is float
+          //return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO(8, 23)), e);
+        //} 
       }
       else {
         return Gen.Not(this.args);
@@ -1070,34 +1076,48 @@ namespace Microsoft.Boogie.VCExprAST {
       Contract.Requires(cce.NonNullElements(args));
       Contract.Ensures(Contract.Result<VCExpr>() != null);
       Contract.Assert(args.Count == 2);
+      Type t = cce.NonNull(cce.NonNull(args[0]).Type);
 
       switch (app.Op) {
         case BinaryOperator.Opcode.Add:
-          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+          if (t.IsInt) {
             return Gen.Function(VCExpressionGenerator.AddIOp, args);
           }
-          else {
+          else if (t.IsReal) {
             return Gen.Function(VCExpressionGenerator.AddROp, args);
           }
+          else { //t is float
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "+"), args);
+          }
         case BinaryOperator.Opcode.Sub:
-          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+          if (t.IsInt) {
             return Gen.Function(VCExpressionGenerator.SubIOp, args);
           }
-          else {
+          else if (t.IsReal) {
             return Gen.Function(VCExpressionGenerator.SubROp, args);
           }
+          else { //t is float
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "-"), args);
+          }
         case BinaryOperator.Opcode.Mul:
-          if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+          if (t.IsInt) {
             return Gen.Function(VCExpressionGenerator.MulIOp, args);
           }
-          else {
+          else if (t.IsReal) {
             return Gen.Function(VCExpressionGenerator.MulROp, args);
           }
+          else
+          { //t is float
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "*"), args);
+          }
         case BinaryOperator.Opcode.Div:
           return Gen.Function(VCExpressionGenerator.DivIOp, args);
         case BinaryOperator.Opcode.Mod:
           return Gen.Function(VCExpressionGenerator.ModOp, args);
         case BinaryOperator.Opcode.RealDiv:
+          if (t.IsFloat) {
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "/"), args);
+          }
           VCExpr arg0 = cce.NonNull(args[0]);
           VCExpr arg1 = cce.NonNull(args[1]);
           if (cce.NonNull(arg0.Type).IsInt) {
@@ -1112,16 +1132,26 @@ namespace Microsoft.Boogie.VCExprAST {
         case BinaryOperator.Opcode.Eq:
         case BinaryOperator.Opcode.Iff:
           // we don't distinguish between equality and equivalence at this point
+          if (t.IsFloat)
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "=="), args);
           return Gen.Function(VCExpressionGenerator.EqOp, args);
         case BinaryOperator.Opcode.Neq:
           return Gen.Function(VCExpressionGenerator.NeqOp, args);
         case BinaryOperator.Opcode.Lt:
+          if (t.IsFloat)
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "<"), args);
           return Gen.Function(VCExpressionGenerator.LtOp, args);
         case BinaryOperator.Opcode.Le:
+          if (t.IsFloat)
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "<="), args);
           return Gen.Function(VCExpressionGenerator.LeOp, args);
         case BinaryOperator.Opcode.Ge:
+          if (t.IsFloat)
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, ">="), args);
           return Gen.Function(VCExpressionGenerator.GeOp, args);
         case BinaryOperator.Opcode.Gt:
+          if (t.IsFloat)
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, ">"), args);
           return Gen.Function(VCExpressionGenerator.GtOp, args);
         case BinaryOperator.Opcode.Imp:
           return Gen.Function(VCExpressionGenerator.ImpliesOp, args);