diff options
| author |  Dietrich <dgeisler50@gmail.com> | 2015-04-20 03:44:03 -0600 |
|---|---|---|
| committer | Dietrich <dgeisler50@gmail.com> | 2015-04-20 03:44:03 -0600 |
| commit | 0776b808b14e62833b3eac1c30c8ac8cc7e62c20 (patch) | |
| tree | 4d78f194944b988c25e05ec13b438f0284bfc422 /Source/AbsInt | |
| parent | b5f62842c113ec93dee7f9ac067ae6d410e7bc29 (diff) | |
added float tipe to AbsyExpr and IntervalDomain. The methods added may require later modification
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
|