diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:01:52 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:01:52 -0400 |
commit | 41082463d783d6f8d8a5aaf69bf459b57bca6000 (patch) | |
tree | 8b9dca4b583b9cb1ea7ed220fe34d611217eb6cc /Test/aitest0 | |
parent | 64e8b33656140b87137d0662d9e6835e004d13c2 (diff) | |
parent | 8ed5dab22d8377924ee6282b83c1b1f8aa8f3573 (diff) |
Merge branch 'upstream' into dfsg_free
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 |