From 0776b808b14e62833b3eac1c30c8ac8cc7e62c20 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Mon, 20 Apr 2015 03:44:03 -0600 Subject: added float tipe to AbsyExpr and IntervalDomain. The methods added may require later modification --- Source/AbsInt/IntervalDomain.cs | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'Source/AbsInt') 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 -- cgit v1.2.3