Commit ea9f432c authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Merge branch 'feature/wp/stats' into 'master'

[wp] updated oracles

See merge request frama-c/meta!70
parents 2503be04 4b14c8bc
......@@ -9,20 +9,20 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 11 goals scheduled
[wp] [Qed] Goal typed_f1_ensures_inv_big_meta : Valid
[wp] [Qed] Goal typed_f1_assigns : Valid
[wp] [Qed] Goal typed_f2_ensures_inv_big_meta : Valid
[wp] [Qed] Goal typed_f2_assigns : Valid
[wp] [Qed] Goal typed_f3_assigns : Valid
[wp] [Qed] Goal typed_f5_assigns : Valid
[wp] [Qed] Goal typed_f4_assigns_exit : Valid
[wp] [Qed] Goal typed_f4_assigns_normal : Valid
[wp] [Alt-Ergo] Goal typed_f4_call_f2_requires_inv_big_meta : Unsuccess
[wp] [Qed] Goal typed_f6_assigns_exit : Valid
[wp] [Qed] Goal typed_f6_assigns_normal : Valid
[wp] [Valid] typed_f1_ensures_inv_big_meta (Qed)
[wp] [Valid] typed_f1_assigns (Qed)
[wp] [Valid] typed_f2_ensures_inv_big_meta (Qed)
[wp] [Valid] typed_f2_assigns (Qed)
[wp] [Valid] typed_f3_assigns (Qed)
[wp] [Valid] typed_f5_assigns (Qed)
[wp] [Valid] typed_f4_assigns_exit (Qed)
[wp] [Valid] typed_f4_assigns_normal (Qed)
[wp] [Unsuccess] typed_f4_call_f2_requires_inv_big_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_f6_assigns_exit (Qed)
[wp] [Valid] typed_f6_assigns_normal (Qed)
[wp] Proved goals: 10 / 11
Qed: 10
Alt-Ergo: 0 (unsuccess: 1)
Qed: 10
Unsuccess: 1
/* Generated by Frama-C */
int A;
int B;
......
......@@ -7,14 +7,14 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
[wp] [Qed] Goal typed_f3_assigns : Valid
[wp] [Qed] Goal typed_f2_assigns_exit : Valid
[wp] [Qed] Goal typed_f2_assigns_normal : Valid
[wp] [Qed] Goal typed_f1_assigns_exit : Valid
[wp] [Qed] Goal typed_f1_assigns_normal : Valid
[wp] [Qed] Goal typed_f0_assert : Valid
[wp] [Qed] Goal typed_f0_assigns_exit : Valid
[wp] [Qed] Goal typed_f0_assigns_normal : Valid
[wp] [Valid] typed_f3_assigns (Qed)
[wp] [Valid] typed_f2_assigns_exit (Qed)
[wp] [Valid] typed_f2_assigns_normal (Qed)
[wp] [Valid] typed_f1_assigns_exit (Qed)
[wp] [Valid] typed_f1_assigns_normal (Qed)
[wp] [Valid] typed_f0_assert (Qed)
[wp] [Valid] typed_f0_assigns_exit (Qed)
[wp] [Valid] typed_f0_assigns_normal (Qed)
[wp] Proved goals: 8 / 8
Qed: 8
/* Generated by Frama-C */
......
......@@ -5,18 +5,18 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_f1_assert_m1_meta : Valid
[wp] [Qed] Goal typed_f1_assert_m2_meta : Valid
[wp] [Qed] Goal typed_f1_assigns : Valid
[wp] [Qed] Goal typed_f2_assert_m3_meta : Valid
[wp] [Alt-Ergo] Goal typed_f2_assert_m2_meta : Unsuccess
[wp] [Qed] Goal typed_f2_assigns : Valid
[wp] [Qed] Goal typed_f3_assert_m3_meta : Valid
[wp] [Alt-Ergo] Goal typed_f3_assert_m3_meta_2 : Unsuccess
[wp] [Qed] Goal typed_f3_assigns : Valid
[wp] [Valid] typed_f1_assert_m1_meta (Qed)
[wp] [Valid] typed_f1_assert_m2_meta (Qed)
[wp] [Valid] typed_f1_assigns (Qed)
[wp] [Valid] typed_f2_assert_m3_meta (Qed)
[wp] [Unsuccess] typed_f2_assert_m2_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_assigns (Qed)
[wp] [Valid] typed_f3_assert_m3_meta (Qed)
[wp] [Unsuccess] typed_f3_assert_m3_meta_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_assigns (Qed)
[wp] Proved goals: 7 / 9
Qed: 7
Alt-Ergo: 0 (unsuccess: 2)
Qed: 7
Unsuccess: 2
/* Generated by Frama-C */
enum Foo {
ONE = 0,
......
......@@ -5,10 +5,10 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_f1_assigns : Valid
[wp] [Qed] Goal typed_main_assert : Valid
[wp] [Qed] Goal typed_main_assigns_exit : Valid
[wp] [Qed] Goal typed_main_assigns_normal : Valid
[wp] [Valid] typed_f1_assigns (Qed)
[wp] [Valid] typed_main_assert (Qed)
[wp] [Valid] typed_main_assigns_exit (Qed)
[wp] [Valid] typed_main_assigns_normal (Qed)
[wp] Proved goals: 4 / 4
Qed: 4
/* Generated by Frama-C */
......
......@@ -5,47 +5,47 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 39 goals scheduled
[wp] [Qed] Goal typed_RW_ensures_strong_invariant_5_meta : Valid
[wp] [Qed] Goal typed_RW_assert_reading_2_meta : Valid
[wp] [Qed] Goal typed_RW_assert_writing_4_meta : Valid
[wp] [Qed] Goal typed_RW_assert_strong_invariant_5_meta : Valid
[wp] [Qed] Goal typed_RW_assigns : Valid
[wp] [Qed] Goal typed_compute_ensures_strong_invariant_5_meta : Valid
[wp] [Qed] Goal typed_compute_assert_writing_3_meta : Valid
[wp] [Qed] Goal typed_compute_assert_writing_3_meta_2 : Valid
[wp] [Qed] Goal typed_compute_assert_reading_1_meta : Valid
[wp] [Qed] Goal typed_compute_assert_reading_2_meta : Valid
[wp] [Qed] Goal typed_compute_assert_strong_invariant_5_meta : Valid
[wp] [Qed] Goal typed_compute_assert_strong_invariant_5_meta_2 : Valid
[wp] [Qed] Goal typed_compute_assigns_part1 : Valid
[wp] [Qed] Goal typed_compute_assigns_part2 : Valid
[wp] [Qed] Goal typed_compute_assigns_part3 : Valid
[wp] [Qed] Goal typed_compute_assigns_part4 : Valid
[wp] [Alt-Ergo] Goal typed_compute_assigns_part5 : Valid
[wp] [Qed] Goal typed_compute_assigns_part6 : Valid
[wp] [Qed] Goal typed_main_requires_strong_invariant_5_meta : Valid
[wp] [Qed] Goal typed_main_ensures_strong_invariant_5_meta : Valid
[wp] [Qed] Goal typed_main_assert_writing_3_meta : Valid
[wp] [Qed] Goal typed_main_assert_writing_4_meta : Valid
[wp] [Qed] Goal typed_main_assert_writing_6_meta : Valid
[wp] [Qed] Goal typed_main_assert_strong_invariant_5_meta : Valid
[wp] [Qed] Goal typed_main_assert_strong_invariant_5_meta_2 : Valid
[wp] [Qed] Goal typed_main_assert_strong_invariant_5_meta_3 : Valid
[wp] [Qed] Goal typed_main_assert_strong_invariant_5_meta_4 : Valid
[wp] [Qed] Goal typed_main_assigns_exit_part1 : Valid
[wp] [Qed] Goal typed_main_assigns_exit_part2 : Valid
[wp] [Qed] Goal typed_main_assigns_exit_part3 : Valid
[wp] [Qed] Goal typed_main_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_main_assigns_normal_part2 : Valid
[wp] [Qed] Goal typed_main_assigns_normal_part3 : Valid
[wp] [Qed] Goal typed_main_assigns_normal_part4 : Valid
[wp] [Qed] Goal typed_main_call_RW_requires : Valid
[wp] [Qed] Goal typed_main_call_RW_requires_2 : Valid
[wp] [Qed] Goal typed_main_call_RW_requires_strong_invariant_5_meta : Valid
[wp] [Qed] Goal typed_main_call_compute_requires : Valid
[wp] [Qed] Goal typed_main_call_compute_requires_strong_invariant_5_meta : Valid
[wp] [Valid] typed_RW_ensures_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_RW_assert_reading_2_meta (Qed)
[wp] [Valid] typed_RW_assert_writing_4_meta (Qed)
[wp] [Valid] typed_RW_assert_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_RW_assigns (Qed)
[wp] [Valid] typed_compute_ensures_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_compute_assert_writing_3_meta (Qed)
[wp] [Valid] typed_compute_assert_writing_3_meta_2 (Qed)
[wp] [Valid] typed_compute_assert_reading_1_meta (Qed)
[wp] [Valid] typed_compute_assert_reading_2_meta (Qed)
[wp] [Valid] typed_compute_assert_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_compute_assert_strong_invariant_5_meta_2 (Qed)
[wp] [Valid] typed_compute_assigns_part1 (Qed)
[wp] [Valid] typed_compute_assigns_part2 (Qed)
[wp] [Valid] typed_compute_assigns_part3 (Qed)
[wp] [Valid] typed_compute_assigns_part4 (Qed)
[wp] [Valid] typed_compute_assigns_part5 (Alt-Ergo) (Cached)
[wp] [Valid] typed_compute_assigns_part6 (Qed)
[wp] [Valid] typed_main_requires_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_main_ensures_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_main_assert_writing_3_meta (Qed)
[wp] [Valid] typed_main_assert_writing_4_meta (Qed)
[wp] [Valid] typed_main_assert_writing_6_meta (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_5_meta_2 (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_5_meta_3 (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_5_meta_4 (Qed)
[wp] [Valid] typed_main_assigns_exit_part1 (Qed)
[wp] [Valid] typed_main_assigns_exit_part2 (Qed)
[wp] [Valid] typed_main_assigns_exit_part3 (Qed)
[wp] [Valid] typed_main_assigns_normal_part1 (Qed)
[wp] [Valid] typed_main_assigns_normal_part2 (Qed)
[wp] [Valid] typed_main_assigns_normal_part3 (Qed)
[wp] [Valid] typed_main_assigns_normal_part4 (Qed)
[wp] [Valid] typed_main_call_RW_requires (Qed)
[wp] [Valid] typed_main_call_RW_requires_2 (Qed)
[wp] [Valid] typed_main_call_RW_requires_strong_invariant_5_meta (Qed)
[wp] [Valid] typed_main_call_compute_requires (Qed)
[wp] [Valid] typed_main_call_compute_requires_strong_invariant_5_meta (Qed)
[wp] Proved goals: 39 / 39
Qed: 38
Qed: 38
Alt-Ergo: 1
[wp] dummy.c:22: Warning:
Memory model hypotheses for function 'RW':
......
......@@ -5,15 +5,16 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_writing_1_meta : Unsuccess
[wp] [Alt-Ergo] Goal typed_main_assert_writing_1_meta_2 : Valid
[wp] [Alt-Ergo] Goal typed_main_assert_writing_1_meta_3 : Valid
[wp] [Alt-Ergo] Goal typed_main_assert_writing_1_meta_4 : Valid
[wp] [Qed] Goal typed_main_assigns_part1 : Valid
[wp] [Qed] Goal typed_main_assigns_part2 : Valid
[wp] [Unsuccess] typed_main_assert_writing_1_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_main_assert_writing_1_meta_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_main_assert_writing_1_meta_3 (Alt-Ergo) (Cached)
[wp] [Valid] typed_main_assert_writing_1_meta_4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_main_assigns_part1 (Qed)
[wp] [Valid] typed_main_assigns_part2 (Qed)
[wp] Proved goals: 5 / 6
Qed: 2
Alt-Ergo: 3 (unsuccess: 1)
Qed: 2
Alt-Ergo: 3
Unsuccess: 1
/* Generated by Frama-C */
int a = 42;
int forbidden[2] = {42, 2713};
......
......@@ -5,36 +5,37 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 27 goals scheduled
[wp] [Qed] Goal typed_requiresInv_ensures_invariant_2_meta : Valid
[wp] [Qed] Goal typed_requiresInv_assigns_exit : Valid
[wp] [Qed] Goal typed_requiresInv_assigns_normal : Valid
[wp] [Qed] Goal typed_requiresInv_call___FC_assert_FC_assert_requires_nonnull_c : Valid
[wp] [Alt-Ergo] Goal typed_breaksInv_ensures_invariant_2_meta : Unsuccess
[wp] [Qed] Goal typed_breaksInv_assigns : Valid
[wp] [Qed] Goal typed_useless_assigns : Valid
[wp] [Alt-Ergo] Goal typed_maintainsInv_ensures_invariant_2_meta : Valid
[wp] [Qed] Goal typed_maintainsInv_assigns_exit : Valid
[wp] [Qed] Goal typed_maintainsInv_assigns_normal : Valid
[wp] [Alt-Ergo] Goal typed_cond_conditional_false_ensures_conditional_false_meta : Unsuccess
[wp] [Qed] Goal typed_cond_assigns : Valid
[wp] [Qed] Goal typed_cond_conditional_true_ensures_conditional_true_meta : Valid
[wp] [Qed] Goal typed_main_requires_strong_invariant_1_meta : Valid
[wp] [Qed] Goal typed_main_ensures_strong_invariant_1_meta : Valid
[wp] [Qed] Goal typed_main_assert_strong_invariant_1_meta : Valid
[wp] [Qed] Goal typed_main_assert_strong_invariant_1_meta_2 : Valid
[wp] [Qed] Goal typed_main_assert_strong_invariant_1_meta_3 : Valid
[wp] [Alt-Ergo] Goal typed_main_assert_strong_invariant_1_meta_4 : Valid
[wp] [Qed] Goal typed_main_assert_strong_invariant_1_meta_5 : Valid
[wp] [Qed] Goal typed_main_assert_strong_invariant_1_meta_6 : Valid
[wp] [Qed] Goal typed_main_assigns_exit : Valid
[wp] [Qed] Goal typed_main_assigns_normal : Valid
[wp] [Qed] Goal typed_main_call_maintainsInv_requires_invariant_2_meta : Valid
[wp] [Qed] Goal typed_main_call_requiresInv_requires_invariant_2_meta : Valid
[wp] [Qed] Goal typed_main_call_breaksInv_requires_invariant_2_meta : Valid
[wp] [Qed] Goal typed_main_call_requiresInv_2_requires_invariant_2_meta : Valid
[wp] [Valid] typed_requiresInv_ensures_invariant_2_meta (Qed)
[wp] [Valid] typed_requiresInv_assigns_exit (Qed)
[wp] [Valid] typed_requiresInv_assigns_normal (Qed)
[wp] [Valid] typed_requiresInv_call___FC_assert_FC_assert_requires_nonnull_c (Qed)
[wp] [Unsuccess] typed_breaksInv_ensures_invariant_2_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_breaksInv_assigns (Qed)
[wp] [Valid] typed_useless_assigns (Qed)
[wp] [Valid] typed_maintainsInv_ensures_invariant_2_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_maintainsInv_assigns_exit (Qed)
[wp] [Valid] typed_maintainsInv_assigns_normal (Qed)
[wp] [Unsuccess] typed_cond_conditional_false_ensures_conditional_false_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_cond_assigns (Qed)
[wp] [Valid] typed_cond_conditional_true_ensures_conditional_true_meta (Qed)
[wp] [Valid] typed_main_requires_strong_invariant_1_meta (Qed)
[wp] [Valid] typed_main_ensures_strong_invariant_1_meta (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_1_meta (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_1_meta_2 (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_1_meta_3 (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_1_meta_4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_main_assert_strong_invariant_1_meta_5 (Qed)
[wp] [Valid] typed_main_assert_strong_invariant_1_meta_6 (Qed)
[wp] [Valid] typed_main_assigns_exit (Qed)
[wp] [Valid] typed_main_assigns_normal (Qed)
[wp] [Valid] typed_main_call_maintainsInv_requires_invariant_2_meta (Qed)
[wp] [Valid] typed_main_call_requiresInv_requires_invariant_2_meta (Qed)
[wp] [Valid] typed_main_call_breaksInv_requires_invariant_2_meta (Qed)
[wp] [Valid] typed_main_call_requiresInv_2_requires_invariant_2_meta (Qed)
[wp] Proved goals: 25 / 27
Qed: 23
Alt-Ergo: 2 (unsuccess: 2)
Qed: 23
Alt-Ergo: 2
Unsuccess: 2
/* Generated by Frama-C */
#include "assert.h"
unsigned int A = (unsigned int)2;
......
......@@ -5,19 +5,19 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Qed] Goal typed_f_ensures_strong_invariant_1_meta : Valid
[wp] [Qed] Goal typed_f_loop_invariant_strong_invariant_1_preserved : Valid
[wp] [Qed] Goal typed_f_loop_invariant_strong_invariant_1_established : Valid
[wp] [Qed] Goal typed_f_assert_strong_invariant_1_meta : Valid
[wp] [Qed] Goal typed_f_loop_assigns : Valid
[wp] [Qed] Goal typed_f_assigns : Valid
[wp] [Qed] Goal typed_main_assigns_exit : Valid
[wp] [Qed] Goal typed_main_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_main_assigns_normal_part2 : Valid
[wp] [Alt-Ergo] Goal typed_main_call_f_requires_strong_invariant_1_meta : Unsuccess
[wp] [Valid] typed_f_ensures_strong_invariant_1_meta (Qed)
[wp] [Valid] typed_f_loop_invariant_strong_invariant_1_preserved (Qed)
[wp] [Valid] typed_f_loop_invariant_strong_invariant_1_established (Qed)
[wp] [Valid] typed_f_assert_strong_invariant_1_meta (Qed)
[wp] [Valid] typed_f_loop_assigns (Qed)
[wp] [Valid] typed_f_assigns (Qed)
[wp] [Valid] typed_main_assigns_exit (Qed)
[wp] [Valid] typed_main_assigns_normal_part1 (Qed)
[wp] [Valid] typed_main_assigns_normal_part2 (Qed)
[wp] [Unsuccess] typed_main_call_f_requires_strong_invariant_1_meta (Alt-Ergo) (Cached)
[wp] Proved goals: 9 / 10
Qed: 9
Alt-Ergo: 0 (unsuccess: 1)
Qed: 9
Unsuccess: 1
/* Generated by Frama-C */
int foo = 1;
/*@ requires strong_invariant_1: meta: foo > 0;
......
......@@ -5,15 +5,15 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_main_assert_writing_1_meta : Valid
[wp] [Qed] Goal typed_main_assert_writing_1_meta_2 : Valid
[wp] [Alt-Ergo] Goal typed_main_assert_writing_1_meta_3 : Unsuccess
[wp] [Qed] Goal typed_main_assert_writing_1_meta_4 : Valid
[wp] [Qed] Goal typed_main_assigns_part1 : Valid
[wp] [Qed] Goal typed_main_assigns_part2 : Valid
[wp] [Valid] typed_main_assert_writing_1_meta (Qed)
[wp] [Valid] typed_main_assert_writing_1_meta_2 (Qed)
[wp] [Unsuccess] typed_main_assert_writing_1_meta_3 (Alt-Ergo) (Cached)
[wp] [Valid] typed_main_assert_writing_1_meta_4 (Qed)
[wp] [Valid] typed_main_assigns_part1 (Qed)
[wp] [Valid] typed_main_assigns_part2 (Qed)
[wp] Proved goals: 5 / 6
Qed: 5
Alt-Ergo: 0 (unsuccess: 1)
Qed: 5
Unsuccess: 1
/* Generated by Frama-C */
int a = 0;
/*@ assigns a; */
......
......@@ -5,22 +5,22 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 13 goals scheduled
[wp] [Qed] Goal typed_f1_ensures_test2_meta : Valid
[wp] [Qed] Goal typed_f1_assert_test2_meta : Valid
[wp] [Alt-Ergo] Goal typed_f1_assert_test2_meta_2 : Unsuccess
[wp] [Qed] Goal typed_f1_assigns : Valid
[wp] [Qed] Goal typed_f2_ensures_test2_meta : Valid
[wp] [Qed] Goal typed_f2_assigns : Valid
[wp] [Qed] Goal typed_f3_ensures_test2_meta : Valid
[wp] [Qed] Goal typed_f3_check_always_check_meta : Valid
[wp] [Qed] Goal typed_f3_assigns : Valid
[wp] [Qed] Goal typed_f4_ensures_test2_meta : Valid
[wp] [Qed] Goal typed_f4_assert_always_assert_meta : Valid
[wp] [Alt-Ergo] Goal typed_f4_assert_test2_meta : Unsuccess
[wp] [Qed] Goal typed_f4_assigns : Valid
[wp] [Valid] typed_f1_ensures_test2_meta (Qed)
[wp] [Valid] typed_f1_assert_test2_meta (Qed)
[wp] [Unsuccess] typed_f1_assert_test2_meta_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_assigns (Qed)
[wp] [Valid] typed_f2_ensures_test2_meta (Qed)
[wp] [Valid] typed_f2_assigns (Qed)
[wp] [Valid] typed_f3_ensures_test2_meta (Qed)
[wp] [Valid] typed_f3_check_always_check_meta (Qed)
[wp] [Valid] typed_f3_assigns (Qed)
[wp] [Valid] typed_f4_ensures_test2_meta (Qed)
[wp] [Valid] typed_f4_assert_always_assert_meta (Qed)
[wp] [Unsuccess] typed_f4_assert_test2_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_assigns (Qed)
[wp] Proved goals: 11 / 13
Qed: 11
Alt-Ergo: 0 (unsuccess: 2)
Qed: 11
Unsuccess: 2
/* Generated by Frama-C */
int C1;
int C2;
......
......@@ -5,22 +5,22 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 13 goals scheduled
[wp] [Alt-Ergo] Goal typed_f1_check_ensures_test2_meta : Unsuccess
[wp] [Alt-Ergo] Goal typed_f1_check_test2_meta : Unsuccess
[wp] [Alt-Ergo] Goal typed_f1_check_test2_meta_2 : Unsuccess
[wp] [Qed] Goal typed_f1_assigns : Valid
[wp] [Alt-Ergo] Goal typed_f2_check_ensures_test2_meta : Unsuccess
[wp] [Qed] Goal typed_f2_assigns : Valid
[wp] [Alt-Ergo] Goal typed_f3_check_ensures_test2_meta : Unsuccess
[wp] [Alt-Ergo] Goal typed_f3_check_always_check_meta : Unsuccess
[wp] [Qed] Goal typed_f3_assigns : Valid
[wp] [Alt-Ergo] Goal typed_f4_check_ensures_test2_meta : Unsuccess
[wp] [Alt-Ergo] Goal typed_f4_assert_always_assert_meta : Unsuccess
[wp] [Alt-Ergo] Goal typed_f4_check_test2_meta : Unsuccess
[wp] [Qed] Goal typed_f4_assigns : Valid
[wp] [Unsuccess] typed_f1_check_ensures_test2_meta (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_f1_check_test2_meta (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_f1_check_test2_meta_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_assigns (Qed)
[wp] [Unsuccess] typed_f2_check_ensures_test2_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_assigns (Qed)
[wp] [Unsuccess] typed_f3_check_ensures_test2_meta (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_f3_check_always_check_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_assigns (Qed)
[wp] [Unsuccess] typed_f4_check_ensures_test2_meta (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_f4_assert_always_assert_meta (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_f4_check_test2_meta (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_assigns (Qed)
[wp] Proved goals: 4 / 13
Qed: 4
Alt-Ergo: 0 (unsuccess: 9)
Qed: 4
Unsuccess: 9
/* Generated by Frama-C */
int C1;
int C2;
......
......@@ -5,16 +5,16 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
[wp] [Qed] Goal typed_foo_assigns : Valid
[wp] [Qed] Goal typed_bar_assert_calling_1_meta : Valid
[wp] [Alt-Ergo] Goal typed_bar_assert_calling_1_meta_2 : Unsuccess
[wp] [Qed] Goal typed_bar_assigns_exit : Valid
[wp] [Qed] Goal typed_bar_assigns_normal : Valid
[wp] [Qed] Goal typed_main_assigns_exit : Valid
[wp] [Qed] Goal typed_main_assigns_normal : Valid
[wp] [Valid] typed_foo_assigns (Qed)
[wp] [Valid] typed_bar_assert_calling_1_meta (Qed)
[wp] [Unsuccess] typed_bar_assert_calling_1_meta_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_bar_assigns_exit (Qed)
[wp] [Valid] typed_bar_assigns_normal (Qed)
[wp] [Valid] typed_main_assigns_exit (Qed)
[wp] [Valid] typed_main_assigns_normal (Qed)
[wp] Proved goals: 6 / 7
Qed: 6
Alt-Ergo: 0 (unsuccess: 1)
Qed: 6
Unsuccess: 1
/* Generated by Frama-C */
int x;
/*@ assigns \nothing; */
......
......@@ -5,8 +5,8 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_f_assert_test_meta : Valid
[wp] [Qed] Goal typed_f_assigns : Valid
[wp] [Valid] typed_f_assert_test_meta (Qed)
[wp] [Valid] typed_f_assigns (Qed)
[wp] Proved goals: 2 / 2
Qed: 2
------------------------------------------------------------
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment