From 812961fd5f0cb1ca17737bebd9d09a318d38ccb6 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 8 Apr 2014 08:31:05 -0700
Subject: Fixed bug in abstract interpretation over reals

---
 Source/AbsInt/IntervalDomain.cs | 17 ++++++++++++++---
 Source/Basetypes/BigDec.cs      |  5 +++++
 2 files changed, 19 insertions(+), 3 deletions(-)

(limited to 'Source')

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
@@ -47,6 +47,11 @@ namespace Microsoft.Basetypes {
       return new BigDec(v, 0);
     }
 
+    [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();
-- 
cgit v1.2.3