diff options
Diffstat (limited to 'Source/AbsInt')
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 7 |
1 files changed, 7 insertions, 0 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
|