diff options
author | RustanLeino <leino@microsoft.com> | 2016-08-17 13:40:57 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-08-17 13:40:57 -0700 |
commit | 12d1543333babd202d76e259418dd03c0c7c56c3 (patch) | |
tree | 69bd181ccb97621378ab630a1357bd5583cc96a8 /Source/AbsInt/IntervalDomain.cs | |
parent | 529b1bc37b6da3f40dc85aef4cf252e9c98dd566 (diff) | |
parent | 2b64144fb02b68d00188ee81c27afa5fbc026b5b (diff) |
Merge pull request #35 from Checkmate50/master
Floating Point Support
Diffstat (limited to 'Source/AbsInt/IntervalDomain.cs')
-rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 34 |
1 files changed, 32 insertions, 2 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 2fd37463..1d35b735 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -180,8 +180,7 @@ namespace Microsoft.Boogie.AbstractInterpretation } } return e; - } else { - Contract.Assert(V.TypedIdent.Type.IsReal); + } else if (V.TypedIdent.Type.IsReal){ Expr e = Expr.True; if (Lo != null && Hi != null && Lo == Hi) { // produce an equality @@ -199,6 +198,30 @@ namespace Microsoft.Boogie.AbstractInterpretation } } return e; + } else { + Contract.Assert(V.TypedIdent.Type.IsFloat); + Expr e = Expr.True; + if (Lo != null && Hi != null && Lo == Hi) + { + // produce an equality + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplEq(ide, NumberToExpr((BigInteger)Lo, V.TypedIdent.Type))); + } + else + { + // produce a (possibly empty) conjunction of inequalities + if (Lo != null) + { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(NumberToExpr((BigInteger)Lo, V.TypedIdent.Type), ide)); + } + if (Hi != null) + { + var ide = new IdentifierExpr(Token.NoToken, V); + e = Expr.And(e, BplLe(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type))); + } + } + return e; } } } @@ -208,6 +231,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.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatSignificand)); } else { Contract.Assume(ty.IsInt); return Expr.Literal(Basetypes.BigNum.FromBigInt(n)); @@ -669,6 +694,11 @@ namespace Microsoft.Boogie.AbstractInterpretation ((BigDec)node.Val).FloorCeiling(out floor, out ceiling); Lo = floor; Hi = ceiling; + } else if (node.Val is BigFloat) { + BigInteger floor, ceiling; + ((BigFloat)node.Val).FloorCeiling(out floor, out ceiling); + Lo = floor; + Hi = ceiling; } else if (node.Val is bool) { if ((bool)node.Val) { // true |