From af8621462cf6b25a6dd29b63ed251629109d6bfb Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Sat, 16 Jul 2016 02:49:06 -0600 Subject: Changed the syntax reading of the float type --- Source/Core/AbsyExpr.cs | 8 ++++---- Source/Core/AbsyType.cs | 48 +++++++++++++++++++++++++++++++++++------------- 2 files changed, 39 insertions(+), 17 deletions(-) (limited to 'Source/Core') 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() != null); - return "float (" + Exponent + " " + Mantissa + ")"; + return "float (" + Exponent + " " + Significand + ")"; } //----------- Equality ---------------------------------- @@ -1105,7 +1105,7 @@ namespace Microsoft.Boogie { List/*!*/ 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 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() != 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) { -- cgit v1.2.3