From 8ed5477b50e912dd74fcdc89a19371fd6f494bfb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 18 Feb 2019 18:05:20 +0100
Subject: [PATCH] [wp] use success-only for qualif
---
src/plugins/wp/register.ml | 2 +-
src/plugins/wp/tests/test_config_qualif | 2 +-
.../stmtcompiler_test.res.oracle | 18 ++---
.../wp/oracle_qualif/wp_behav.0.res.oracle | 14 ++--
.../wp/oracle_qualif/wp_behav.1.res.oracle | 18 ++---
.../wp/oracle_qualif/wp_strategy.res.oracle | 18 ++---
src/plugins/wp/tests/wp/stmtcompiler_test.i | 2 +-
.../wp/tests/wp/stmtcompiler_test_rela.i | 2 +-
src/plugins/wp/tests/wp/wp_strategy.c | 2 +-
.../wp_acsl/oracle_qualif/arith.1.res.oracle | 4 +-
.../oracle_qualif/assigns_range.1.res.oracle | 14 ++--
.../wp_acsl/oracle_qualif/axioms.res.oracle | 6 +-
.../wp_acsl/oracle_qualif/bitwise.res.oracle | 8 +-
.../wp_acsl/oracle_qualif/cnf.res.oracle | 2 +-
.../oracle_qualif/div_mod.2.res.oracle | 6 +-
.../oracle_qualif/init_label.res.oracle | 4 +-
.../oracle_qualif/init_value.1.res.oracle | 38 +++++-----
.../oracle_qualif/label_escape.1.res.oracle | 4 +-
.../wp_acsl/oracle_qualif/logic.res.oracle | 34 ++++-----
.../oracle_qualif/pointer.0.res.oracle | 14 ++--
.../oracle_qualif/pointer.1.res.oracle | 14 ++--
.../oracle_qualif/post_result.res.oracle | 4 +-
.../oracle_qualif/precedence.1.res.oracle | 76 +++++++++----------
.../wp_acsl/oracle_qualif/reads.0.res.oracle | 6 +-
.../wp_acsl/oracle_qualif/reads.1.res.oracle | 8 +-
.../wp_acsl/oracle_qualif/record.1.res.oracle | 4 +-
.../struct_use_case.1.res.oracle | 6 +-
.../oracle_qualif/type_guard.1.res.oracle | 4 +-
.../oracle_qualif/unit_bit_test.res.oracle | 4 +-
.../user_def_type_guard.1.res.oracle | 4 +-
.../wp_bts/oracle_qualif/bts779.res.oracle | 4 +-
.../wp_bts/oracle_qualif/bts_1360.res.oracle | 4 +-
.../wp_bts/oracle_qualif/bts_1462.res.oracle | 4 +-
.../wp_bts/oracle_qualif/bts_1586.res.oracle | 6 +-
.../oracle_qualif/bts_1828.0.res.oracle | 6 +-
.../wp_bts/oracle_qualif/issue_494.res.oracle | 6 +-
.../wp_hoare/oracle_qualif/byref.0.res.oracle | 4 +-
.../oracle_qualif/reference.res.oracle | 6 +-
.../oracle_qualif/refguards.res.oracle | 4 +-
src/plugins/wp/tests/wp_plugin/convert.i | 2 +-
src/plugins/wp/tests/wp_plugin/math.i | 2 +-
.../wp_plugin/oracle_qualif/asm.res.oracle | 6 +-
.../wp_plugin/oracle_qualif/bool.0.res.oracle | 10 +--
.../oracle_qualif/dynamic.res.oracle | 4 +-
.../oracle_qualif/flash.0.res.oracle | 12 +--
.../oracle_qualif/float_format.0.res.oracle | 4 +-
.../oracle_qualif/float_format.1.res.oracle | 4 +-
.../oracle_qualif/float_format.2.res.oracle | 4 +-
.../oracle_qualif/float_real.1.res.oracle | 4 +-
.../wp_plugin/oracle_qualif/frame.res.oracle | 10 +--
.../oracle_qualif/init_const.res.oracle | 6 +-
.../oracle_qualif/init_const_guard.res.oracle | 4 +-
.../oracle_qualif/init_extern.res.oracle | 6 +-
.../oracle_qualif/init_valid.res.oracle | 4 +-
.../oracle_qualif/injector.1.res.oracle | 10 +--
.../wp_plugin/oracle_qualif/loop.res.oracle | 4 +-
.../wp_plugin/oracle_qualif/math.2.res.oracle | 20 ++---
.../wp_plugin/oracle_qualif/math.3.res.oracle | 20 ++---
.../oracle_qualif/overarray.res.oracle | 10 +--
.../oracle_qualif/overassign.res.oracle | 10 +--
.../oracle_qualif/polarity.res.oracle | 4 +-
.../oracle_qualif/removed.res.oracle | 4 +-
.../wp_plugin/oracle_qualif/rte.res.oracle | 12 +--
.../oracle_qualif/subset_fopen.res.oracle | 4 +-
.../wp_plugin/oracle_qualif/trig.res.oracle | 4 +-
.../oracle_qualif/unsupported_init.res.oracle | 4 +-
src/plugins/wp/tests/wp_plugin/removed.i | 2 +-
.../oracle_qualif/nonaliasing.1.res.oracle | 6 +-
.../tac_split_quantifiers.res.oracle | 10 +--
.../oracle_qualif/unit_bitwise.1.res.oracle | 10 +--
.../oracle_qualif/unit_hard.res.oracle | 4 +-
.../oracle_qualif/unit_lemma.res.oracle | 4 +-
.../oracle_qualif/unit_loopscope.0.res.oracle | 4 +-
.../oracle_qualif/unit_loopscope.1.res.oracle | 4 +-
.../oracle_qualif/unit_matrix.res.oracle | 4 +-
75 files changed, 311 insertions(+), 311 deletions(-)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index a21ded01520..98c9a894acf 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 8006bdebe92..e8a8597428d 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 d2ce6cd6a42..d3b2208c9f1 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 1b6f43fb505..78a9e8c0f3f 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 745a17600fa..bc1f4d8ead0 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 8dfdb335c2b..71f60a87453 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 b4b68fb8812..264b9e58d48 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 d5c4846b870..4dafe25db11 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 af3b27b5f8d..0afd35c1320 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 473a012c3e2..67dde50a424 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 73d00d5b60c..62dbc55d245 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 f5638f7fcd1..1af8a459bfd 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 3e2273eac83..74ff28899fe 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 6ebd97b44fd..bc588e84733 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 dd6bba2a705..3d3ad3145f0 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 c3f090839d6..b4b67bf6b9f 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 6fd6542afa8..ab90d518152 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 8c92ea1ed5d..32bbae5f36c 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 d22e02bbbd1..26b176ac8f2 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 7c36192fd7a..b319d2b2537 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 ae8ae26c94a..77732b04cfe 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 0bdbeee3cfe..4df28dabcef 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 b5d9d479c01..d8de2ea9bac 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 1134f879730..f5b9a542056 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 d35f0f34da7..ccb9ad6d07a 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 72d59398c6b..b5fa183f53f 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 c79e18f32be..dce325df60f 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 4c0a4a82d06..25cc92fe77c 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 ee02448280b..d5c9648c9d9 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 25a1b0cae03..e25eb05dbab 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 12719676778..57d0e72ba57 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 286ecc0a8de..1c324eef37b 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 fcbb90261d3..d5c0104b187 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 2dd381f40d3..300282b34a9 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 d9d788c7c7b..c1f6dc0e2ae 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 88a873c857c..0bdfc3c7769 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 bfdcf78517e..d0b99a55052 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 c33ec4bf50b..0dd9bdf4efe 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 07afbfc11d9..b183563a0de 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 a62380975ed..380f6dc6405 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 d5ad44b5195..a2120d8296f 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 07c476c9ce8..95ecc4413a6 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 606944d6c95..9b576523536 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 d6cbf500964..30dcd6fe79e 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 94e4b5d3816..3b6766f3873 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 b7b96a66718..e99bbe52581 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 97b86f838a7..4abab0bd7af 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 d5a6e2d19b6..2559e2a4b9d 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 9d641a24aef..635a026579a 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 1ada5c75caf..1d743b2e6bb 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 55dfd7a78b6..483dc58e36e 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 37a5407fe0c..7fa9591a61b 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 56d58accfc3..ec5da8c77e1 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 6e4b4317e3c..0eda5beada3 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 4862a74bd90..7bf755e5732 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 31fb187436c..66d473a27d5 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 820740cac73..4c36f71d737 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 bb249beaf01..c8da0ce7146 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 4e444f5c792..09dcba792d0 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 16f6ce465df..35e9b6933aa 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 c02d51b2502..32502e791d3 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 1859d60bf14..c1ef69535ae 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 61f7720660b..3749d98a6ad 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 4450cc80140..b6125143bf1 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 13c1a6e9219..2c19f508dd4 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 5cb5f531ab2..b8aa2126915 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 f0601535550..060f7e15435 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 53b6eb42b5a..c491cb3a4d4 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 b1263cdfe29..c11cdf6e713 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 a2caebabd5b..07921fa2d8e 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 9f608e372b6..911633abb53 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 4bb7a33b0ce..20ba906fa59 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 b2061aaf772..5bc492834ba 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 d703b7baa1c..36b4aa5e260 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 2f2abe5fd49..de8017ed01f 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
--
GitLab