diff options
Diffstat (limited to 'Test/aitest0')
-rw-r--r-- | Test/aitest0/Intervals.bpl | 15 | ||||
-rw-r--r-- | Test/aitest0/Intervals.bpl.expect | 2 | ||||
-rw-r--r-- | Test/aitest0/Issue25.bpl | 14 | ||||
-rw-r--r-- | Test/aitest0/Issue25.bpl.expect | 8 |
4 files changed, 38 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 diff --git a/Test/aitest0/Issue25.bpl b/Test/aitest0/Issue25.bpl new file mode 100644 index 00000000..6ffcd113 --- /dev/null +++ b/Test/aitest0/Issue25.bpl @@ -0,0 +1,14 @@ +// RUN: %boogie -infer:j "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +const N: int; +axiom 0 <= N; + +procedure vacuous_post() +ensures (forall k, l: int :: 0 <= k && k <= l && l < N ==> N < N); // Used to verify at some point (see https://github.com/boogie-org/boogie/issues/25). +{ +var x: int; +x := -N; +while (x != x) { +} +} diff --git a/Test/aitest0/Issue25.bpl.expect b/Test/aitest0/Issue25.bpl.expect new file mode 100644 index 00000000..f56502e2 --- /dev/null +++ b/Test/aitest0/Issue25.bpl.expect @@ -0,0 +1,8 @@ +Issue25.bpl(12,1): Error BP5003: A postcondition might not hold on this return path. +Issue25.bpl(8,1): Related location: This is the postcondition that might not hold. +Execution trace: + Issue25.bpl(11,3): anon0 + Issue25.bpl(12,1): anon2_LoopHead + Issue25.bpl(12,1): anon2_LoopDone + +Boogie program verifier finished with 0 verified, 1 error |