Changed the syntax reading of the float type

6 files changed, 51 insertions, 29 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 0dd78cbb..9d37476f 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -232,7 +232,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
       } else if (ty.IsReal) {
         return Expr.Literal(Basetypes.BigDec.FromBigInt(n));
       } else if (ty.IsFloat) {
-        return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatMantissa));
+        return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatSignificand));
       } else {
         Contract.Assume(ty.IsInt);
         return Expr.Literal(Basetypes.BigNum.FromBigInt(n));
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index 5fc5fd54..bc2b4391 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1724,10 +1724,10 @@ namespace Microsoft.Boogie {
             return Type.Real;
           }
           if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
-            return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);
+            return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatSignificand);
           }
           if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
-            return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);
+            return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatSignificand);
           }
           goto BAD_TYPE;
         case Opcode.Div:
@@ -1742,10 +1742,10 @@ namespace Microsoft.Boogie {
             return Type.Real;
           }
           if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
-            return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);
+            return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatSignificand);
           }
           if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
-            return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);
+            return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatSignificand);
           }
           goto BAD_TYPE;
         case Opcode.Pow:
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index 96de5c0b..08cf37cc 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -340,12 +340,12 @@ namespace Microsoft.Boogie {
         } // Type.FloatExponent should never be called
       }
     }
-    public virtual int FloatMantissa {
+    public virtual int FloatSignificand {
       get {
         {
           Contract.Assert(false);
           throw new cce.UnreachableException();
-        } // Type.FloatMantissa should never be called
+        } // Type.FloatSignificand should never be called
       }
     }
     public virtual bool IsBv {
@@ -1046,20 +1046,20 @@ namespace Microsoft.Boogie {
 
   //Note that the functions in this class were directly copied from the BV class just below
   public class FloatType : Type { 
-    public readonly int Mantissa; //Size of mantissa in bits
+    public readonly int Significand; //Size of Significand in bits
     public readonly int Exponent; //Size of exponent in bits
 
-    public FloatType(IToken token, int exponent, int mantissa)
+    public FloatType(IToken token, int significand, int exponent)
       : base(token) {
       Contract.Requires(token != null);
+      Significand = significand;
       Exponent = exponent;
-      Mantissa = mantissa;
     }
 
-    public FloatType(int exponent, int mantissa)
+    public FloatType(int significand, int exponent)
       : base(Token.NoToken) {
+      Significand = significand;
       Exponent = exponent;
-      Mantissa = mantissa;
     }
 
     //-----------  Cloning  ----------------------------------
@@ -1094,7 +1094,7 @@ namespace Microsoft.Boogie {
     public override string ToString()
     {
       Contract.Ensures(Contract.Result<string>() != null);
-      return "float (" + Exponent + " " + Mantissa + ")";
+      return "float (" + Exponent + " " + Significand + ")";
     }
 
     //-----------  Equality  ----------------------------------
@@ -1105,7 +1105,7 @@ namespace Microsoft.Boogie {
                                 List<TypeVariable>/*!*/ thatBoundVariables)
     {
       FloatType thatFloatType = TypeProxy.FollowProxy(that.Expanded) as FloatType;
-      return thatFloatType != null && this.Mantissa == thatFloatType.Mantissa && this.Exponent == thatFloatType.Exponent;
+      return thatFloatType != null && this.Significand == thatFloatType.Significand && this.Exponent == thatFloatType.Exponent;
     }
 
     //-----------  Unification of types  -----------
@@ -1141,7 +1141,7 @@ namespace Microsoft.Boogie {
     [Pure]
     public override int GetHashCode(List<TypeVariable> boundVariables)
     {
-      return this.Mantissa.GetHashCode() + this.Exponent.GetHashCode();
+      return this.Significand.GetHashCode() + this.Exponent.GetHashCode();
     }
 
     //-----------  Resolution  ----------------------------------
@@ -1181,9 +1181,9 @@ namespace Microsoft.Boogie {
         return true;
       }
     }
-    public override int FloatMantissa {
+    public override int FloatSignificand {
       get {
-        return Mantissa;
+        return Significand;
       }
     }
     public override int FloatExponent {
@@ -1481,7 +1481,7 @@ Contract.Requires(that != null);
     public override Type ResolveType(ResolutionContext rc) {
       //Contract.Requires(rc != null);
       Contract.Ensures(Contract.Result<Type>() != null);
-      // first case: the type name denotes a bitvector-type
+      // first case: the type name denotes a bitvector-type or float-type
       if (Name.StartsWith("bv") && Name.Length > 2) {
         bool is_bv = true;
         for (int i = 2; i < Name.Length; ++i) {
@@ -1500,6 +1500,28 @@ Contract.Requires(that != null);
         }
       }
 
+      if (Name.StartsWith("float") && Name.Length > 5)
+      {
+        bool is_float = true;
+        int i = 5;
+        for (; is_float && Name[i] != 'e'; i++)
+          if (i >= Name.Length-1 || !char.IsDigit(Name[i])) //There must be an e
+            is_float = false;
+        int mid = i;
+        i++;
+        for (; i < Name.Length && is_float; i++)
+          if (!char.IsDigit(Name[i]))
+            is_float = false;
+        if (is_float) {
+          if (Arguments.Count > 0) {
+            rc.Error(this,
+                     "float types must not be applied to arguments: {0}",
+                     Name);
+          }
+          return new FloatType(tok, int.Parse(Name.Substring(5, mid-5)), int.Parse(Name.Substring(mid+1)));
+        }
+      }
+
       // second case: the identifier is resolved to a type variable
       TypeVariable var = rc.LookUpTypeBinder(Name);
       if (var != null) {
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 99dd849d..7b2525f7 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -146,7 +146,7 @@ namespace Microsoft.Boogie.SMTLib
       else if (t.IsReal)
         return "Real";
       else if (t.IsFloat)
-        return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")";
+        return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatSignificand + ")";
       else if (t.IsBv) {
         return "(_ BitVec " + t.BvBits + ")";
       } else {
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index a3364ad8..1bcb6afc 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -1087,7 +1087,7 @@ namespace Microsoft.Boogie.VCExprAST {
             return Gen.Function(VCExpressionGenerator.AddROp, args);
           }
           else { //t is float
-            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "+"), args);
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "+"), args);
           }
         case BinaryOperator.Opcode.Sub:
           if (t.IsInt) {
@@ -1097,7 +1097,7 @@ namespace Microsoft.Boogie.VCExprAST {
             return Gen.Function(VCExpressionGenerator.SubROp, args);
           }
           else { //t is float
-            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "-"), args);
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "-"), args);
           }
         case BinaryOperator.Opcode.Mul:
           if (t.IsInt) {
@@ -1108,7 +1108,7 @@ namespace Microsoft.Boogie.VCExprAST {
           }
           else
           { //t is float
-            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "*"), args);
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "*"), args);
           }
         case BinaryOperator.Opcode.Div:
           return Gen.Function(VCExpressionGenerator.DivIOp, args);
@@ -1116,7 +1116,7 @@ namespace Microsoft.Boogie.VCExprAST {
           return Gen.Function(VCExpressionGenerator.ModOp, args);
         case BinaryOperator.Opcode.RealDiv:
           if (t.IsFloat) {
-            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "/"), args);
+            return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatSignificand, "/"), args);
           }
           VCExpr arg0 = cce.NonNull(args[0]);
           VCExpr arg1 = cce.NonNull(args[1]);
@@ -1133,25 +1133,25 @@ namespace Microsoft.Boogie.VCExprAST {
         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.FloatMantissa, "=="), args);
+            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.FloatMantissa, "<"), args);
+            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.FloatMantissa, "<="), args);
+            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.FloatMantissa, ">="), args);
+            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.FloatMantissa, ">"), args);
+            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);
diff --git a/Test/floats/float0.bpl b/Test/floats/float0.bpl
index b1a240be..1a642835 100644
--- a/Test/floats/float0.bpl
+++ b/Test/floats/float0.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -proverWarnings:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-procedure foo(x : real) returns (r : float<8, 24>)
+procedure foo(x : real) returns (r : float8e24)
 {
 	r := 15;  // Error
 	r := 15.0;  // Error