diff options
| author |  Rustan Leino <unknown> | 2014-04-08 08:31:05 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-08 08:31:05 -0700 |
| commit | 812961fd5f0cb1ca17737bebd9d09a318d38ccb6 (patch) | |
| tree | 84d98104bd72072cecae8b030c36320ac3ac7e5e /Source | |
| parent | 55bdb8b4ba8c49654fae37d74b34cbc4597c08fb (diff) | |
Fixed bug in abstract interpretation over reals
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 17 | ||||
| -rw-r--r-- | Source/Basetypes/BigDec.cs | 5 |
2 files changed, 19 insertions, 3 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 4b5ae903..640a50fc 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -166,16 +166,16 @@ namespace Microsoft.Boogie.AbstractInterpretation if (Lo != null && Hi != null && Lo + 1 == Hi) {
// produce an equality
var ide = new IdentifierExpr(Token.NoToken, V);
- e = Expr.And(e, BplEq(ide, Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Lo))));
+ 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(Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Lo)), ide));
+ 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, BplLt(ide, Expr.Literal(Basetypes.BigNum.FromBigInt((BigInteger)Hi))));
+ e = Expr.And(e, BplLt(ide, NumberToExpr((BigInteger)Hi, V.TypedIdent.Type)));
}
}
return e;
@@ -183,6 +183,17 @@ namespace Microsoft.Boogie.AbstractInterpretation }
}
+ static Expr NumberToExpr(BigInteger n, Type ty) {
+ if (n == null) {
+ return null;
+ } else if (ty.IsReal) {
+ return Expr.Literal(Basetypes.BigDec.FromBigInt(n));
+ } else {
+ Contract.Assume(ty.IsInt);
+ return Expr.Literal(Basetypes.BigNum.FromBigInt(n));
+ }
+ }
+
List<BigInteger> upThresholds; // invariant: thresholds are sorted
List<BigInteger> downThresholds; // invariant: thresholds are sorted
diff --git a/Source/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs index 301774f6..beb9ec54 100644 --- a/Source/Basetypes/BigDec.cs +++ b/Source/Basetypes/BigDec.cs @@ -48,6 +48,11 @@ namespace Microsoft.Basetypes { }
[Pure]
+ public static BigDec FromBigInt(BIM v) {
+ return new BigDec(v, 0);
+ }
+
+ [Pure]
public static BigDec FromString(string v) {
if (v == null) throw new FormatException();
|