summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/AbsInt/IntervalDomain.cs2
-rw-r--r--Source/Core/AbsyExpr.cs8
-rw-r--r--Source/Core/AbsyType.cs48
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs2
-rw-r--r--Source/VCExpr/Boogie2VCExpr.cs18
5 files changed, 50 insertions, 28 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);
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 01:37:41 +0000