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 /Test | |
| parent | 1c16dc829c81426e17427c0d103ed831a48f1f81 (diff) | |
Improve precision of abstract interpreter for modulo operations.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/aitest0/Intervals.bpl | 15 | ||||
| -rw-r--r-- | Test/aitest0/Intervals.bpl.expect | 2 |
2 files changed, 16 insertions, 1 deletions
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 |