Skip to content
Snippets Groups Projects
Commit c1701ced authored by Loïc Correnson's avatar Loïc Correnson Committed by Allan Blanchard
Browse files

[wp] update test

parent 0552c3c2
No related branches found
No related tags found
No related merge requests found
/*@
requires 0 <= n;
*/
void f (int n) {
//@ loop variant n - i;
/*@
loop invariant 0 <= i <= n;
loop assigns i;
loop variant n - i;
*/
for (int i = 0; i < n; i++) {
/*@ assert \at(i,LoopEntry) == 0; */
int j = 0;
//@ loop variant i - j;
/*@
loop invariant 0 <= j <= i;
loop assigns j;
loop variant i - j;
*/
while (j++ < i) {
/*@ assert \at(j,LoopEntry) == 0; */
/*@ assert \at(j,LoopCurrent) + 1 == j; */
......
......@@ -4,53 +4,95 @@
[wp] [CFG] Goal f_exits : Valid (Unreachable)
[wp] [CFG] Goal f_terminates : Valid (Trivial)
[wp] Warning: Missing RTE guards
[wp] loopextra.i:8: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] loopextra.i:4: Warning:
Missing assigns clause (assigns 'everything' instead)
------------------------------------------------------------
Function f
------------------------------------------------------------
Goal Assertion (file loopextra.i, line 5):
Goal Preservation of Invariant (file loopextra.i, line 6):
Prove: true.
------------------------------------------------------------
Goal Assertion (file loopextra.i, line 9):
Goal Establishment of Invariant (file loopextra.i, line 6):
Prove: true.
------------------------------------------------------------
Goal Assertion (file loopextra.i, line 10):
Goal Assertion (file loopextra.i, line 11):
Prove: true.
------------------------------------------------------------
Goal Decreasing of Loop variant at loop (file loopextra.i, line 4):
Assume {
Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(j) /\ is_sint32(n_1) /\
is_sint32(n) /\ is_sint32(1 + i_1).
(* Then *)
Have: i < n_1.
(* Else *)
Have: i_1 <= j.
}
Prove: (i + n) <= (i_1 + n_1).
Goal Preservation of Invariant (file loopextra.i, line 14):
Prove: true.
------------------------------------------------------------
Goal Establishment of Invariant (file loopextra.i, line 14):
Prove: true.
------------------------------------------------------------
Goal Assertion (file loopextra.i, line 19):
Prove: true.
------------------------------------------------------------
Goal Assertion (file loopextra.i, line 20):
Prove: true.
------------------------------------------------------------
Goal Loop assigns (file loopextra.i, line 7) (1/4):
Prove: true.
------------------------------------------------------------
Goal Loop assigns (file loopextra.i, line 7) (2/4):
Effect at line 18
Prove: true.
------------------------------------------------------------
Goal Loop assigns (file loopextra.i, line 7) (3/4):
Effect at line 18
Prove: true.
------------------------------------------------------------
Goal Loop assigns (file loopextra.i, line 7) (4/4):
Effect at line 18
Prove: true.
------------------------------------------------------------
Goal Loop assigns (file loopextra.i, line 15) (1/2):
Prove: true.
------------------------------------------------------------
Goal Loop assigns (file loopextra.i, line 15) (2/2):
Effect at line 18
Prove: true.
------------------------------------------------------------
Goal Decreasing of Loop variant at loop (file loopextra.i, line 10):
Prove: true.
------------------------------------------------------------
Goal Positivity of Loop variant at loop (file loopextra.i, line 4):
Goal Positivity of Loop variant at loop (file loopextra.i, line 10):
Prove: true.
------------------------------------------------------------
Goal Decreasing of Loop variant at loop (file loopextra.i, line 8):
Goal Decreasing of Loop variant at loop (file loopextra.i, line 18):
Prove: true.
------------------------------------------------------------
Goal Positivity of Loop variant at loop (file loopextra.i, line 8):
Goal Positivity of Loop variant at loop (file loopextra.i, line 18):
Prove: true.
------------------------------------------------------------
......@@ -4,24 +4,29 @@
[wp] [CFG] Goal f_exits : Valid (Unreachable)
[wp] [CFG] Goal f_terminates : Valid (Trivial)
[wp] Warning: Missing RTE guards
[wp] loopextra.i:8: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] loopextra.i:4: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 7 goals scheduled
[wp] 17 goals scheduled
[wp] [Valid] typed_f_loop_invariant_preserved (Qed)
[wp] [Valid] typed_f_loop_invariant_established (Qed)
[wp] [Valid] typed_f_assert (Qed)
[wp] [Valid] typed_f_loop_invariant_2_preserved (Qed)
[wp] [Valid] typed_f_loop_invariant_2_established (Qed)
[wp] [Valid] typed_f_assert_2 (Qed)
[wp] [Valid] typed_f_assert_3 (Qed)
[wp] [Unsuccess] typed_f_loop_variant_decrease (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_loop_assigns_part1 (Qed)
[wp] [Valid] typed_f_loop_assigns_part2 (Qed)
[wp] [Valid] typed_f_loop_assigns_part3 (Qed)
[wp] [Valid] typed_f_loop_assigns_part4 (Qed)
[wp] [Valid] typed_f_loop_assigns_2_part1 (Qed)
[wp] [Valid] typed_f_loop_assigns_2_part2 (Qed)
[wp] [Valid] typed_f_loop_variant_decrease (Qed)
[wp] [Valid] typed_f_loop_variant_positive (Qed)
[wp] [Valid] typed_f_loop_variant_2_decrease (Qed)
[wp] [Valid] typed_f_loop_variant_2_positive (Qed)
[wp] Proved goals: 8 / 9
[wp] Proved goals: 19 / 19
Terminating: 1
Unreachable: 1
Qed: 6
Unsuccess: 1
Qed: 17
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f 6 - 7 85.7%
f 17 - 17 100%
------------------------------------------------------------
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment