Merge branch 'feature/wp/unsuccess-status' into 'master'

[wp] key success-only for qualif tests

See merge request frama-c/frama-c!2161

src/plugins/wp/VCS.ml

@@ -27,6 +27,7 @@
 let dkey_no_time_info = Wp_parameters.register_category "no-time-info"
 let dkey_no_step_info = Wp_parameters.register_category "no-step-info"
 let dkey_no_goals_info = Wp_parameters.register_category "no-goals-info"
+let dkey_success_only = Wp_parameters.register_category "success-only"
 
 type prover =
   | Why3 of string (* Prover via WHY *)
@@ -339,8 +340,12 @@ let pp_res ~extended fmt r =
   | NoResult -> Format.pp_print_string fmt (if extended then "No Result" else "-")
   | Invalid -> Format.pp_print_string fmt "Invalid"
   | Computing _ -> Format.pp_print_string fmt "Computing"
-  | Valid -> Format.fprintf fmt "Valid%a" (pp_perf ~extended) r
   | Checked -> Format.fprintf fmt "Typechecked"
+  | Valid when Wp_parameters.has_dkey dkey_success_only ->
+      Format.pp_print_string fmt "Valid"
+  | (Timeout|Stepout|Unknown) when Wp_parameters.has_dkey dkey_success_only ->
+      Format.pp_print_string fmt "Unsuccess"
+  | Valid -> Format.fprintf fmt "Valid%a" (pp_perf ~extended) r
   | Unknown -> Format.fprintf fmt "Unknown%a" (pp_perf ~extended) r
   | Timeout -> Format.fprintf fmt "Timeout%a" (pp_perf ~extended) r
   | Stepout -> Format.fprintf fmt "Step limit%a" (pp_perf ~extended) r

src/plugins/wp/VCS.mli

@@ -138,3 +138,4 @@ val best : result list -> result
 val dkey_no_time_info: Wp_parameters.category
 val dkey_no_step_info: Wp_parameters.category
 val dkey_no_goals_info: Wp_parameters.category
+val dkey_success_only: Wp_parameters.category

src/plugins/wp/register.ml

@@ -359,39 +359,62 @@ let do_wpo_success goal s =
           Wp_parameters.feedback ~ontty:`Silent
             "[%a] Goal %s : Valid" VCS.pp_prover prover (Wpo.get_gid goal)
 
+let do_report_time fmt s =
+  begin
+    if s.n_time > 0 &&
+       s.u_time > Rformat.epsilon &&
+       not (Wp_parameters.has_dkey VCS.dkey_no_time_info) &&
+       not (Wp_parameters.has_dkey VCS.dkey_success_only)
+    then
+      let mean = s.a_time /. float s.n_time in
+      let epsilon = 0.05 *. mean in
+      let delta = s.u_time -. s.d_time in
+      if delta < epsilon then
+        Format.fprintf fmt " (%a)" Rformat.pp_time mean
+      else
+        let middle = (s.u_time +. s.d_time) *. 0.5 in
+        if abs_float (middle -. mean) < epsilon then
+          Format.fprintf fmt " (%a-%a)"
+            Rformat.pp_time s.d_time
+            Rformat.pp_time s.u_time
+        else
+          Format.fprintf fmt " (%a-%a-%a)"
+            Rformat.pp_time s.d_time
+            Rformat.pp_time mean
+            Rformat.pp_time s.u_time
+  end
+
+let do_report_steps fmt s =
+  begin
+    if s.steps > 0 &&
+       not (Wp_parameters.has_dkey VCS.dkey_no_step_info) &&
+       not (Wp_parameters.has_dkey VCS.dkey_success_only)
+    then
+      Format.fprintf fmt " (%d)" s.steps ;
+  end
+
+let do_report_stopped fmt s =
+  if Wp_parameters.has_dkey VCS.dkey_success_only then
+    begin
+      let n = s.interrupted + s.unknown in
+      if n > 0 then
+        Format.fprintf fmt " (unsuccess: %d)" n ;
+    end
+  else
+    begin
+      if s.interrupted > 0 then
+        Format.fprintf fmt " (interrupted: %d)" s.interrupted ;
+      if s.unknown > 0 then
+        Format.fprintf fmt " (unknown: %d)" s.unknown ;
+    end
+
 let do_report_prover_stats pp_prover fmt (p,s) =
   begin
     let name = VCS.title_of_prover p in
     Format.fprintf fmt "%a %4d " pp_prover name s.proved ;
-    begin
-      if s.n_time > 0 &&
-         s.u_time > Rformat.epsilon &&
-         not (Wp_parameters.has_dkey VCS.dkey_no_time_info)
-      then
-        let mean = s.a_time /. float s.n_time in
-        let epsilon = 0.05 *. mean in
-        let delta = s.u_time -. s.d_time in
-        if delta < epsilon then
-          Format.fprintf fmt " (%a)" Rformat.pp_time mean
-        else
-          let middle = (s.u_time +. s.d_time) *. 0.5 in
-          if abs_float (middle -. mean) < epsilon then
-            Format.fprintf fmt " (%a-%a)"
-              Rformat.pp_time s.d_time
-              Rformat.pp_time s.u_time
-          else
-            Format.fprintf fmt " (%a-%a-%a)"
-              Rformat.pp_time s.d_time
-              Rformat.pp_time mean
-              Rformat.pp_time s.u_time
-    end ;
-    if s.steps > 0  &&
-       not (Wp_parameters.has_dkey VCS.dkey_no_step_info) then
-      Format.fprintf fmt " (%d)" s.steps ;
-    if s.interrupted > 0 then
-      Format.fprintf fmt " (interrupted: %d)" s.interrupted ;
-    if s.unknown > 0 then
-      Format.fprintf fmt " (unknown: %d)" s.unknown ;
+    do_report_time fmt s ;
+    do_report_steps fmt s ;
+    do_report_stopped fmt s ;
     if s.failed > 0 then
       Format.fprintf fmt " (failed: %d)" s.failed ;
     Format.fprintf fmt "@\n" ;

src/plugins/wp/tests/test_config_qualif

-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 90 -wp-share ./share -wp-msg-key shell,no-time-info,no-step-info -wp-report-json @PTEST_FILE@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-out @PTEST_FILE@.@PTEST_NUMBER@.out @PTEST_FILE@
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 90 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_FILE@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-out @PTEST_FILE@.@PTEST_NUMBER@.out @PTEST_FILE@
 OPT:

src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle

@@ -13,33 +13,33 @@
 [wp] [Qed] Goal typed_behavior2_assert : Valid
 [wp] [Qed] Goal typed_behavior3_assert : Valid
 [wp] [Qed] Goal typed_behavior4_assert : Valid
-[wp] [Alt-Ergo] Goal typed_behavior5_assert_bad : Unknown
+[wp] [Alt-Ergo] Goal typed_behavior5_assert_bad : Unsuccess
 [wp] [Qed] Goal typed_compare_assert : Valid
 [wp] [Qed] Goal typed_empty_assert : Valid
 [wp] [Alt-Ergo] Goal typed_if_assert_assert : Valid
-[wp] [Alt-Ergo] Goal typed_if_assert_assert_2 : Unknown
+[wp] [Alt-Ergo] Goal typed_if_assert_assert_2 : Unsuccess
 [wp] [Qed] Goal typed_if_assert_assert_3 : Valid
-[wp] [Alt-Ergo] Goal typed_if_assert_assert_missing_return : Unknown
+[wp] [Alt-Ergo] Goal typed_if_assert_assert_missing_return : Unsuccess
 [wp] [Qed] Goal typed_main_assert : Valid
 [wp] [Qed] Goal typed_main_assigns_global_assert : Valid
 [wp] [Qed] Goal typed_main_assigns_global_assert_2 : Valid
-[wp] [Alt-Ergo] Goal typed_main_assigns_global_assert_bad : Unknown
+[wp] [Alt-Ergo] Goal typed_main_assigns_global_assert_bad : Unsuccess
 [wp] [Qed] Goal typed_main_ensures_result_assert : Valid
-[wp] [Alt-Ergo] Goal typed_not_main_assert_bad : Unknown
+[wp] [Alt-Ergo] Goal typed_not_main_assert_bad : Unsuccess
 [wp] [Qed] Goal typed_one_assign_assert : Valid
 [wp] [Qed] Goal typed_one_if_assert : Valid
 [wp] [Qed] Goal typed_some_seq_assert : Valid
 [wp] [Qed] Goal typed_some_seq_assert_2 : Valid
 [wp] [Qed] Goal typed_zloop_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_zloop_loop_invariant_preserved : Unknown
+[wp] [Alt-Ergo] Goal typed_zloop_loop_invariant_preserved : Unsuccess
 [wp] [Qed] Goal typed_zloop_loop_invariant_established : Valid
 [wp] [Qed] Goal typed_zloop_assert : Valid
 [wp] [Qed] Goal typed_zloop_assert_2 : Valid
-[wp] [Alt-Ergo] Goal typed_zloop_assert_3 : Unknown
-[wp] [Alt-Ergo] Goal typed_zloop_assert_bad : Unknown
+[wp] [Alt-Ergo] Goal typed_zloop_assert_3 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_zloop_assert_bad : Unsuccess
 [wp] Proved goals:   19 / 27
   Qed:            18 
-  Alt-Ergo:        1  (unknown: 8)
+  Alt-Ergo:        1  (unsuccess: 8)
 [wp] Report 'tests/wp/stmtcompiler_test.i.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success

src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle

@@ -14,13 +14,13 @@
 [wp] tests/wp/wp_behav.c:81: Warning: 
   Missing assigns clause (assigns 'everything' instead)
 [wp] 38 goals scheduled
-[wp] [Alt-Ergo] Goal typed_assert_needed_assert_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_assert_needed_assert_ko : Unsuccess
 [wp] [Qed] Goal typed_assert_needed_assert_qed_ok_ok_with_hyp : Valid
 [wp] [Alt-Ergo] Goal typed_bhv_complete_pos_neg : Valid
 [wp] [Qed] Goal typed_bhv_neg_ensures_qed_ok : Valid
 [wp] [Qed] Goal typed_bhv_pos_ensures_qed_ok : Valid
-[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko1 : Unknown
-[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko2 : Unknown
+[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko1 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko2 : Unsuccess
 [wp] [Qed] Goal typed_f_ensures_qed_ok : Valid
 [wp] [Qed] Goal typed_f_x1_ensures_qed_ok : Valid
 [wp] [Qed] Goal typed_f_assert_qed_ok : Valid
@@ -36,12 +36,12 @@
 [wp] [Qed] Goal typed_more_stmt_assigns_blk_assigns_part1 : Valid
 [wp] [Qed] Goal typed_more_stmt_assigns_blk_assigns_part2 : Valid
 [wp] [Qed] Goal typed_part_stmt_bhv_b1_ensures_qed_ok : Valid
-[wp] [Alt-Ergo] Goal typed_part_stmt_bhv_bs_ensures : Unknown
+[wp] [Alt-Ergo] Goal typed_part_stmt_bhv_bs_ensures : Unsuccess
 [wp] [Alt-Ergo] Goal typed_razT_loop_invariant_qed_ok_preserved : Valid
 [wp] [Qed] Goal typed_razT_loop_invariant_qed_ok_established : Valid
-[wp] [Alt-Ergo] Goal typed_razT_b1_ensures_e1 : Unknown
+[wp] [Alt-Ergo] Goal typed_razT_b1_ensures_e1 : Unsuccess
 [wp] [Qed] Goal typed_stmt_assigns_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_stmt_assigns_assigns : Unknown
+[wp] [Alt-Ergo] Goal typed_stmt_assigns_assigns : Unsuccess
 [wp] [Qed] Goal typed_stmt_contract_requires_qed_ok : Valid
 [wp] [Qed] Goal typed_stmt_contract_ensures_qed_ok : Valid
 [wp] [Qed] Goal typed_stmt_contract_ok_ensures_qed_ok : Valid
@@ -54,7 +54,7 @@
 [wp] [Qed] Goal typed_stmt_contract_label_ensures_qed_ok : Valid
 [wp] Proved goals:   32 / 38
   Qed:            30 
-  Alt-Ergo:        2  (unknown: 6)
+  Alt-Ergo:        2  (unsuccess: 6)
 [wp] Report 'tests/wp/wp_behav.c.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success

src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle

@@ -8,16 +8,16 @@
 [wp] tests/wp/wp_behav.c:69: Warning: 
   Missing assigns clause (assigns 'everything' instead)
 [wp] 8 goals scheduled
-[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_f_x1_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_f_x2_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_min_bx_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_min_by_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_stmt_contract_ko_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_stmt_contract_ko_without_asgn_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_stmt_contract_assigns_ko_ensures_qed_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f_x1_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f_x2_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_min_bx_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_min_by_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_stmt_contract_ko_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_stmt_contract_ko_without_asgn_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_stmt_contract_assigns_ko_ensures_qed_ko : Unsuccess
 [wp] Proved goals:    0 / 8
-  Alt-Ergo:        0  (unknown: 8)
+  Alt-Ergo:        0  (unsuccess: 8)
 [wp] Report 'tests/wp/wp_behav.c.1.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success

src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle

@@ -11,34 +11,34 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] 25 goals scheduled
-[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko1 : Unknown
-[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko2 : Unknown
-[wp] [Alt-Ergo] Goal hoare_bts0513_bis_assert_qed_ko_ko1 : Unknown
+[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko1 : Unsuccess
+[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko2 : Unsuccess
+[wp] [Alt-Ergo] Goal hoare_bts0513_bis_assert_qed_ko_ko1 : Unsuccess
 [wp] [Qed] Goal hoare_bts0513_bis_assert_qed_ok_ok : Valid
 [wp] [Qed] Goal hoare_default_behaviors_ensures_qed_ok : Valid
 [wp] [Qed] Goal hoare_default_behaviors_assert_qed_ok_2 : Valid
 [wp] [Qed] Goal hoare_default_behaviors_ensures_qed_ok_stmt_p : Valid
 [wp] [Qed] Goal hoare_default_behaviors_assert_qed_ok : Valid
-[wp] [Alt-Ergo] Goal hoare_default_behaviors_assert_rte_signed_overflow : Unknown
+[wp] [Alt-Ergo] Goal hoare_default_behaviors_assert_rte_signed_overflow : Unsuccess
 [wp] [Qed] Goal hoare_default_behaviors_assigns : Valid
 [wp] [Qed] Goal hoare_dpd1_assert_qed_ok_A : Valid
-[wp] [Alt-Ergo] Goal hoare_dpd1_ensures_qed_ko_Eko : Unknown
+[wp] [Alt-Ergo] Goal hoare_dpd1_ensures_qed_ko_Eko : Unsuccess
 [wp] [Qed] Goal hoare_dpd1_assigns : Valid
 [wp] [Qed] Goal hoare_dpd2_assert_qed_ok_A : Valid
-[wp] [Alt-Ergo] Goal hoare_dpd2_ensures_qed_ko_Eko : Unknown
+[wp] [Alt-Ergo] Goal hoare_dpd2_ensures_qed_ko_Eko : Unsuccess
 [wp] [Qed] Goal hoare_dpd2_assigns : Valid
 [wp] [Qed] Goal hoare_spec_if_ensures_qed_ok_2 : Valid
 [wp] [Qed] Goal hoare_spec_if_ensures_qed_ok : Valid
 [wp] [Qed] Goal hoare_spec_if_assigns : Valid
-[wp] [Alt-Ergo] Goal hoare_spec_if_assert_rte_signed_overflow : Unknown
+[wp] [Alt-Ergo] Goal hoare_spec_if_assert_rte_signed_overflow : Unsuccess
 [wp] [Qed] Goal hoare_spec_if_assigns_2 : Valid
-[wp] [Alt-Ergo] Goal hoare_spec_if_assert_rte_signed_overflow_2 : Unknown
+[wp] [Alt-Ergo] Goal hoare_spec_if_assert_rte_signed_overflow_2 : Unsuccess
 [wp] [Qed] Goal hoare_spec_if_assigns_3 : Valid
 [wp] [Qed] Goal hoare_spec_if_cond_ensures_qed_ok : Valid
 [wp] [Qed] Goal hoare_spec_if_not_cond_ensures_qed_ok : Valid
 [wp] Proved goals:   17 / 25
   Qed:            17 
-  Alt-Ergo:        0  (unknown: 8)
+  Alt-Ergo:        0  (unsuccess: 8)
 [wp] Report 'tests/wp/wp_strategy.c.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success

src/plugins/wp/tests/wp/stmtcompiler_test.i

 /* run.config
-   OPT: -load-script tests/wp/stmtcompiler_test.ml -wp-msg-key no-time-info -wp-msg-key no-step-info
+   OPT: -load-script tests/wp/stmtcompiler_test.ml -wp-msg-key success-only
 */
 
 int empty (int c){

src/plugins/wp/tests/wp/stmtcompiler_test_rela.i

 /* run.config_qualif
-   OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key no-time-info -wp-msg-key no-step-info
+   OPT: -load-script tests/wp/stmtcompiler_test_rela.ml -wp-msg-key success-only
 */
 
 int empty (int c){

src/plugins/wp/tests/wp/wp_strategy.c

@@ -4,7 +4,7 @@ OPT: -journal-disable -wp-model Typed -wp-verbose 2 -wp-prop @assigns
 */
 
 /* run.config_qualif
-OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key "no-time-info"
+OPT: -journal-disable -rte -wp -wp-model Hoare -wp-par 1 -wp-msg-key "success-only"
 */
 /*----------------------------------------------------------------------------*/
 

src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle

@@ -4,9 +4,9 @@
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
-[wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unsuccess
 [wp] Proved goals:    0 / 1
-  Alt-Ergo:        0  (unknown: 1)
+  Alt-Ergo:        0  (unsuccess: 1)
 [wp] Report 'tests/wp_acsl/arith.i.1.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success

src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle

@@ -4,14 +4,14 @@
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
-[wp] [Alt-Ergo] Goal typed_call_assigns_t1_assigns_exit : Unknown
-[wp] [Alt-Ergo] Goal typed_call_assigns_t1_assigns_normal : Unknown
-[wp] [Alt-Ergo] Goal typed_call_assigns_t2_assigns_exit : Unknown
-[wp] [Alt-Ergo] Goal typed_call_assigns_t2_assigns_normal : Unknown
-[wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_exit : Unknown
-[wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_normal : Unknown
+[wp] [Alt-Ergo] Goal typed_call_assigns_t1_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_call_assigns_t1_assigns_normal : Unsuccess
+[wp] [Alt-Ergo] Goal typed_call_assigns_t2_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_call_assigns_t2_assigns_normal : Unsuccess
+[wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_exit : Unsuccess
+[wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_normal : Unsuccess
 [wp] Proved goals:    0 / 6
-  Alt-Ergo:        0  (unknown: 6)
+  Alt-Ergo:        0  (unsuccess: 6)
 [wp] Report 'tests/wp_acsl/assigns_range.i.1.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success

src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle

@@ -4,7 +4,7 @@
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 10 goals scheduled
-[wp] [Alt-Ergo] Goal typed_f_ensures_P_todo : Unknown
+[wp] [Alt-Ergo] Goal typed_f_ensures_P_todo : Unsuccess
 [wp] [Alt-Ergo] Goal typed_f_ensures_Q : Valid
 [wp] [Alt-Ergo] Goal typed_f_loop_invariant_Index_preserved : Valid
 [wp] [Alt-Ergo] Goal typed_f_loop_invariant_Index_established : Valid
@@ -13,10 +13,10 @@
 [wp] [Qed] Goal typed_f_loop_assigns_part1 : Valid
 [wp] [Qed] Goal typed_f_loop_assigns_part2 : Valid
 [wp] [Alt-Ergo] Goal typed_f_loop_assigns_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_f_assigns : Unknown
+[wp] [Alt-Ergo] Goal typed_f_assigns : Unsuccess
 [wp] Proved goals:    8 / 10
   Qed:             3 
-  Alt-Ergo:        5  (unknown: 2)
+  Alt-Ergo:        5  (unsuccess: 2)
 [wp] Report 'tests/wp_acsl/axioms.i.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success

src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle

@@ -12,7 +12,7 @@
 [wp] [Qed] Goal typed_band_bit2_ensures_band4 : Valid
 [wp] [Qed] Goal typed_band_bit3_ensures_band5 : Valid
 [wp] [Qed] Goal typed_band_bit4_ensures_band6 : Valid
-[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Unknown
+[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Unsuccess
 [wp] [Qed] Goal typed_band_bool_true_ensures : Valid
 [wp] [Qed] Goal typed_bnot_ensures : Valid
 [wp] [Qed] Goal typed_bor_ensures : Valid
@@ -20,12 +20,12 @@
 [wp] [Qed] Goal typed_bor_bit1_ensures_bor1 : Valid
 [wp] [Qed] Goal typed_bor_bit2_ensures_bor2 : Valid
 [wp] [Qed] Goal typed_bor_bit3_ensures_bor3 : Valid
-[wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Unknown
+[wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Unsuccess
 [wp] [Alt-Ergo] Goal typed_bor_bool_true_ensures : Valid
 [wp] [Qed] Goal typed_bxor_ensures : Valid
 [wp] [Qed] Goal typed_bxor_bit1_ensures : Valid
 [wp] [Qed] Goal typed_bxor_bit2_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Unknown
+[wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Unsuccess
 [wp] [Qed] Goal typed_bxor_bool_true_ensures : Valid
 [wp] [Qed] Goal typed_lshift_ensures : Valid
 [wp] [Qed] Goal typed_lshift_shift1_ensures_lsl1 : Valid
@@ -35,7 +35,7 @@
 [wp] [Qed] Goal typed_rshift_shift1_ensures_lsr1 : Valid
 [wp] Proved goals:   26 / 29
   Qed:            25 
-  Alt-Ergo:        1  (unknown: 3)
+  Alt-Ergo:        1  (unsuccess: 3)
 [wp] Report 'tests/wp_acsl/bitwise.i.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success

src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle

@@ -308,4 +308,4 @@
 Functions           WP     Alt-Ergo        Total   Success
 f                   11     32 (336..384)    43       100%
 -------------------------------------------------------------
-[wp] Logging keys: shell,no-time-info,no-step-info,cnf.
+[wp] Logging keys: success-only,shell,cnf.

src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle

@@ -4,10 +4,10 @@
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_f_ensures_d7_div_0_x_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_f_ensures_m7_mod_0_x_ko : Unknown
+[wp] [Alt-Ergo] Goal typed_f_ensures_d7_div_0_x_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f_ensures_m7_mod_0_x_ko : Unsuccess
 [wp] Proved goals:    0 / 2
-  Alt-Ergo:        0  (unknown: 2)
+  Alt-Ergo:        0  (unsuccess: 2)
 [wp] Report 'tests/wp_acsl/div_mod.i.2.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success

src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle

@@ -6,13 +6,13 @@
   No code nor implicit assigns clause for function main, generating default assigns from the prototype
 [wp] Warning: Missing RTE guards
 [wp] 4 goals scheduled
-[wp] [Alt-Ergo] Goal typed_extra_ensures_KO : Unknown
+[wp] [Alt-Ergo] Goal typed_extra_ensures_KO : Unsuccess
 [wp] [Qed] Goal typed_foreign_ensures_OK : Valid
 [wp] [Alt-Ergo] Goal typed_job_ensures_OK : Valid
 [wp] [Qed] Goal typed_main_requires_OK : Valid
 [wp] Proved goals:    3 / 4
   Qed:             2 
-  Alt-Ergo:        1  (unknown: 1)
+  Alt-Ergo:        1  (unsuccess: 1)
 [wp] Report 'tests/wp_acsl/init_label.i.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success

src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle

@@ -4,26 +4,26 @@
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 18 goals scheduled
-[wp] [Alt-Ergo] Goal typed_fa1_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_fa1_ensures_qed_ko_2 : Unknown
-[wp] [Alt-Ergo] Goal typed_fa2_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_fa2_ensures_qed_ko_2 : Unknown
-[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko_2 : Unknown
-[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko_3 : Unknown
-[wp] [Alt-Ergo] Goal typed_fs1_ensures_qed_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_fs1_ensures_qed_ko_2 : Unknown
-[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_eq_ko : Unknown
-[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_t : Unknown
-[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_c_2 : Unknown
-[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Tab_no_init : Unknown
-[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_With_Array_Struct_3 : Unknown
-[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Simple_Array_1 : Unknown
-[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_T1_6 : Unknown
-[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_indirect_init_union_b : Unknown
-[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_indirect_init_union_t : Unknown
+[wp] [Alt-Ergo] Goal typed_fa1_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fa1_ensures_qed_ko_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fa2_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fa2_ensures_qed_ko_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fa3_ensures_qed_ko_3 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fs1_ensures_qed_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fs1_ensures_qed_ko_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_eq_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_t : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Sc_c_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Tab_no_init : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_With_Array_Struct_3 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_Simple_Array_1 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_T1_6 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_indirect_init_union_b : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_indirect_init_union_t : Unsuccess
 [wp] Proved goals:    0 / 18
-  Alt-Ergo:        0  (unknown: 18)
+  Alt-Ergo:        0  (unsuccess: 18)
 [wp] Report 'tests/wp_acsl/init_value.i.1.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success

src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle

@@ -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