diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2016-01-04 19:26:36 -0800 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2016-01-04 19:26:36 -0800 |
| commit | 6fad4313b1a4e7f8e6cfcd12b92126a3d9ad58d0 (patch) | |
| tree | 7404eda3568a7f271ea2827f8e1603c139c5b452 /Source/AbsInt | |
| parent | a1c9e11736bda4bf8ea4bf431523b9b975b01670 (diff) | |
Added several test cases and some basic documentation for fp usage
Diffstat (limited to 'Source/AbsInt')
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 29 |
1 files changed, 26 insertions, 3 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index a27ae68d..0c954f9a 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;
}
}
}
@@ -209,7 +232,7 @@ namespace Microsoft.Boogie.AbstractInterpretation } else if (ty.IsReal) {
return Expr.Literal(Basetypes.BigDec.FromBigInt(n));
} else if (ty.IsFloat) {
- return Expr.Literal(Basetypes.BigFloat.FromBigInt(n));
+ return Expr.Literal(Basetypes.BigFloat.FromBigInt(n, ty.FloatExponent, ty.FloatMantissa));
} else {
Contract.Assume(ty.IsInt);
return Expr.Literal(Basetypes.BigNum.FromBigInt(n));
|