diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index a21ded01520598d554c5b182a96088c017eea56a..98c9a894acfb073a3ffd07396b26a3d7794c7101 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -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
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 8006bdebe926f013a5b162fa96dfc7caef369b8d..e8a8597428de758b3a07b1fe611e7a60377460a4 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,2 +1,2 @@
-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:
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
index d2ce6cd6a429ef0dfa80b108ed4773ad1fc56dff..d3b2208c9f1317bc1e3e5219040302803a0fe570 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
index 1b6f43fb505c53f5a984707b26ff1a6153372581..78a9e8c0f3f8beeca2bb660c464f5da3455dc46d 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
index 745a17600fa3965aa0a10b658d65edde47f6910e..bc1f4d8ead03c9525aa99d4317548402bc40f1a8 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
index 8dfdb335c2b8ed73c162e80ac9d560a08bbabc39..71f60a8745347a66874fab4ead9a29e3611c196b 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.i b/src/plugins/wp/tests/wp/stmtcompiler_test.i
index b4b68fb8812277aca990e46dfd0c62b942a4373d..264b9e58d48e6401b1c73564a7755720598f2b97 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.i
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.i
@@ -1,5 +1,5 @@
/* 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){
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
index d5c4846b870b61f37084f13faa641394e4c3db6a..4dafe25db11100c8549fc7f6291914f0a31f9df0 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.i
@@ -1,5 +1,5 @@
/* 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){
diff --git a/src/plugins/wp/tests/wp/wp_strategy.c b/src/plugins/wp/tests/wp/wp_strategy.c
index af3b27b5f8dcd341f55acef981619804f7edc258..0afd35c132005b5dc32d047c4d9847b410013b91 100644
--- a/src/plugins/wp/tests/wp/wp_strategy.c
+++ b/src/plugins/wp/tests/wp/wp_strategy.c
@@ -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"
*/
/*----------------------------------------------------------------------------*/
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle
index 473a012c3e21722c774d5dde8a1d77be84ef94ee..67dde50a424bc42ba6b80701fccdf266405bc14e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle
index 73d00d5b60c654dd9afa4677e6010add74322230..62dbc55d245fe4e925d2a1ac63591c34370e0f28 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle
index f5638f7fcd190c69e8182ab88bdc7c4b6dcff689..1af8a459bfdeb0960a2d12dd1ead540356b54878 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
index 3e2273eac8354bdd6fb8fdb663d0c28f8e47bc6c..74ff28899fe122380fc43713123a188e008b450d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
index 6ebd97b44fdd765b8aca8b5bbeca9eadb450e4ac..bc588e84733e9a0de61ff9ee6dab315e55d40340 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle
@@ -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.
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
index dd6bba2a7058bbc80cd6555bf7a31ae028ce1e13..3d3ad3145f0e68bbe2994c8f0aded0eeb5c642e3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
index c3f090839d60777287c9ef82e5ad5055ba596528..b4b67bf6b9fc6af79eeb7a71aae4388331a80215 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
index 6fd6542afa8361c5a6836072b77949b948416ead..ab90d518152d0b9470b56a19d016b350fc73b81c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle
index 8c92ea1ed5d628d3e0034db66ae7e2581d0f622e..32bbae5f36c05d490ab9e9ca2550da3fcd34c2b6 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
index d22e02bbbd1cbe7cd09d5e8f0b635136c58655b7..26b176ac8f201f65fc9bb05568dae7c130f0faa9 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
index 7c36192fd7af34f0c6f8d194d94f4307d5195843..b319d2b25373519a08ebc79571aae33c600994b4 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle
@@ -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
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
index ae8ae26c94ab00e62049da1bfbe6c2ba3b3b546b..77732b04cfe1ee2bf3dc38ce6b3fc7dcc9bb6fd3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle
@@ -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_absurd_ensures_qed_ko_Base_oracle_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_absurd_ensures_qed_ko_Comp_oracle_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_absurd_ensures_qed_ko_Base_oracle_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_absurd_ensures_qed_ko_Comp_oracle_ko : Unsuccess
[wp] [Qed] Goal typed_array_ensures_Lt : Valid
[wp] [Qed] Goal typed_array_ensures_Le : Valid
[wp] [Qed] Goal typed_array_ensures_Eq : Valid
-[wp] [Alt-Ergo] Goal typed_mixed_array_pointer_ensures_qed_ko_Le_oracle_ko : Unknown (Stronger)
-[wp] [Alt-Ergo] Goal typed_mixed_array_pointer_ensures_qed_ko_Lt_oracle_ko : Unknown (Stronger)
-[wp] [Alt-Ergo] Goal typed_pointer_ensures_qed_ko_Le_oracle_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_pointer_ensures_qed_ko_Eq_oracle_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_mixed_array_pointer_ensures_qed_ko_Le_oracle_ko : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_mixed_array_pointer_ensures_qed_ko_Lt_oracle_ko : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_pointer_ensures_qed_ko_Le_oracle_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_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.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle
index 0bdbeee3cfe21360a3934f5a720115c7111ca45e..4df28dabcef36cee5c289d21963b2625c2369075 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle
@@ -5,10 +5,10 @@
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_correct_assert_OK : Valid
-[wp] [Alt-Ergo] Goal typed_wrong_assert_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_wrong_assert_KO : Unsuccess
[wp] Proved goals: 1 / 2
Qed: 1
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_acsl/post_result.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle
index b5d9d479c01f387417e3f2800de0874cecf618f7..d8de2ea9bacf099e5e588b5bd027f4c83a3d4dc2 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle
@@ -40,45 +40,45 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 37 goals scheduled
-[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_precedence_xor_and : Unknown
-[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_r_precedence_xor_and : Unknown
-[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_precedence_or_xor : Unknown
-[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_r_precedence_or_xor : Unknown
-[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_precedence_implies_or : Unknown
-[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_assoc_implies : Unknown
-[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_r_precedence_equiv_implies : Unknown
-[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_precedence_equiv_implies : Unknown
-[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_r_precedence_and_eq : Unknown
-[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_l_precedence_and_eq : Unknown
-[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_l_nonassoc_eq : Unknown
-[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_r_nonassoc_eq : Unknown
-[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_r_precedence_and_neq : Unknown
-[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_l_precedence_and_neq : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_xor_and : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_xor_and : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_or_xor : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_or_xor : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_implies_or : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_assoc_implies : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_equiv_implies : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_equiv_implies : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_ite_equiv : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_ite_equiv : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_assoc_ite : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_forall_ite : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_m_precedence_forall_ite : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_forall_ite : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_assoc_forall : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_exists_ite : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_m_precedence_exists_ite : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_exists_ite : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_assoc_exist : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_let_ite : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_m_precedence_let_ite : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_let_ite : Unknown
-[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_assoc_naming : Unknown
+[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_precedence_xor_and : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_r_precedence_xor_and : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_precedence_or_xor : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_r_precedence_or_xor : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_precedence_implies_or : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_assoc_implies : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_r_precedence_equiv_implies : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bitwise_ensures_ko_l_precedence_equiv_implies : Unsuccess
+[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_r_precedence_and_eq : Unsuccess
+[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_l_precedence_and_eq : Unsuccess
+[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_l_nonassoc_eq : Unsuccess
+[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_r_nonassoc_eq : Unsuccess
+[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_r_precedence_and_neq : Unsuccess
+[wp] [Alt-Ergo] Goal typed_comparison_ensures_ko_l_precedence_and_neq : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_xor_and : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_xor_and : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_or_xor : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_or_xor : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_implies_or : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_assoc_implies : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_equiv_implies : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_equiv_implies : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_ite_equiv : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_ite_equiv : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_assoc_ite : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_forall_ite : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_m_precedence_forall_ite : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_forall_ite : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_assoc_forall : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_exists_ite : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_m_precedence_exists_ite : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_exists_ite : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_assoc_exist : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_r_precedence_let_ite : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_m_precedence_let_ite : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_precedence_let_ite : Unsuccess
+[wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_assoc_naming : Unsuccess
[wp] Proved goals: 0 / 37
- Alt-Ergo: 0 (unknown: 37)
+ Alt-Ergo: 0 (unsuccess: 37)
[wp] Report 'tests/wp_acsl/precedence.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle
index 1134f87973041a8458dc62fa39859376138ef84f..f5b9a5420564d1bf4008a47c8532986445da978e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle
@@ -7,13 +7,13 @@
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ok : Valid
[wp] [Alt-Ergo] Goal typed_g_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_modifies_x_ensures_qed_ok_F_OK : Valid
-[wp] [Alt-Ergo] Goal typed_modifies_x_ensures_qed_ok_W_OK_todo : Unknown
+[wp] [Alt-Ergo] Goal typed_modifies_x_ensures_qed_ok_W_OK_todo : Unsuccess
[wp] [Qed] Goal typed_modifies_y_ensures_qed_ok_F_OK : Valid
[wp] [Qed] Goal typed_modifies_y_ensures_qed_ok_G_OK : Valid
-[wp] [Alt-Ergo] Goal typed_modifies_y_ensures_qed_ok_W_OK_todo : Unknown
+[wp] [Alt-Ergo] Goal typed_modifies_y_ensures_qed_ok_W_OK_todo : Unsuccess
[wp] Proved goals: 5 / 7
Qed: 3
- Alt-Ergo: 2 (unknown: 2)
+ Alt-Ergo: 2 (unsuccess: 2)
[wp] Report 'tests/wp_acsl/reads.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle
index d35f0f34da7689d26651e64ae1adf2cb9de89f6d..ccb9ad6d07a333b76c3e2d3057cf3701934066e9 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle
@@ -4,11 +4,11 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
-[wp] [Alt-Ergo] Goal typed_modifies_x_ensures_qed_ko_G_KO : Unknown
-[wp] [Alt-Ergo] Goal typed_modifies_x_ensures_qed_ko_H_KO : Unknown
-[wp] [Alt-Ergo] Goal typed_modifies_y_ensures_qed_ko_H_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_modifies_x_ensures_qed_ko_G_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_modifies_x_ensures_qed_ko_H_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_modifies_y_ensures_qed_ko_H_KO : Unsuccess
[wp] Proved goals: 0 / 3
- Alt-Ergo: 0 (unknown: 3)
+ Alt-Ergo: 0 (unsuccess: 3)
[wp] Report 'tests/wp_acsl/reads.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle
index 72d59398c6be91dad9e49ad0527e4fbe318b36ab..b5fa183f53fd5aeb360f357364331ac1a78eb0fd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle
@@ -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_ensures_KP5_qed_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_f_ensures_KP5_qed_ko : Unsuccess
[wp] Proved goals: 0 / 1
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_acsl/record.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle
index c79e18f32beff0106a9501e7819fa5cd7491182e..dce325df60f2bbe9a387f7a250800092f12c4ab8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle
@@ -4,10 +4,10 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_caveat_f_ensures_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_caveat_g_ensures_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_caveat_f_ensures_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_caveat_g_ensures_ko : Unsuccess
[wp] Proved goals: 0 / 2
- Alt-Ergo: 0 (unknown: 2)
+ Alt-Ergo: 0 (unsuccess: 2)
[wp] Report 'tests/wp_acsl/struct_use_case.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle
index 4c0a4a82d065b3f536d0d7f827695ee0651a7645..25cc92fe77cee318b601983e2da2628116ee64f7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle
@@ -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_ensures_qed_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess
[wp] Proved goals: 0 / 1
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_acsl/type_guard.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle
index ee02448280b4c73aa34876eb3a4874e1c0502ffe..d5c9648c9d9d36c855907cc05b7834a541649234 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle
@@ -7,10 +7,10 @@
[wp] [Qed] Goal typed_rotate_left_ensures_bit_zero : Valid
[wp] [Alt-Ergo] Goal typed_rotate_left_ensures_other_bits : Valid
[wp] [Qed] Goal typed_sum_ensures_ok : Valid
-[wp] [Alt-Ergo] Goal typed_sum_ensures_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_sum_ensures_ko : Unsuccess
[wp] Proved goals: 3 / 4
Qed: 2
- Alt-Ergo: 1 (unknown: 1)
+ Alt-Ergo: 1 (unsuccess: 1)
[wp] Report 'tests/wp_acsl/unit_bit_test.c.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle
index 25a1b0cae037d1c7fb6fdbbfff453344fa380fc0..e25eb05dbab6975d2e0eeff52c68aa272b31be9f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle
@@ -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_ensures_qed_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess
[wp] Proved goals: 0 / 1
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_acsl/user_def_type_guard.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
index 127196767780aace8ed7c0ed30048afe85d8f93d..57d0e72ba574007a74eaf0ae8a8eac436014c897 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
@@ -5,10 +5,10 @@
[rte] annotating function f
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_assert : Valid
-[wp] [Alt-Ergo] Goal typed_f_assert_rte_mem_access : Unknown
+[wp] [Alt-Ergo] Goal typed_f_assert_rte_mem_access : Unsuccess
[wp] Proved goals: 1 / 2
Qed: 0
- Alt-Ergo: 1 (unknown: 1)
+ Alt-Ergo: 1 (unsuccess: 1)
[wp] Report 'tests/wp_bts/bts779.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
index 286ecc0a8dee3fb7dba30c53a896e206bf001fc9..1c324eef37b4e64a5e03e2568d664d08a010b915 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
@@ -13,11 +13,11 @@
[wp] [Qed] Goal typed_foo_wrong_ensures : Valid
[wp] [Qed] Goal typed_foo_wrong_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_foo_wrong_assert_rte_mem_access_2 : Valid
-[wp] [Alt-Ergo] Goal typed_foo_wrong_assert_rte_mem_access_3 : Unknown
+[wp] [Alt-Ergo] Goal typed_foo_wrong_assert_rte_mem_access_3 : Unsuccess
[wp] [Qed] Goal typed_foo_wrong_assigns : Valid
[wp] Proved goals: 9 / 10
Qed: 8
- Alt-Ergo: 1 (unknown: 1)
+ Alt-Ergo: 1 (unsuccess: 1)
[wp] Report 'tests/wp_bts/bts_1360.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle
index fcbb90261d3d8c3ab690bfc37fec3a81edc9ac22..d5c0104b1871bbb379e6971fedb6b04e7b63df99 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle
@@ -9,7 +9,7 @@
[wp] [Qed] Goal typed_local_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_local_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_wrong_assert_for_value : Valid
-[wp] [Alt-Ergo] Goal typed_wrong_loop_invariant_A_KO_preserved : Unknown
+[wp] [Alt-Ergo] Goal typed_wrong_loop_invariant_A_KO_preserved : Unsuccess
[wp] [Qed] Goal typed_wrong_loop_invariant_A_KO_established : Valid
[wp] [Qed] Goal typed_wrong_loop_invariant_B_preserved : Valid
[wp] [Qed] Goal typed_wrong_loop_invariant_B_established : Valid
@@ -19,7 +19,7 @@
[wp] [Qed] Goal typed_wrong_loop_assigns : Valid
[wp] Proved goals: 12 / 13
Qed: 10
- Alt-Ergo: 2 (unknown: 1)
+ Alt-Ergo: 2 (unsuccess: 1)
[wp] Report 'tests/wp_bts/bts_1462.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle
index 2dd381f40d3f750773b19857a69fc1372df87e55..300282b34a9d81b83976ae30b4dff16febc45130 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle
@@ -6,11 +6,11 @@
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_compute_bizarre_Bizarre_ensures_TRANS : Valid
[wp] [Qed] Goal typed_compute_normal_Normal_ensures_TRANS : Valid
-[wp] [Alt-Ergo] Goal typed_main_bizarre_KO_assert_FALSE : Unknown
-[wp] [Alt-Ergo] Goal typed_main_normal_KO_assert_FALSE : Unknown
+[wp] [Alt-Ergo] Goal typed_main_bizarre_KO_assert_FALSE : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_normal_KO_assert_FALSE : Unsuccess
[wp] Proved goals: 2 / 4
Qed: 2
- Alt-Ergo: 0 (unknown: 2)
+ Alt-Ergo: 0 (unsuccess: 2)
[wp] Report 'tests/wp_bts/bts_1586.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
index d9d788c7c7b07fb0911308c1b3170d9051a90d17..c1f6dc0e2ae85a7b1090fc9b62f6cff9ccf983ce 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle
@@ -4,15 +4,15 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
-[wp] [Alt-Ergo] Goal typed_global_frame_ensures_sep_iff_ref : Unknown
-[wp] [Alt-Ergo] Goal typed_global_frame_ensures_one_iff_ref : Unknown
+[wp] [Alt-Ergo] Goal typed_global_frame_ensures_sep_iff_ref : Unsuccess
+[wp] [Alt-Ergo] Goal typed_global_frame_ensures_one_iff_ref : Unsuccess
[wp] [Qed] Goal typed_global_frame_ensures_zero_always : Valid
[wp] [Qed] Goal typed_global_frame_assert_ok : Valid
[wp] [Qed] Goal typed_global_frame_assert_ok_2 : Valid
[wp] [Alt-Ergo] Goal typed_local_frame_assert_ok : Valid
[wp] Proved goals: 4 / 6
Qed: 3
- Alt-Ergo: 1 (unknown: 2)
+ Alt-Ergo: 1 (unsuccess: 2)
[wp] Report 'tests/wp_bts/bts_1828.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle
index 88a873c857cfc22dfeccbc23a480d184dae469b5..0bdfc3c776943da644f8345d5b125927ba59928f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle
@@ -5,11 +5,11 @@
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_job_ko_fixed_assert_Wrong : Unknown
-[wp] [Alt-Ergo] Goal typed_job_ko_success_assert_Wrong : Unknown
+[wp] [Alt-Ergo] Goal typed_job_ko_fixed_assert_Wrong : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_ko_success_assert_Wrong : Unsuccess
[wp] Proved goals: 1 / 3
Qed: 0
- Alt-Ergo: 1 (unknown: 2)
+ Alt-Ergo: 1 (unsuccess: 2)
[wp] Report 'tests/wp_bts/issue_494.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle
index bfdcf78517ee881e901469d2e70c43bc0d3b37db..d0b99a55052bde7b45bcb91f3d9afc39187fe309 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle
@@ -15,10 +15,10 @@
[wp] [Qed] Goal typed_pointer_ensures : Valid
[wp] [Qed] Goal typed_pointer_call_f_requires : Valid
[wp] [Qed] Goal typed_wrong_without_ref_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_wrong_without_ref_call_f_requires : Unknown
+[wp] [Alt-Ergo] Goal typed_wrong_without_ref_call_f_requires : Unsuccess
[wp] Proved goals: 11 / 12
Qed: 11
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_hoare/byref.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
index c33ec4bf50b7ab3be30245accec6b646e6b73cf1..0dd9bdf4efe543c3438e155deb4a11b58c01ee85 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle
@@ -7,10 +7,10 @@
[wp] [Qed] Goal typed_ref_call_f2_ensures : Valid
[wp] [Qed] Goal typed_ref_call_f2_assigns_exit_part1 : Valid
[wp] [Qed] Goal typed_ref_call_f2_assigns_exit_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_ref_call_f2_assigns_exit_part3 : Unknown
+[wp] [Alt-Ergo] Goal typed_ref_call_f2_assigns_exit_part3 : Unsuccess
[wp] [Qed] Goal typed_ref_call_f2_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_ref_call_f2_assigns_normal_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_ref_call_f2_assigns_normal_part3 : Unknown
+[wp] [Alt-Ergo] Goal typed_ref_call_f2_assigns_normal_part3 : Unsuccess
[wp] [Qed] Goal typed_ref_call_f2_assigns_normal_part4 : Valid
[wp] [Qed] Goal typed_ref_call_f2_call_f2_requires : Valid
[wp] [Qed] Goal typed_ref_call_global_ensures : Valid
@@ -29,7 +29,7 @@
[wp] [Qed] Goal typed_ref_write_assigns : Valid
[wp] Proved goals: 21 / 23
Qed: 21
- Alt-Ergo: 0 (unknown: 2)
+ Alt-Ergo: 0 (unsuccess: 2)
[wp] Report 'tests/wp_hoare/reference.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
index 07afbfc11d90ae4148f52336769ac7e05eea9240..b183563a0deae7e95460759cbeb1ea38d98e6c09 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle
@@ -12,10 +12,10 @@
[wp] [Qed] Goal typed_ref_s_ensures_3 : Valid
[wp] [Qed] Goal typed_ref_s_ensures_4 : Valid
[wp] [Qed] Goal typed_ref_s_ensures_5 : Valid
-[wp] [Alt-Ergo] Goal typed_ref_s_ensures_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_ref_s_ensures_KO : Unsuccess
[wp] Proved goals: 8 / 9
Qed: 7
- Alt-Ergo: 1 (unknown: 1)
+ Alt-Ergo: 1 (unsuccess: 1)
[wp] Report 'tests/wp_hoare/refguards.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/convert.i b/src/plugins/wp/tests/wp_plugin/convert.i
index a62380975edb116b35a799bf16b74b67027e4205..380f6dc6405686b87144779477816abc64802aea 100644
--- a/src/plugins/wp/tests/wp_plugin/convert.i
+++ b/src/plugins/wp/tests/wp_plugin/convert.i
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-timeout 100 -wp-steps 500 -wp-share ./share -wp-msg-key shell,no-time-info,no-step-info -wp-out @PTEST_FILE@.@PTEST_NUMBER@.out @PTEST_FILE@
+ CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-timeout 100 -wp-steps 500 -wp-share ./share -wp-msg-key shell,success-only -wp-out @PTEST_FILE@.@PTEST_NUMBER@.out @PTEST_FILE@
OPT: -wp-prover alt-ergo -wp-report=tests/qualif.report
OPT: -wp-prover why3:alt-ergo -wp-report=tests/qualif-why3.report
*/
diff --git a/src/plugins/wp/tests/wp_plugin/math.i b/src/plugins/wp/tests/wp_plugin/math.i
index d5ad44b51958f9e964891777a2e844243d848256..a2120d8296fef339049046fe3f32a80cf429accc 100644
--- a/src/plugins/wp/tests/wp_plugin/math.i
+++ b/src/plugins/wp/tests/wp_plugin/math.i
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,no-time-info,no-step-info -wp-out @PTEST_FILE@.@PTEST_NUMBER@.out @PTEST_FILE@
+ CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,success-only -wp-out @PTEST_FILE@.@PTEST_NUMBER@.out @PTEST_FILE@
OPT: -wp-prover alt-ergo -wp-report=tests/qualif.report -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
OPT: -wp-prover why3:alt-ergo -wp-report=tests/qualif-why3.report -wp-prop=-ko -wp-timeout 100 -wp-steps 1500
OPT: -wp-prover alt-ergo -wp-report=tests/qualif.report -wp-prop=ko -wp-timeout 1 -wp-steps 50
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle
index 07c476c9ce818006974d6ddf657ad7642b753f66..95ecc4413a6883e323c16403071a1dbeed4fc6b2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle
@@ -5,11 +5,11 @@
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_main_assert_OK : Valid
-[wp] [Alt-Ergo] Goal typed_main_assert_KO : Unknown
-[wp] [Alt-Ergo] Goal typed_main_assigns : Unknown
+[wp] [Alt-Ergo] Goal typed_main_assert_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_assigns : Unsuccess
[wp] Proved goals: 1 / 3
Qed: 1
- Alt-Ergo: 0 (unknown: 2)
+ Alt-Ergo: 0 (unsuccess: 2)
[wp] Report 'tests/wp_plugin/asm.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
index 606944d6c95ef7f41701f7baf4198e97d50990d0..9b576523536c99e990f8e19427637bdbdbc03739 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle
@@ -4,16 +4,16 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
-[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] [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] [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] [Alt-Ergo] Goal typed_job_ensures : Unknown
+[wp] [Alt-Ergo] Goal typed_job_ensures : Unsuccess
[wp] Proved goals: 3 / 7
Qed: 2
- Alt-Ergo: 1 (unknown: 4)
+ Alt-Ergo: 1 (unsuccess: 4)
[wp] Report 'tests/wp_plugin/bool.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
index d6cbf500964e4ff7407ae0ee9c73160dbb6ee164..30dcd6fe79eccde523862af001b34620751e4679 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle
@@ -23,7 +23,7 @@
[wp] [Qed] Goal typed_guarded_call_ensures_part2 : Valid
[wp] [Qed] Goal typed_guarded_call_ensures_2_part1 : Valid
[wp] [Qed] Goal typed_guarded_call_ensures_2_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_missing_context_call_point_h1_s25 : Unknown
+[wp] [Alt-Ergo] Goal typed_missing_context_call_point_h1_s25 : Unsuccess
[wp] [Qed] Goal typed_missing_context_ensures : Valid
[wp] [Qed] Goal typed_missing_context_assigns_exit : Valid
[wp] [Qed] Goal typed_missing_context_assigns_normal_part1 : Valid
@@ -58,7 +58,7 @@
[wp] [Qed] Goal typed_some_behaviors_bhv1_assigns_normal_part5 : Valid
[wp] Proved goals: 50 / 51
Qed: 47
- Alt-Ergo: 3 (unknown: 1)
+ Alt-Ergo: 3 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/dynamic.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle
index 94e4b5d38162d1674edec315e1a9a287d5455566..3b6766f387365dc2d167cf6f46cbc22309010830 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle
@@ -5,14 +5,14 @@
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Qed] Goal typed_job_ensures_Events : Valid
-[wp] [Alt-Ergo] Goal typed_job_ensures_A_reads : Unknown
-[wp] [Alt-Ergo] Goal typed_job_ensures_B_reads : Unknown
-[wp] [Alt-Ergo] Goal typed_job_ensures_B_writes : Unknown
-[wp] [Alt-Ergo] Goal typed_job_ensures_ReadValues : Unknown
-[wp] [Alt-Ergo] Goal typed_job_ensures_WriteValues : Unknown
+[wp] [Alt-Ergo] Goal typed_job_ensures_A_reads : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_ensures_B_reads : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_ensures_B_writes : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_ensures_ReadValues : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_ensures_WriteValues : Unsuccess
[wp] Proved goals: 1 / 6
Qed: 1
- Alt-Ergo: 0 (unknown: 5)
+ Alt-Ergo: 0 (unsuccess: 5)
[wp] Report 'tests/wp_plugin/flash.c.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
index b7b96a6671885c7a7520af8435f44eae9e3e2e4a..e99bbe5258183342cb25e77f585efb9108504d2b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle
@@ -8,9 +8,9 @@
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Coq] Goal typed_output_ensures_KO : Default tactic
-[wp] [Coq] Goal typed_output_ensures_KO : Unknown
+[wp] [Coq] Goal typed_output_ensures_KO : Unsuccess
[wp] Proved goals: 0 / 1
- Coq: 0 (unknown: 1)
+ Coq: 0 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/float_format.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
index 97b86f838a739b903ae5c37ab8f562360e1d342d..4abab0bd7afe096e8c3a153f482ac9e378135d5f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle
@@ -7,9 +7,9 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
-[wp] [Alt-Ergo] Goal typed_output_ensures_KO : Step limit
+[wp] [Alt-Ergo] Goal typed_output_ensures_KO : Unsuccess
[wp] Proved goals: 0 / 1
- Alt-Ergo: 0 (interrupted: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/float_format.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
index d5a6e2d19b65c96884d80ee6a92158063f4b2a35..2559e2a4b9d05a3b8b3cbec56f4ebabaee63c66a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle
@@ -7,9 +7,9 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
-[wp] [alt-ergo] Goal typed_output_ensures_KO : Unknown
+[wp] [alt-ergo] Goal typed_output_ensures_KO : Unsuccess
[wp] Proved goals: 0 / 1
- alt-ergo: 0 (unknown: 1)
+ alt-ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/float_format.i.2.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle
index 9d641a24aef9385bf3e0db628e475248c80f9187..635a026579adb9e650a60f95550f2fe18c387ea9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle
@@ -7,9 +7,9 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
-[wp] [Alt-Ergo] Goal typed_dequal_ensures : Unknown
+[wp] [Alt-Ergo] Goal typed_dequal_ensures : Unsuccess
[wp] Proved goals: 0 / 1
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/float_real.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle
index 1ada5c75caf4987e62c791656845dd4e79966209..1d743b2e6bb3f3c5094dcdd081b4f631a38bb40b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle
@@ -4,15 +4,15 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
-[wp] [Alt-Ergo] Goal typed_alias_ensures_KO : Unknown
-[wp] [Alt-Ergo] Goal typed_global_ensures_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_alias_ensures_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_global_ensures_KO : Unsuccess
[wp] [Qed] Goal typed_local_ensures_FRAMED : Valid
-[wp] [Alt-Ergo] Goal typed_local_ensures_KO : Unknown
-[wp] [Alt-Ergo] Goal typed_localref_ensures_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_local_ensures_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_localref_ensures_KO : Unsuccess
[wp] [Qed] Goal typed_localref_assert_FRAMED : Valid
[wp] Proved goals: 2 / 6
Qed: 2
- Alt-Ergo: 0 (unknown: 4)
+ Alt-Ergo: 0 (unsuccess: 4)
[wp] Report 'tests/wp_plugin/frame.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle
index 55dfd7a78b60b76a1adbec7ce6a6e88586a8ebc7..483dc58e36e489c94a8816342e9294de9d3b0439 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle
@@ -4,13 +4,13 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
-[wp] [Alt-Ergo] Goal typed_fA_ensures_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_fA_ensures_KO : Unsuccess
[wp] [Qed] Goal typed_fB_ensures_OK : Valid
-[wp] [Alt-Ergo] Goal typed_fC_ensures_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_fC_ensures_KO : Unsuccess
[wp] [Qed] Goal typed_fD_ensures_OK : Valid
[wp] Proved goals: 2 / 4
Qed: 2
- Alt-Ergo: 0 (unknown: 2)
+ Alt-Ergo: 0 (unsuccess: 2)
[wp] Report 'tests/wp_plugin/init_const.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle
index 37a5407fe0cc5eb006eb192b74540eb830370947..7fa9591a61becc59477b16b43a6397fef16010a2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle
@@ -10,10 +10,10 @@
[wp] [Qed] Goal typed_f_ensures_Q_NotWrite : Valid
[wp] [Qed] Goal typed_g_ensures_P_not_Const : Valid
[wp] [Alt-Ergo] Goal typed_g_assert_Read : Valid
-[wp] [Alt-Ergo] Goal typed_g_assert_Guard_against_Const : Unknown
+[wp] [Alt-Ergo] Goal typed_g_assert_Guard_against_Const : Unsuccess
[wp] Proved goals: 6 / 7
Qed: 4
- Alt-Ergo: 2 (unknown: 1)
+ Alt-Ergo: 2 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/init_const_guard.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle
index 56d58accfc3dde00676746ecc7c2bf6879d04976..ec5da8c77e12e512f94b967b80ce3aa01586ff44 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle
@@ -6,11 +6,11 @@
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_f_ensures_OK : Valid
-[wp] [Alt-Ergo] Goal typed_f_ensures_KO : Unknown
-[wp] [Alt-Ergo] Goal typed_f_ensures_KO_2 : Unknown
+[wp] [Alt-Ergo] Goal typed_f_ensures_KO : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f_ensures_KO_2 : Unsuccess
[wp] Proved goals: 1 / 3
Qed: 1
- Alt-Ergo: 0 (unknown: 2)
+ Alt-Ergo: 0 (unsuccess: 2)
[wp] Report 'tests/wp_plugin/init_extern.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle
index 6e4b4317e3c942b37849c4b27aa5960db38756d4..0eda5beada338fe9c6267459a72a281b97a488eb 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle
@@ -7,10 +7,10 @@
[wp] [Qed] Goal typed_validA_assert_OK : Valid
[wp] [Qed] Goal typed_validA_assert_OK_2 : Valid
[wp] [Qed] Goal typed_validB_assert_OK : Valid
-[wp] [Alt-Ergo] Goal typed_validB_assert_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_validB_assert_KO : Unsuccess
[wp] Proved goals: 3 / 4
Qed: 3
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/init_valid.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle
index 4862a74bd900b08f9b57715585fe92acc38bc5de..7bf755e5732115dc829fc36879b22a3351e4328c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle
@@ -4,12 +4,12 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
-[wp] [Alt-Ergo] Goal typed_f_ko_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_f_ko_1_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_f_ko_1_ensures_qed_ko_2 : Unknown
-[wp] [Alt-Ergo] Goal typed_f_ko_1_ensures_qed_ko_3 : Unknown
+[wp] [Alt-Ergo] Goal typed_f_ko_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f_ko_1_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f_ko_1_ensures_qed_ko_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f_ko_1_ensures_qed_ko_3 : Unsuccess
[wp] Proved goals: 0 / 4
- Alt-Ergo: 0 (unknown: 4)
+ Alt-Ergo: 0 (unsuccess: 4)
[wp] Report 'tests/wp_plugin/injector.c.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle
index 31fb187436c43ad82a36d338ba9a42aa110a0aaf..66d473a27d59405842479224eeea1aa7688dfc5a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle
@@ -12,10 +12,10 @@
[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_init_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_assigns_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_init_assigns : Unknown
+[wp] [Alt-Ergo] Goal typed_init_assigns : Unsuccess
[wp] Proved goals: 8 / 9
Qed: 3
- Alt-Ergo: 5 (unknown: 1)
+ Alt-Ergo: 5 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/loop.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
index 820740cac730923d31743afa06ad43224d7120d5..4c36f71d73739c1ca598c2923285c6845a22d8c7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.2.res.oracle
@@ -4,17 +4,17 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_sin_asin : Step limit
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_cos_acos : Step limit
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_asin_sin : Step limit
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_acos_cos : Step limit
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_atan_tan : Step limit
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_log_pow : Step limit
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_exp_log : Step limit
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_exp_log_add_mul : Step limit
-[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_sqrt_pos : Step limit
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_sin_asin : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_cos_acos : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_asin_sin : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_acos_cos : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_atan_tan : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_log_pow : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_exp_log : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_exp_log_add_mul : Unsuccess
+[wp] [Alt-Ergo] Goal typed_ko_ensures_ko_sqrt_pos : Unsuccess
[wp] Proved goals: 0 / 9
- Alt-Ergo: 0 (interrupted: 9)
+ Alt-Ergo: 0 (unsuccess: 9)
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
ko - - 9 0.0%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
index bb249beaf01e222a7b5c8e2a99309eb00701e68f..c8da0ce71468d4f596928935394adb03d0ec72de 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/math.3.res.oracle
@@ -4,17 +4,17 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
-[wp] [alt-ergo] Goal typed_ko_ensures_ko_sin_asin : Timeout
-[wp] [alt-ergo] Goal typed_ko_ensures_ko_cos_acos : Timeout
-[wp] [alt-ergo] Goal typed_ko_ensures_ko_asin_sin : Timeout
-[wp] [alt-ergo] Goal typed_ko_ensures_ko_acos_cos : Timeout
-[wp] [alt-ergo] Goal typed_ko_ensures_ko_atan_tan : Timeout
-[wp] [alt-ergo] Goal typed_ko_ensures_ko_log_pow : Timeout
-[wp] [alt-ergo] Goal typed_ko_ensures_ko_exp_log : Timeout
-[wp] [alt-ergo] Goal typed_ko_ensures_ko_exp_log_add_mul : Timeout
-[wp] [alt-ergo] Goal typed_ko_ensures_ko_sqrt_pos : Timeout
+[wp] [alt-ergo] Goal typed_ko_ensures_ko_sin_asin : Unsuccess
+[wp] [alt-ergo] Goal typed_ko_ensures_ko_cos_acos : Unsuccess
+[wp] [alt-ergo] Goal typed_ko_ensures_ko_asin_sin : Unsuccess
+[wp] [alt-ergo] Goal typed_ko_ensures_ko_acos_cos : Unsuccess
+[wp] [alt-ergo] Goal typed_ko_ensures_ko_atan_tan : Unsuccess
+[wp] [alt-ergo] Goal typed_ko_ensures_ko_log_pow : Unsuccess
+[wp] [alt-ergo] Goal typed_ko_ensures_ko_exp_log : Unsuccess
+[wp] [alt-ergo] Goal typed_ko_ensures_ko_exp_log_add_mul : Unsuccess
+[wp] [alt-ergo] Goal typed_ko_ensures_ko_sqrt_pos : Unsuccess
[wp] Proved goals: 0 / 9
- alt-ergo: 0 (interrupted: 9)
+ alt-ergo: 0 (unsuccess: 9)
----------------------------------------------------------
Functions WP Alt-Ergo(Why3) Total Success
ko - - 9 0.0%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle
index 4e444f5c792756e54ecde7d9d12f951091879771..09dcba792d0c72d1783d78b2192292735dd860b2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle
@@ -12,13 +12,13 @@
[wp] [Qed] Goal typed_f3_ok_assigns_normal : Valid
[wp] [Qed] Goal typed_f4_ok_assigns_exit : Valid
[wp] [Qed] Goal typed_f4_ok_assigns_normal : Valid
-[wp] [Alt-Ergo] Goal typed_f5_ko_assigns_exit : Unknown
-[wp] [Alt-Ergo] Goal typed_f5_ko_assigns_normal : Unknown
-[wp] [Alt-Ergo] Goal typed_f6_ko_assigns_exit : Unknown
-[wp] [Alt-Ergo] Goal typed_f6_ko_assigns_normal : Unknown
+[wp] [Alt-Ergo] Goal typed_f5_ko_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f5_ko_assigns_normal : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f6_ko_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f6_ko_assigns_normal : Unsuccess
[wp] Proved goals: 8 / 12
Qed: 8
- Alt-Ergo: 0 (unknown: 4)
+ Alt-Ergo: 0 (unsuccess: 4)
[wp] Report 'tests/wp_plugin/overarray.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
index 16f6ce465df500059dfbd2359c7787d47e02d660..35e9b6933aa7d334cc0cafe94f3af6114b81fc1c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle
@@ -12,13 +12,13 @@
[wp] [Alt-Ergo] Goal typed_f3_ok_assigns_normal : Valid
[wp] [Alt-Ergo] Goal typed_f4_ok_assigns_exit : Valid
[wp] [Alt-Ergo] Goal typed_f4_ok_assigns_normal : Valid
-[wp] [Alt-Ergo] Goal typed_f5_ko_assigns_exit : Unknown
-[wp] [Alt-Ergo] Goal typed_f5_ko_assigns_normal : Unknown
-[wp] [Alt-Ergo] Goal typed_f6_ko_assigns_exit : Unknown
-[wp] [Alt-Ergo] Goal typed_f6_ko_assigns_normal : Unknown
+[wp] [Alt-Ergo] Goal typed_f5_ko_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f5_ko_assigns_normal : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f6_ko_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f6_ko_assigns_normal : Unsuccess
[wp] Proved goals: 8 / 12
Qed: 4
- Alt-Ergo: 4 (unknown: 4)
+ Alt-Ergo: 4 (unsuccess: 4)
[wp] Report 'tests/wp_plugin/overassign.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle
index c02d51b2502f60ff4c7e840cac217e7bba44e43e..32502e791d3adc44f89e06ea6c9145cd2db5a38a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle
@@ -7,9 +7,9 @@
Allocation, initialization and danglingness not yet implemented
(\initialized(\at(p,wp:pre)))
[wp] 1 goal scheduled
-[wp] [Alt-Ergo] Goal typed_f_assert : Unknown (Stronger)
+[wp] [Alt-Ergo] Goal typed_f_assert : Unsuccess (Stronger)
[wp] Proved goals: 0 / 1
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/polarity.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
index 1859d60bf14d74f93857487bc8a1314ef0c9151e..c1ef69535aed91d4f33ce7fbba751711bdbe85f1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.res.oracle
@@ -13,9 +13,9 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] 1 goal scheduled
-[wp] [Alt-Ergo] Goal typed_main_assert_Eva_signed_overflow : Unknown
+[wp] [Alt-Ergo] Goal typed_main_assert_Eva_signed_overflow : Unsuccess
[wp] Proved goals: 0 / 1
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 0 goal scheduled
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
index 61f7720660b11d7a738b88ebad0178c0f541447f..3749d98a6ad36a1e047d362ed40c4eeb00dcec9c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
@@ -10,15 +10,15 @@
[wp] tests/wp_plugin/rte.i:34: Warning:
Option -wp-bool-range incompatiable with RTE (ignored)
[wp] 6 goals scheduled
-[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access : Unknown
-[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access_2 : Unknown
-[wp] [Alt-Ergo] Goal typed_job_assert_rte_signed_overflow : Unknown
-[wp] [Alt-Ergo] Goal typed_job_assert_rte_signed_overflow_2 : Unknown
+[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_assert_rte_signed_overflow : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_assert_rte_signed_overflow_2 : Unsuccess
[wp] [Qed] Goal typed_job_assert_rte_mem_access_3 : Valid
-[wp] [Alt-Ergo] Goal typed_job3_assert_rte_bool_value : Unknown
+[wp] [Alt-Ergo] Goal typed_job3_assert_rte_bool_value : Unsuccess
[wp] Proved goals: 1 / 6
Qed: 1
- Alt-Ergo: 0 (unknown: 5)
+ Alt-Ergo: 0 (unsuccess: 5)
[wp] Report 'tests/wp_plugin/rte.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
index 4450cc801407543b8002c418855ad3c972f3faec..b6125143bf15f8dae93ff247ff52bea8fdd42c62 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle
@@ -4,14 +4,14 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
-[wp] [Alt-Ergo] Goal typed_f_assert_Ok_A : Unknown
+[wp] [Alt-Ergo] Goal typed_f_assert_Ok_A : Unsuccess
[wp] [Qed] Goal typed_f_assert_Ok_B : Valid
[wp] [Qed] Goal typed_f_assert_Ok_C : Valid
[wp] [Qed] Goal typed_f_assert_Ok_D : Valid
[wp] [Alt-Ergo] Goal typed_f_assert_Ok_E : Valid
[wp] Proved goals: 4 / 5
Qed: 3
- Alt-Ergo: 1 (unknown: 1)
+ Alt-Ergo: 1 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/subset_fopen.c.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
index 13c1a6e92193642c657b9833e30ce9351c426c54..2c19f508dd4fd32298bdcf4d0869d6625af79e4f 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
@@ -6,11 +6,11 @@
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_S : Valid
[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_A : Valid
-[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_B : Unknown
+[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_B : Unsuccess
[wp] [Qed] Goal typed_foo_call_fconcat_requires_qed_ok : Valid
[wp] Proved goals: 3 / 4
Qed: 1
- Alt-Ergo: 2 (unknown: 1)
+ Alt-Ergo: 2 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/trig.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle
index 5cb5f531ab2cff415b146d2960bb24cd8a29737e..b8aa2126915eed425245450cd6ce34e76a1a1f1d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle
@@ -8,10 +8,10 @@
(r1: \initialized(Y + (0 .. 99)))
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_f_assert_a1 : Valid
-[wp] [Alt-Ergo] Goal typed_f_call_cp_requires_r1 : Unknown (Degenerated)
+[wp] [Alt-Ergo] Goal typed_f_call_cp_requires_r1 : Unsuccess (Degenerated)
[wp] Proved goals: 1 / 2
Qed: 1
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_plugin/unsupported_init.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index f06015355500af3a51dab1649ecc50d3310a3a7a..060f7e15435fe72e046f671f1bbef4d7131b4a2d 100644
--- a/src/plugins/wp/tests/wp_plugin/removed.i
+++ b/src/plugins/wp/tests/wp_plugin/removed.i
@@ -1,5 +1,5 @@
/* run.config_qualif
- CMD: @frama-c@ -wp-share ./share -wp-msg-key no-time-info,no-step-info -wp-par 1 -wp-timeout 100 -wp-steps 500
+ CMD: @frama-c@ -wp-share ./share -wp-msg-key success-only -wp-par 1 -wp-timeout 100 -wp-steps 500
OPT: -eva -then -wp -then -no-eva -warn-unsigned-overflow -wp
*/
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle
index 53b6eb42b5afa2a59847fd1eb7a5f60f29705402..c491cb3a4d48773069e4040377eb707baf7aa35b 100644
--- a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle
@@ -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_qed_ko_P_oracle_ko : Step limit
-[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko_Q_oracle_ko : Step limit
+[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko_P_oracle_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko_Q_oracle_ko : Unsuccess
[wp] Proved goals: 0 / 2
- Alt-Ergo: 0 (interrupted: 2)
+ Alt-Ergo: 0 (unsuccess: 2)
[wp] Report 'tests/wp_store/nonaliasing.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
index b1263cdfe2943478bfb771d4ac1f794c4fee5daf..c11cdf6e7134b4bd112c68082f8c10628d23f91b 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
@@ -4,11 +4,11 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
-[wp] [Tactical] Goal typed_split_ensures_Goal_Exist_Or : Unknown
-[wp] [Tactical] Goal typed_split_ensures_Goal_Exist_And : Unknown
-[wp] [Tactical] Goal typed_split_ensures_Goal_Exist_And_bis : Unknown
-[wp] [Tactical] Goal typed_split_ensures_Hyp_Forall_And : Unknown
-[wp] [Tactical] Goal typed_split_ensures_Hyp_Forall_Or_bis : Unknown
+[wp] [Tactical] Goal typed_split_ensures_Goal_Exist_Or : Unsuccess
+[wp] [Tactical] Goal typed_split_ensures_Goal_Exist_And : Unsuccess
+[wp] [Tactical] Goal typed_split_ensures_Goal_Exist_And_bis : Unsuccess
+[wp] [Tactical] Goal typed_split_ensures_Hyp_Forall_And : Unsuccess
+[wp] [Tactical] Goal typed_split_ensures_Hyp_Forall_Or_bis : Unsuccess
[wp] Proved goals: 0 / 5
[wp] Report 'tests/wp_tip/tac_split_quantifiers.i.0.report.json'
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle
index a2caebabd5becd1830646d5aab478094978856a4..07921fa2d8e21c72ed45aca656d02ac7fb582c10 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle
@@ -4,12 +4,12 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
-[wp] [Alt-Ergo] Goal typed_band_int_assert_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_bnot_uchar_ensures_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_bnot_uint_ensures_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_cast_assert_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_band_int_assert_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bnot_uchar_ensures_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bnot_uint_ensures_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_cast_assert_ko : Unsuccess
[wp] Proved goals: 0 / 4
- Alt-Ergo: 0 (unknown: 4)
+ Alt-Ergo: 0 (unsuccess: 4)
[wp] Report 'tests/wp_typed/unit_bitwise.c.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle
index 9f608e372b6afc911ba866a11fb091dedc7bf480..911633abb53918de798479223d34a5dc6ead8be5 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle
@@ -6,10 +6,10 @@
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_main_requires_p_is_33FF : Valid
[wp] [Qed] Goal typed_main_requires_q_is_66F0 : Valid
-[wp] [Alt-Ergo] Goal typed_main_requires_r_is_q1_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_main_requires_r_is_q1_ko : Unsuccess
[wp] Proved goals: 2 / 3
Qed: 2
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_typed/unit_hard.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle
index 4bb7a33b0ce1f200e88ae5874eec2b8941bb2e9d..20ba906fa590daff417528bb0f15233addf2d1bb 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle
@@ -3,7 +3,7 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] 6 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_P23_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_lemma_P23_KO : Unsuccess
[wp] [Alt-Ergo] Goal typed_lemma_P52 : Valid
[wp] [Alt-Ergo] Goal typed_lemma_P13 : Valid
[wp] [Alt-Ergo] Goal typed_lemma_P14 : Valid
@@ -11,7 +11,7 @@
[wp] [Alt-Ergo] Goal typed_lemma_Foo : Valid
[wp] Proved goals: 5 / 6
Qed: 0
- Alt-Ergo: 5 (unknown: 1)
+ Alt-Ergo: 5 (unsuccess: 1)
[wp] Report 'tests/wp_typed/unit_lemma.i.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle
index b2061aaf772d9df676fc6447432bc1abb323a55a..5bc492834ba6ae6bf598ea37d07a0a8abc89de5b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle
@@ -7,10 +7,10 @@
Missing assigns clause (assigns 'everything' instead)
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_f_loop_invariant_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_f_loop_invariant_established : Unknown
+[wp] [Alt-Ergo] Goal typed_f_loop_invariant_established : Unsuccess
[wp] Proved goals: 1 / 2
Qed: 1
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_typed/unit_loopscope.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
index d703b7baa1c6cab1069eaf5fe9262a112f81e35b..36b4aa5e260103639b72a2bc50fd5c932602fabe 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle
@@ -7,10 +7,10 @@
Missing assigns clause (assigns 'everything' instead)
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_ref_f_loop_invariant_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_ref_f_loop_invariant_established : Unknown
+[wp] [Alt-Ergo] Goal typed_ref_f_loop_invariant_established : Unsuccess
[wp] Proved goals: 1 / 2
Qed: 1
- Alt-Ergo: 0 (unknown: 1)
+ Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_typed/unit_loopscope.i.1.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle
index 2f2abe5fd490075164b369f079aebb42299febfe..de8017ed01f1bc776acbb2cbaa2e6cd0427c006e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle
@@ -6,10 +6,10 @@
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_make_ensures_OK1 : Valid
[wp] [Qed] Goal typed_make_ensures_OK2 : Valid
-[wp] [Alt-Ergo] Goal typed_make_ensures_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_make_ensures_KO : Unsuccess
[wp] Proved goals: 2 / 3
Qed: 1
- Alt-Ergo: 1 (unknown: 1)
+ Alt-Ergo: 1 (unsuccess: 1)
[wp] Report 'tests/wp_typed/unit_matrix.i.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success