Skip to content
Snippets Groups Projects
Commit 8ed5477b authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] use success-only for qualif

parent b1abc7b4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 106 additions and 106 deletions
src/plugins/wp/register.ml
+ 1
− 1
View file @ 8ed5477b
......@@ -400,7 +400,7 @@ let do_report_steps fmt s =
let do_report_stopped fmt s =
if Wp_parameters.has_dkey VCS.dkey_success_only then
begin
let n = s.interrupted + s.unknown + s.failed in
let n = s.interrupted + s.unknown in
if n > 0 then
Format.fprintf fmt " (unsuccess: %d)" n ;
end
......
src/plugins/wp/tests/test_config_qualif
+ 1
− 1
View file @ 8ed5477b
CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 90 -wp-share ./share -wp-msg-key shell,no-time-info,no-step-info -wp-report-json @PTEST_FILE@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-out @PTEST_FILE@.@PTEST_NUMBER@.out @PTEST_FILE@
CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 90 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_FILE@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-out @PTEST_FILE@.@PTEST_NUMBER@.out @PTEST_FILE@
OPT:
src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
+ 9
− 9
View file @ 8ed5477b
......@@ -13,33 +13,33 @@
[wp] [Qed] Goal typed_behavior2_assert : Valid
[wp] [Qed] Goal typed_behavior3_assert : Valid
[wp] [Qed] Goal typed_behavior4_assert : Valid
[wp] [Alt-Ergo] Goal typed_behavior5_assert_bad : Unknown
[wp] [Alt-Ergo] Goal typed_behavior5_assert_bad : Unsuccess
[wp] [Qed] Goal typed_compare_assert : Valid
[wp] [Qed] Goal typed_empty_assert : Valid
[wp] [Alt-Ergo] Goal typed_if_assert_assert : Valid
[wp] [Alt-Ergo] Goal typed_if_assert_assert_2 : Unknown
[wp] [Alt-Ergo] Goal typed_if_assert_assert_2 : Unsuccess
[wp] [Qed] Goal typed_if_assert_assert_3 : Valid
[wp] [Alt-Ergo] Goal typed_if_assert_assert_missing_return : Unknown
[wp] [Alt-Ergo] Goal typed_if_assert_assert_missing_return : Unsuccess
[wp] [Qed] Goal typed_main_assert : Valid
[wp] [Qed] Goal typed_main_assigns_global_assert : Valid
[wp] [Qed] Goal typed_main_assigns_global_assert_2 : Valid
[wp] [Alt-Ergo] Goal typed_main_assigns_global_assert_bad : Unknown
[wp] [Alt-Ergo] Goal typed_main_assigns_global_assert_bad : Unsuccess
[wp] [Qed] Goal typed_main_ensures_result_assert : Valid
[wp] [Alt-Ergo] Goal typed_not_main_assert_bad : Unknown
[wp] [Alt-Ergo] Goal typed_not_main_assert_bad : Unsuccess
[wp] [Qed] Goal typed_one_assign_assert : Valid
[wp] [Qed] Goal typed_one_if_assert : Valid
[wp] [Qed] Goal typed_some_seq_assert : Valid
[wp] [Qed] Goal typed_some_seq_assert_2 : Valid
[wp] [Qed] Goal typed_zloop_ensures : Valid
[wp] [Alt-Ergo] Goal typed_zloop_loop_invariant_preserved : Unknown
[wp] [Alt-Ergo] Goal typed_zloop_loop_invariant_preserved : Unsuccess
[wp] [Qed] Goal typed_zloop_loop_invariant_established : Valid
[wp] [Qed] Goal typed_zloop_assert : Valid
[wp] [Qed] Goal typed_zloop_assert_2 : Valid
[wp] [Alt-Ergo] Goal typed_zloop_assert_3 : Unknown
[wp] [Alt-Ergo] Goal typed_zloop_assert_bad : Unknown
[wp] [Alt-Ergo] Goal typed_zloop_assert_3 : Unsuccess
[wp] [Alt-Ergo] Goal typed_zloop_assert_bad : Unsuccess
[wp] Proved goals: 19 / 27
Qed: 18
Alt-Ergo: 1 (unknown: 8)
Alt-Ergo: 1 (unsuccess: 8)
[wp] Report 'tests/wp/stmtcompiler_test.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
+ 7
− 7
View file @ 8ed5477b
......@@ -14,13 +14,13 @@
[wp] tests/wp/wp_behav.c:81: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 38 goals scheduled
[wp] [Alt-Ergo] Goal typed_assert_needed_assert_ko : Unknown
[wp] [Alt-Ergo] Goal typed_assert_needed_assert_ko : Unsuccess
[wp] [Qed] Goal typed_assert_needed_assert_qed_ok_ok_with_hyp : Valid
[wp] [Alt-Ergo] Goal typed_bhv_complete_pos_neg : Valid
[wp] [Qed] Goal typed_bhv_neg_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_bhv_pos_ensures_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko1 : Unknown
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko2 : Unknown
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko1 : Unsuccess
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko2 : Unsuccess
[wp] [Qed] Goal typed_f_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_x1_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_assert_qed_ok : Valid
......@@ -36,12 +36,12 @@
[wp] [Qed] Goal typed_more_stmt_assigns_blk_assigns_part1 : Valid
[wp] [Qed] Goal typed_more_stmt_assigns_blk_assigns_part2 : Valid
[wp] [Qed] Goal typed_part_stmt_bhv_b1_ensures_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_part_stmt_bhv_bs_ensures : Unknown
[wp] [Alt-Ergo] Goal typed_part_stmt_bhv_bs_ensures : Unsuccess
[wp] [Alt-Ergo] Goal typed_razT_loop_invariant_qed_ok_preserved : Valid
[wp] [Qed] Goal typed_razT_loop_invariant_qed_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_razT_b1_ensures_e1 : Unknown
[wp] [Alt-Ergo] Goal typed_razT_b1_ensures_e1 : Unsuccess
[wp] [Qed] Goal typed_stmt_assigns_ensures : Valid
[wp] [Alt-Ergo] Goal typed_stmt_assigns_assigns : Unknown
[wp] [Alt-Ergo] Goal typed_stmt_assigns_assigns : Unsuccess
[wp] [Qed] Goal typed_stmt_contract_requires_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_stmt_contract_ok_ensures_qed_ok : Valid
......@@ -54,7 +54,7 @@
[wp] [Qed] Goal typed_stmt_contract_label_ensures_qed_ok : Valid
[wp] Proved goals: 32 / 38
Qed: 30
Alt-Ergo: 2 (unknown: 6)
Alt-Ergo: 2 (unsuccess: 6)
[wp] Report 'tests/wp/wp_behav.c.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
+ 9
− 9
View file @ 8ed5477b
......@@ -8,16 +8,16 @@
[wp] tests/wp/wp_behav.c:69: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_f_x1_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_f_x2_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_min_bx_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_min_by_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_stmt_contract_ko_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_stmt_contract_ko_without_asgn_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_stmt_contract_assigns_ko_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_f_x1_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_f_x2_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_min_bx_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_min_by_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_stmt_contract_ko_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_stmt_contract_ko_without_asgn_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_stmt_contract_assigns_ko_ensures_qed_ko : Unsuccess
[wp] Proved goals: 0 / 8
Alt-Ergo: 0 (unknown: 8)
Alt-Ergo: 0 (unsuccess: 8)
[wp] Report 'tests/wp/wp_behav.c.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
+ 9
− 9
View file @ 8ed5477b
......@@ -11,34 +11,34 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] 25 goals scheduled
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko1 : Unknown
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko2 : Unknown
[wp] [Alt-Ergo] Goal hoare_bts0513_bis_assert_qed_ko_ko1 : Unknown
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko1 : Unsuccess
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko2 : Unsuccess
[wp] [Alt-Ergo] Goal hoare_bts0513_bis_assert_qed_ko_ko1 : Unsuccess
[wp] [Qed] Goal hoare_bts0513_bis_assert_qed_ok_ok : Valid
[wp] [Qed] Goal hoare_default_behaviors_ensures_qed_ok : Valid
[wp] [Qed] Goal hoare_default_behaviors_assert_qed_ok_2 : Valid
[wp] [Qed] Goal hoare_default_behaviors_ensures_qed_ok_stmt_p : Valid
[wp] [Qed] Goal hoare_default_behaviors_assert_qed_ok : Valid
[wp] [Alt-Ergo] Goal hoare_default_behaviors_assert_rte_signed_overflow : Unknown
[wp] [Alt-Ergo] Goal hoare_default_behaviors_assert_rte_signed_overflow : Unsuccess
[wp] [Qed] Goal hoare_default_behaviors_assigns : Valid
[wp] [Qed] Goal hoare_dpd1_assert_qed_ok_A : Valid
[wp] [Alt-Ergo] Goal hoare_dpd1_ensures_qed_ko_Eko : Unknown
[wp] [Alt-Ergo] Goal hoare_dpd1_ensures_qed_ko_Eko : Unsuccess
[wp] [Qed] Goal hoare_dpd1_assigns : Valid
[wp] [Qed] Goal hoare_dpd2_assert_qed_ok_A : Valid
[wp] [Alt-Ergo] Goal hoare_dpd2_ensures_qed_ko_Eko : Unknown
[wp] [Alt-Ergo] Goal hoare_dpd2_ensures_qed_ko_Eko : Unsuccess
[wp] [Qed] Goal hoare_dpd2_assigns : Valid
[wp] [Qed] Goal hoare_spec_if_ensures_qed_ok_2 : Valid
[wp] [Qed] Goal hoare_spec_if_ensures_qed_ok : Valid
[wp] [Qed] Goal hoare_spec_if_assigns : Valid
[wp] [Alt-Ergo] Goal hoare_spec_if_assert_rte_signed_overflow : Unknown
[wp] [Alt-Ergo] Goal hoare_spec_if_assert_rte_signed_overflow : Unsuccess
[wp] [Qed] Goal hoare_spec_if_assigns_2 : Valid
[wp] [Alt-Ergo] Goal hoare_spec_if_assert_rte_signed_overflow_2 : Unknown
[wp] [Alt-Ergo] Goal hoare_spec_if_assert_rte_signed_overflow_2 : Unsuccess
[wp] [Qed] Goal hoare_spec_if_assigns_3 : Valid
[wp] [Qed] Goal hoare_spec_if_cond_ensures_qed_ok : Valid
[wp] [Qed] Goal hoare_spec_if_not_cond_ensures_qed_ok : Valid
[wp] Proved goals: 17 / 25
Qed: 17
Alt-Ergo: 0 (unknown: 8)
Alt-Ergo: 0 (unsuccess: 8)
[wp] Report 'tests/wp/wp_strategy.c.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp/stmtcompiler_test.i
+ 1
− 1
View file @ 8ed5477b
/* run.config
OPT: -load-script tests/wp/stmtcompiler_test.ml -wp-msg-key no-time-info -wp-msg-key no-step-info
OPT: -load-script tests/wp/stmtcompiler_test.ml -wp-msg-key success-only
*/
int empty (int c){
......
src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
+ 1
− 1
View file @ 8ed5477b
/* run.config_qualif
OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key no-time-info -wp-msg-key no-step-info
OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key success-only
*/
int empty (int c){
......
src/plugins/wp/tests/wp/wp_strategy.c
+ 1
− 1
View file @ 8ed5477b
......@@ -4,7 +4,7 @@ OPT: -journal-disable -wp-model Typed -wp-verbose 2 -wp-prop @assigns
*/
/* run.config_qualif
OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key "no-time-info"
OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key "success-only"
*/
/*----------------------------------------------------------------------------*/
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle
+ 2
− 2
View file @ 8ed5477b
......@@ -4,9 +4,9 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unknown
[wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unsuccess
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unknown: 1)
Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_acsl/arith.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle
+ 7
− 7
View file @ 8ed5477b
......@@ -4,14 +4,14 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_call_assigns_t1_assigns_exit : Unknown
[wp] [Alt-Ergo] Goal typed_call_assigns_t1_assigns_normal : Unknown
[wp] [Alt-Ergo] Goal typed_call_assigns_t2_assigns_exit : Unknown
[wp] [Alt-Ergo] Goal typed_call_assigns_t2_assigns_normal : Unknown
[wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_exit : Unknown
[wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_normal : Unknown
[wp] [Alt-Ergo] Goal typed_call_assigns_t1_assigns_exit : Unsuccess
[wp] [Alt-Ergo] Goal typed_call_assigns_t1_assigns_normal : Unsuccess
[wp] [Alt-Ergo] Goal typed_call_assigns_t2_assigns_exit : Unsuccess
[wp] [Alt-Ergo] Goal typed_call_assigns_t2_assigns_normal : Unsuccess
[wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_exit : Unsuccess
[wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_normal : Unsuccess
[wp] Proved goals: 0 / 6
Alt-Ergo: 0 (unknown: 6)
Alt-Ergo: 0 (unsuccess: 6)
[wp] Report 'tests/wp_acsl/assigns_range.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle
+ 3
− 3
View file @ 8ed5477b
......@@ -4,7 +4,7 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_P_todo : Unknown
[wp] [Alt-Ergo] Goal typed_f_ensures_P_todo : Unsuccess
[wp] [Alt-Ergo] Goal typed_f_ensures_Q : Valid
[wp] [Alt-Ergo] Goal typed_f_loop_invariant_Index_preserved : Valid
[wp] [Alt-Ergo] Goal typed_f_loop_invariant_Index_established : Valid
......@@ -13,10 +13,10 @@
[wp] [Qed] Goal typed_f_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_f_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_f_loop_assigns_part3 : Valid
[wp] [Alt-Ergo] Goal typed_f_assigns : Unknown
[wp] [Alt-Ergo] Goal typed_f_assigns : Unsuccess
[wp] Proved goals: 8 / 10
Qed: 3
Alt-Ergo: 5 (unknown: 2)
Alt-Ergo: 5 (unsuccess: 2)
[wp] Report 'tests/wp_acsl/axioms.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
+ 4
− 4
View file @ 8ed5477b
......@@ -12,7 +12,7 @@
[wp] [Qed] Goal typed_band_bit2_ensures_band4 : Valid
[wp] [Qed] Goal typed_band_bit3_ensures_band5 : Valid
[wp] [Qed] Goal typed_band_bit4_ensures_band6 : Valid
[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Unknown
[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Unsuccess
[wp] [Qed] Goal typed_band_bool_true_ensures : Valid
[wp] [Qed] Goal typed_bnot_ensures : Valid
[wp] [Qed] Goal typed_bor_ensures : Valid
......@@ -20,12 +20,12 @@
[wp] [Qed] Goal typed_bor_bit1_ensures_bor1 : Valid
[wp] [Qed] Goal typed_bor_bit2_ensures_bor2 : Valid
[wp] [Qed] Goal typed_bor_bit3_ensures_bor3 : Valid
[wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Unknown
[wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Unsuccess
[wp] [Alt-Ergo] Goal typed_bor_bool_true_ensures : Valid
[wp] [Qed] Goal typed_bxor_ensures : Valid
[wp] [Qed] Goal typed_bxor_bit1_ensures : Valid
[wp] [Qed] Goal typed_bxor_bit2_ensures : Valid
[wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Unknown
[wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Unsuccess
[wp] [Qed] Goal typed_bxor_bool_true_ensures : Valid
[wp] [Qed] Goal typed_lshift_ensures : Valid
[wp] [Qed] Goal typed_lshift_shift1_ensures_lsl1 : Valid
......@@ -35,7 +35,7 @@
[wp] [Qed] Goal typed_rshift_shift1_ensures_lsr1 : Valid
[wp] Proved goals: 26 / 29
Qed: 25
Alt-Ergo: 1 (unknown: 3)
Alt-Ergo: 1 (unsuccess: 3)
[wp] Report 'tests/wp_acsl/bitwise.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
+ 1
− 1
View file @ 8ed5477b
......@@ -308,4 +308,4 @@
Functions WP Alt-Ergo Total Success
f 11 32 (336..384) 43 100%
-------------------------------------------------------------
[wp] Logging keys: shell,no-time-info,no-step-info,cnf.
[wp] Logging keys: success-only,shell,cnf.
src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
+ 3
− 3
View file @ 8ed5477b
......@@ -4,10 +4,10 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_d7_div_0_x_ko : Unknown
[wp] [Alt-Ergo] Goal typed_f_ensures_m7_mod_0_x_ko : Unknown
[wp] [Alt-Ergo] Goal typed_f_ensures_d7_div_0_x_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_f_ensures_m7_mod_0_x_ko : Unsuccess
[wp] Proved goals: 0 / 2
Alt-Ergo: 0 (unknown: 2)
Alt-Ergo: 0 (unsuccess: 2)
[wp] Report 'tests/wp_acsl/div_mod.i.2.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
+ 2
− 2
View file @ 8ed5477b
......@@ -6,13 +6,13 @@
No code nor implicit assigns clause for function main, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_extra_ensures_KO : Unknown
[wp] [Alt-Ergo] Goal typed_extra_ensures_KO : Unsuccess
[wp] [Qed] Goal typed_foreign_ensures_OK : Valid
[wp] [Alt-Ergo] Goal typed_job_ensures_OK : Valid
[wp] [Qed] Goal typed_main_requires_OK : Valid
[wp] Proved goals: 3 / 4
Qed: 2
Alt-Ergo: 1 (unknown: 1)
Alt-Ergo: 1 (unsuccess: 1)
[wp] Report 'tests/wp_acsl/init_label.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
+ 19
− 19
View file @ 8ed5477b
......@@ -4,26 +4,26 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 18 goals scheduled
[wp] [Alt-Ergo] Goal typed_fa1_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_fa1_ensures_qed_ko_2 : Unknown
[wp] [Alt-Ergo] Goal typed_fa2_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_fa2_ensures_qed_ko_2 : Unknown
[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko_2 : Unknown
[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko_3 : Unknown
[wp] [Alt-Ergo] Goal typed_fs1_ensures_qed_ko : Unknown
[wp] [Alt-Ergo] Goal typed_fs1_ensures_qed_ko_2 : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_eq_ko : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_t : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_c_2 : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Tab_no_init : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_With_Array_Struct_3 : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Simple_Array_1 : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_T1_6 : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_indirect_init_union_b : Unknown
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_indirect_init_union_t : Unknown
[wp] [Alt-Ergo] Goal typed_fa1_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_fa1_ensures_qed_ko_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_fa2_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_fa2_ensures_qed_ko_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko_3 : Unsuccess
[wp] [Alt-Ergo] Goal typed_fs1_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_fs1_ensures_qed_ko_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_eq_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_t : Unsuccess
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_c_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Tab_no_init : Unsuccess
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_With_Array_Struct_3 : Unsuccess
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Simple_Array_1 : Unsuccess
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_T1_6 : Unsuccess
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_indirect_init_union_b : Unsuccess
[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_indirect_init_union_t : Unsuccess
[wp] Proved goals: 0 / 18
Alt-Ergo: 0 (unknown: 18)
Alt-Ergo: 0 (unsuccess: 18)
[wp] Report 'tests/wp_acsl/init_value.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle
+ 2
− 2
View file @ 8ed5477b
......@@ -4,9 +4,9 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_assert_qed_ko_oracle_ko : Unknown
[wp] [Alt-Ergo] Goal typed_f_assert_qed_ko_oracle_ko : Unsuccess
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unknown: 1)
Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_acsl/label_escape.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
+ 17
− 17
View file @ 8ed5477b
......@@ -41,30 +41,30 @@
[wp] tests/wp_acsl/logic.i:62: Warning:
Logic cast to struct (Tint2) from (int [6]) not implemented yet
[wp] 21 goals scheduled
[wp] [Alt-Ergo] Goal typed_h_ensures : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_h_ensures : Unsuccess (Stronger)
[wp] [Qed] Goal typed_h_assigns_exit : Valid
[wp] [Qed] Goal typed_h_assigns_normal : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_2 : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_3 : Valid
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_4 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_5 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_6 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_7 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_8 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_9 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_10 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_11 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_12 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_13 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_14 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_15 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_16 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_17 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_18 : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_4 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_5 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_6 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_7 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_8 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_9 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_10 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_11 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_12 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_13 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_14 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_15 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_16 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_17 : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_18 : Unsuccess (Stronger)
[wp] Proved goals: 5 / 21
Qed: 3
Alt-Ergo: 2 (unknown: 16)
Alt-Ergo: 2 (unsuccess: 16)
[wp] Report 'tests/wp_acsl/logic.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
+ 7
− 7
View file @ 8ed5477b
......@@ -6,18 +6,18 @@
[wp] tests/wp_acsl/pointer.i:50: Warning: Uncomparable locations p_0 and mem:t
[wp] tests/wp_acsl/pointer.i:49: Warning: Uncomparable locations p_0 and mem:t
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_ref_absurd_ensures_qed_ko_Base_oracle_ko : Unknown
[wp] [Alt-Ergo] Goal typed_ref_absurd_ensures_qed_ko_Comp_oracle_ko : Unknown
[wp] [Alt-Ergo] Goal typed_ref_absurd_ensures_qed_ko_Base_oracle_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_ref_absurd_ensures_qed_ko_Comp_oracle_ko : Unsuccess
[wp] [Qed] Goal typed_ref_array_ensures_Lt : Valid
[wp] [Qed] Goal typed_ref_array_ensures_Le : Valid
[wp] [Qed] Goal typed_ref_array_ensures_Eq : Valid
[wp] [Alt-Ergo] Goal typed_ref_mixed_array_pointer_ensures_qed_ko_Le_oracle_ko : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_ref_mixed_array_pointer_ensures_qed_ko_Lt_oracle_ko : Unknown (Stronger)
[wp] [Alt-Ergo] Goal typed_ref_pointer_ensures_qed_ko_Le_oracle_ko : Unknown
[wp] [Alt-Ergo] Goal typed_ref_pointer_ensures_qed_ko_Eq_oracle_ko : Unknown
[wp] [Alt-Ergo] Goal typed_ref_mixed_array_pointer_ensures_qed_ko_Le_oracle_ko : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_ref_mixed_array_pointer_ensures_qed_ko_Lt_oracle_ko : Unsuccess (Stronger)
[wp] [Alt-Ergo] Goal typed_ref_pointer_ensures_qed_ko_Le_oracle_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_ref_pointer_ensures_qed_ko_Eq_oracle_ko : Unsuccess
[wp] Proved goals: 3 / 9
Qed: 3
Alt-Ergo: 0 (unknown: 6)
Alt-Ergo: 0 (unsuccess: 6)
[wp] Report 'tests/wp_acsl/pointer.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
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