Improve precision of abstract interpreter for modulo operations.

alexanderjsummers · Dec 29, 2015 · dd8e69b · dd8e69b
1 parent 1c16dc8
commit dd8e69b
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 1 deletion.
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
@@ -884,6 +884,10 @@ public override Expr VisitNAryExpr(NAryExpr node) {
               if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
                 Lo = BigInteger.Zero;
                 Hi = hi1;
+                if (lo0 < lo1 && hi0 != null && hi0 < lo1) {
+                  Lo = lo0;
+                  Hi = hi0;
+                }
               }
               break;
             case BinaryOperator.Opcode.RealDiv:

diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
@@ -332,3 +332,18 @@ procedure W0(N: real)
     assert N - i <= bf0 - 1.0;
   }
 }
+
+// mod
+
+procedure Mod0(n: int)
+  requires 10 < n;
+{
+    var i: int;
+
+    i := 0;
+    while (i < 10)
+    {
+        i := (i mod n) + 1;
+    }
+    assert i == 10;
+}
diff --git a/Test/aitest0/Intervals.bpl.expect b/Test/aitest0/Intervals.bpl.expect
@@ -54,4 +54,4 @@ Execution trace:
     Intervals.bpl(303,3): anon3_LoopHead
     Intervals.bpl(303,3): anon3_LoopDone
 
-Boogie program verifier finished with 16 verified, 11 errors
+Boogie program verifier finished with 17 verified, 11 errors