diff options
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 7 | ||||
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 5 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 2 |
3 files changed, 13 insertions, 1 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 1ac80970..b7c6ab5b 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -208,6 +208,8 @@ namespace Microsoft.Boogie.AbstractInterpretation return null;
} else if (ty.IsReal) {
return Expr.Literal(Basetypes.BigDec.FromBigInt(n));
+ } else if (ty.IsFloat) {
+ return Expr.Literal(Basetypes.FP32.FromBigInt(n));
} else {
Contract.Assume(ty.IsInt);
return Expr.Literal(Basetypes.BigNum.FromBigInt(n));
@@ -669,6 +671,11 @@ namespace Microsoft.Boogie.AbstractInterpretation ((BigDec)node.Val).FloorCeiling(out floor, out ceiling);
Lo = floor;
Hi = ceiling;
+ } else if (node.Val is FP32) {
+ BigInteger floor, ceiling;
+ ((BigDec)node.Val).FloorCeiling(out floor, out ceiling);
+ Lo = floor;
+ Hi = ceiling;
} else if (node.Val is bool) {
if ((bool)node.Val) {
// true
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 00306a5e..62145eed 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -356,6 +356,11 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return new LiteralExpr(Token.NoToken, value);
}
+ public static LiteralExpr Literal(FP32 value)
+ {
+ Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+ return new LiteralExpr(Token.NoToken, value);
+ }
private static LiteralExpr/*!*/ true_ = Literal(true);
public static LiteralExpr/*!*/ True {
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 4bf11e53..696a72ed 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -665,7 +665,7 @@ private class BvBounds : Expr { } else if (la.kind == 15) {
Get();
ty = new BasicType(t, SimpleType.Real);
- } else if (la.kind == 112837) {
+ } else if (la.kind == 135) {
Get();
ty = new BasicType(t, SimpleType.Float);
} else if (la.kind == 16) {
|