diff options
| author |  Valentin Wüstholz <wuestholz@gmail.com> | 2015-12-28 20:22:03 -0600 |
|---|---|---|
| committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-12-28 20:22:03 -0600 |
| commit | dd8e69b7b71a9375b7206a70633deae234175ef8 (patch) | |
| tree | 3ec3a9796afb6ce8c808a407c672237ce94f4b78 | |
| parent | 1c16dc829c81426e17427c0d103ed831a48f1f81 (diff) | |
Improve precision of abstract interpreter for modulo operations.
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 4 | ||||
| -rw-r--r-- | Test/aitest0/Intervals.bpl | 15 | ||||
| -rw-r--r-- | Test/aitest0/Intervals.bpl.expect | 2 |
3 files changed, 20 insertions, 1 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index ee9d632b..2fd37463 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -884,6 +884,10 @@ namespace Microsoft.Boogie.AbstractInterpretation 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 index fddce05a..8d40b81d 100644 --- 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 index a0769ec5..980593a9 100644 --- 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 |