From fa041e2e482fca829240bb2f03b137df85fc33c2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 11 Jul 2022 20:52:21 +0200
Subject: [PATCH] [wp] updated oracles
---
src/plugins/wp/Stats.ml | 8 ++--
src/plugins/wp/register.ml | 8 ++--
.../initialized_memvar.res.oracle | 24 +++++-----
.../binary-multiplication.res.oracle | 2 +-
.../oracle_qualif/bsearch.res.oracle | 14 +++---
.../oracle_qualif/euclid.res.oracle | 10 ++--
.../oracle_qualif/bitmask0x8000.res.oracle | 4 +-
.../wp_plugin/oracle_qualif/doomed.res.oracle | 10 ++--
.../oracle_qualif/doomed_axioms.res.oracle | 6 +--
.../oracle_qualif/doomed_call.1.res.oracle | 47 +++++++++----------
.../oracle_qualif/doomed_call.2.res.oracle | 47 +++++++++----------
.../oracle_qualif/doomed_dead.0.res.oracle | 46 +++++++++---------
.../oracle_qualif/doomed_dead.1.res.oracle | 46 +++++++++---------
.../oracle_qualif/doomed_localinit.res.oracle | 4 +-
.../oracle_qualif/doomed_loop.res.oracle | 6 +--
.../oracle_qualif/doomed_pre.res.oracle | 27 +++++------
.../oracle_qualif/doomed_report_ko.res.oracle | 6 +--
.../oracle_qualif/doomed_report_ok.res.oracle | 6 +--
.../oracle_qualif/doomed_unreach.res.oracle | 6 +--
.../oracle_qualif/doomed_unroll.res.oracle | 6 +--
.../wp_plugin/oracle_qualif/unroll.res.oracle | 2 +-
.../wp/tests/wp_tip/oracle/clear.res.oracle | 2 -
.../wp_tip/oracle/induction_typing.res.oracle | 1 -
.../tests/wp_tip/oracle/modmask.0.res.oracle | 6 +--
.../tests/wp_tip/oracle/modmask.1.res.oracle | 6 +--
.../wp/tests/wp_tip/oracle/split.res.oracle | 29 +++---------
.../oracle_qualif/induction.0.res.oracle | 2 +-
.../wp_tip/oracle_qualif/overflow.res.oracle | 4 +-
.../wp_tip/oracle_qualif/unroll.res.oracle | 6 +--
.../oracle_qualif/user_init.1.res.oracle | 24 +++++-----
30 files changed, 192 insertions(+), 223 deletions(-)
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index cd724a5c7eb..d1ac1c97502 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -152,13 +152,13 @@ let results ~smoke prs =
else
let cached = List.fold_left
(fun c (_,r) -> if r.VCS.cached then succ c else c)
- 0 doomed in
+ 0 passed in
let stucked = List.map
(fun (p,r) -> p, ptime r.prover_time true)
- doomed in
+ passed in
let solver = List.fold_left
(fun t (_,r) -> t +. r.solver_time)
- 0.0 doomed in
+ 0.0 passed in
let provers = pmerge [Qed,ptime solver false] stucked in
let verdict =
if missing <> [] then NoResult else
@@ -166,7 +166,7 @@ let results ~smoke prs =
| [] -> NoResult
| u::w -> (snd @@ List.fold_left choose_worst u w).verdict in
let proved = List.length passed in
- let failed = List.length missing + List.length doomed in
+ let failed = List.length missing in
{ empty with verdict ; provers ; cached ; proved ; failed }
let add a b =
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index bdd6e296559..6eb4c7af7ce 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -330,14 +330,14 @@ let do_wpo_success ~shell ~updating goal success =
else
let smoke = Wpo.is_smoke_test goal in
let stats = ProofEngine.consolidated goal in
+ let proof, target = Wpo.get_proof goal in
begin
- if shell || stats.verdict <> Valid then
+ if shell || proof <> `Passed then
do_report_stats ~shell ~updating goal ~smoke stats ;
- if smoke && stats.verdict <> Valid then
+ if smoke && proof <> `Passed then
begin
- let target = Wpo.get_target goal in
let source = fst (Property.location target) in
- Wp_parameters.warning ~source "Failed smoke-test"
+ Wp_parameters.warning ~once:true ~source "Failed smoke-test"
end ;
end
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
index 396c8780705..483eeffddd0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
@@ -6,17 +6,17 @@
[wp] [Valid] typed_globals_check_qed_ok (Qed)
[wp] [Valid] typed_globals_check_qed_ok_2 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_3 (Qed)
-[wp] [Unknown] typed_globals_check_qed_ko (Alt-Ergo)
+[wp] [Unknown] typed_globals_check_qed_ko (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_qed_ok_4 (Qed)
-[wp] [Unknown] typed_globals_check_qed_ko_2 (Alt-Ergo)
+[wp] [Unknown] typed_globals_check_qed_ko_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_qed_ok_5 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_6 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_7 (Qed)
[wp] [Valid] typed_globals_check_provable (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_2 (Alt-Ergo) (Cached)
-[wp] [Unknown] typed_globals_check_not_provable (Alt-Ergo)
+[wp] [Unknown] typed_globals_check_not_provable (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_3 (Alt-Ergo) (Cached)
-[wp] [Unknown] typed_globals_check_qed_ko_3 (Alt-Ergo)
+[wp] [Unknown] typed_globals_check_qed_ko_3 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_qed_ok_8 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_9 (Qed)
[wp] [Valid] typed_globals_check_qed_ok_10 (Qed)
@@ -27,13 +27,13 @@
[wp] [Valid] typed_globals_check_provable_5 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_6 (Alt-Ergo) (Cached)
[wp] [Valid] typed_globals_check_provable_7 (Alt-Ergo) (Cached)
-[wp] [Unknown] typed_globals_check_qed_ko_4 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_qed_ko_5 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_qed_ko_6 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_qed_ko_7 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_not_provable_2 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_not_provable_3 (Alt-Ergo)
-[wp] [Unknown] typed_globals_check_not_provable_4 (Alt-Ergo)
+[wp] [Unknown] typed_globals_check_qed_ko_4 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_qed_ko_5 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_qed_ko_6 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_qed_ko_7 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_not_provable_2 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_not_provable_3 (Alt-Ergo) (Cached)
+[wp] [Unknown] typed_globals_check_not_provable_4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_locals_check_qed_ok (Qed)
[wp] [Valid] typed_locals_check_qed_ok_2 (Qed)
[wp] [Valid] typed_locals_check_qed_ok_3 (Qed)
@@ -75,7 +75,7 @@
[wp] [Valid] typed_complex_struct_check_qed_ok_16 (Qed)
[wp] [Valid] typed_complex_struct_check_qed_ok_17 (Qed)
[wp] [Valid] typed_complex_struct_check_qed_ok_18 (Qed)
-[wp] [Valid] typed_complex_struct_check_provable (Script)
+[wp] [Valid] typed_complex_struct_check_provable (Script) (Qed 2/2)
[wp] Proved goals: 62 / 73
Qed: 52
Script: 1
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
index 03a05ff6f73..810a70de3c6 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
@@ -19,7 +19,7 @@
[wp] [Valid] typed_BinaryMultiplication_loop_assigns (Qed)
[wp] [Valid] typed_BinaryMultiplication_loop_variant_decrease (Alt-Ergo) (Cached)
[wp] [Valid] typed_BinaryMultiplication_loop_variant_positive (Qed)
-[wp] [Valid] typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved (Script)
+[wp] [Valid] typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved (Script 4) (Qed 1/10) (Alt-Ergo 9/10) (Cached)
[wp] Proved goals: 17 / 17
Qed: 4
Script: 1
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
index 14a3c030932..8151ffdaf4f 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
@@ -3,13 +3,13 @@
[wp] Running WP plugin...
[rte:annot] annotating function binary_search
[wp] 28 goals scheduled
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_loop_s3 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s8 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s17 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_binary_search_wp_smoke_dead_code_s18 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_loop_s3 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s8 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s17 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_binary_search_wp_smoke_dead_code_s18 (Alt-Ergo) (Cached)
[wp] [Valid] typed_binary_search_ensures_Result (Alt-Ergo) (Cached)
[wp] [Valid] typed_binary_search_ensures_Found (Qed)
[wp] [Valid] typed_binary_search_ensures_NotFound (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
index 82d93e86a62..41392f11994 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[rte:annot] annotating function euclid_gcd
[wp] 16 goals scheduled
-[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s6 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s6 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_euclid_euclid_gcd_wp_smoke_dead_code_s12 (Alt-Ergo) (Cached)
[wp] [Valid] typed_euclid_euclid_gcd_ensures (Alt-Ergo) (Cached)
[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_established (Qed)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle
index 6840a885209..dec011b7676 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.res.oracle
@@ -2,8 +2,8 @@
[kernel] Parsing bitmask0x8000.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
-[wp] [Valid] typed_lemma_res_n (Script)
-[wp] [Valid] typed_lemma_res_y (Script)
+[wp] [Valid] typed_lemma_res_n (Script) (Qed 1/2) (Alt-Ergo 1/2) (Cached)
+[wp] [Valid] typed_lemma_res_y (Script) (Qed 1/2) (Alt-Ergo 1/2) (Cached)
[wp] Proved goals: 2 / 2
Qed: 0
Script: 2
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
index 33b379e24f6..2dba4628c01 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed.res.oracle
@@ -3,13 +3,13 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 7 goals scheduled
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_A_requires (Qed)
+[wp] [Passed (Timeout)] typed_foo_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_A_requires (Qed)
[wp] doomed.i:27: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_B_requires (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_bar_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_foo_wp_smoke_B_requires (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_bar_wp_smoke_default_requires (Alt-Ergo) (Cached)
[wp] [Valid] typed_bar_ensures (Qed)
-[wp] [Passed (Invalid)] typed_buzz_wp_smoke_default_requires (Qed)
+[wp] [Failed (Doomed)] typed_buzz_wp_smoke_default_requires (Qed)
[wp] doomed.i:41: Warning: Failed smoke-test
[wp] [Valid] typed_buzz_ensures (Qed)
[wp] Proved goals: 5 / 7
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
index 114b97fe7db..f42a17c0ef3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_axioms.res.oracle
@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
[wp] doomed_axioms.i:29: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] doomed_axioms.i:30: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] doomed_axioms.i:32: Warning: Failed smoke-test
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
index 8876b4535d6..5968d7b5785 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.1.res.oracle
@@ -3,43 +3,42 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 33 goals scheduled
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_ensures (Qed)
[wp] [Valid] typed_f1_ok_exits (Qed)
-[wp] [Failed (Doomed)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_ensures (Qed)
[wp] [Valid] typed_f2_ok_exits (Qed)
-[wp] [Passed (Invalid)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
+[wp] [Failed (Doomed)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
[wp] doomed_call.i:68: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
+[wp] [Failed (Doomed)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
[wp] doomed_call.i:69: Warning: Failed smoke-test
[wp] [Valid] typed_f3_ko_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_ensures (Qed)
-[wp] [Passed (Invalid)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
+[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
[wp] doomed_call.i:89: Warning: Failed smoke-test
[wp] [Valid] typed_f4_ko_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
-[wp] doomed_call.i:121: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
+[wp] [Passed (Unknown)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
[wp] doomed_call.i:121: Warning: Failed smoke-test
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
[wp] [Valid] typed_f5_ko_ensures (Qed)
[wp] Proved goals: 28 / 33
Qed: 10 (failed: 5)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
index 4b8fcaef2ef..6d8460a9afb 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_call.2.res.oracle
@@ -3,46 +3,45 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 36 goals scheduled
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s2 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s2 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_ensures_part1 (Qed)
[wp] [Valid] typed_f1_ok_ensures_part2 (Qed)
[wp] [Valid] typed_f1_ok_exits (Qed)
-[wp] [Failed (Doomed)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_post_ok_wp_smoke_dead_call_s9 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s11 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_ensures_part1 (Qed)
[wp] [Valid] typed_f2_ok_ensures_part2 (Qed)
[wp] [Valid] typed_f2_ok_exits_part1 (Qed)
[wp] [Valid] typed_f2_ok_exits_part2 (Qed)
-[wp] [Passed (Invalid)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
+[wp] [Failed (Doomed)] typed_call_ko_wp_smoke_dead_call_s14 (Qed)
[wp] doomed_call.i:68: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
+[wp] [Failed (Doomed)] typed_f3_ko_wp_smoke_dead_code_s15 (Qed)
[wp] doomed_call.i:69: Warning: Failed smoke-test
[wp] [Valid] typed_f3_ko_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_exit_ok_wp_smoke_dead_call_s18 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_ko_global_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_ensures (Qed)
-[wp] [Passed (Invalid)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
+[wp] [Failed (Doomed)] typed_call_ko_global_wp_smoke_dead_call_s26 (Qed)
[wp] doomed_call.i:89: Warning: Failed smoke-test
[wp] [Valid] typed_f4_ko_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s29 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_ensures (Qed)
-[wp] [Failed (Doomed)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
-[wp] doomed_call.i:121: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
+[wp] [Passed (Unknown)] typed_call_wrong_wp_smoke_dead_call_s35 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_call_effect_wp_smoke_dead_call_s34 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_call_effect_wp_smoke_dead_call_s36 (Qed)
[wp] doomed_call.i:121: Warning: Failed smoke-test
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s36 (Qed)
[wp] [Valid] typed_f5_ko_ensures (Qed)
[wp] Proved goals: 31 / 36
Qed: 13 (failed: 5)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
index 4f879169d52..b04f6240163 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.0.res.oracle
@@ -3,50 +3,50 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 46 goals scheduled
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f1_ok_assigns_part2 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_assigns_exit (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part2 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
[wp] doomed_dead.i:44: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ko_assigns_exit (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part2 (Qed)
-[wp] [Failed (Doomed)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_assigns_exit (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part2 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_assert (Qed)
[wp] [Valid] typed_f4_ok_assigns_exit (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part2 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part3 (Qed)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part3 (Qed)
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
[wp] doomed_dead.i:90: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ko_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part3 (Qed)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
index 2440cab302c..09fda7dac28 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_dead.1.res.oracle
@@ -3,52 +3,52 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 48 goals scheduled
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f1_ok_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f1_ok_wp_smoke_dead_code_s10 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f1_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f1_ok_assigns_part2 (Qed)
[wp] [Valid] typed_f1_ok_assigns_part3 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s14 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s14 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ok_wp_smoke_dead_code_s16 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ok_assigns_exit (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part2 (Qed)
[wp] [Valid] typed_f2_ok_assigns_normal_part3 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s22 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s22 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s23 (Qed)
[wp] doomed_dead.i:44: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f2_ko_wp_smoke_dead_code_s26 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f2_ko_assigns_exit (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f2_ko_assigns_normal_part2 (Qed)
-[wp] [Failed (Doomed)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_call_wp_smoke_dead_call_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s30 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f3_ok_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f3_ok_wp_smoke_dead_code_s34 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f3_ok_assigns_exit (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f3_ok_assigns_normal_part2 (Qed)
-[wp] [Failed (Doomed)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_exit_wp_smoke_dead_call_s38 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f4_ok_wp_smoke_dead_code_s41 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f4_ok_assert (Qed)
[wp] [Valid] typed_f4_ok_assigns_exit (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part1 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part2 (Qed)
[wp] [Valid] typed_f4_ok_assigns_normal_part3 (Qed)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s48 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ok_wp_smoke_dead_code_s50 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ok_wp_smoke_dead_code_s52 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ok_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ok_assigns_part3 (Qed)
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s56 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s61 (Qed)
[wp] doomed_dead.i:90: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_f5_ko_wp_smoke_dead_code_s63 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_f5_ko_wp_smoke_dead_code_s65 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f5_ko_assigns_part1 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part2 (Qed)
[wp] [Valid] typed_f5_ko_assigns_part3 (Qed)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle
index 2556b38935c..057f17ce243 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_localinit.res.oracle
@@ -3,8 +3,8 @@
[wp] Running WP plugin...
[rte:annot] annotating function access
[wp] 4 goals scheduled
-[wp] [Failed (Doomed)] typed_access_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_access_wp_smoke_dead_code_s5 (Qed)
+[wp] [Passed (Unknown)] typed_access_wp_smoke_dead_code_s3 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_access_wp_smoke_dead_code_s5 (Qed)
[wp] doomed_localinit.i:11: Warning: Failed smoke-test
[wp] [Timeout] typed_access_assert_rte_mem_access (Alt-Ergo) (Cached)
[wp] [Timeout] typed_access_assert_rte_mem_access_2 (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
index 0cecf94944c..bd83f9550eb 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_loop.res.oracle
@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_loop_s2 (Qed)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Qed)
[wp] doomed_loop.i:22: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s7 (Qed)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Qed)
[wp] doomed_loop.i:23: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s9 (Qed)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Qed)
[wp] doomed_loop.i:25: Warning: Failed smoke-test
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Qed)
[wp] [Unknown] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
index 1f8c5660894..d568292aa0e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_pre.res.oracle
@@ -3,27 +3,26 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 13 goals scheduled
-[wp] [Passed (Invalid)] typed_requires_wp_smoke_default_requires (Qed)
+[wp] [Failed (Doomed)] typed_requires_wp_smoke_default_requires (Qed)
[wp] doomed_pre.i:10: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_reqs_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_reqs_assumes_wp_smoke_B_assumes (Qed)
+[wp] [Passed (Timeout)] typed_reqs_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_reqs_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:16: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_reqs_2_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_reqs_2_2_assumes_wp_smoke_B_assumes (Qed)
+[wp] [Passed (Timeout)] typed_reqs_2_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_reqs_2_2_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:23: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_reqs_1_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_reqs_1_2_assumes_wp_smoke_B_assumes (Qed)
+[wp] [Passed (Timeout)] typed_reqs_1_2_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_reqs_1_2_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:30: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_reqs_combined_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_reqs_combined_assumes_wp_smoke_B_assumes (Qed)
+[wp] [Passed (Unknown)] typed_reqs_combined_assumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_reqs_combined_assumes_wp_smoke_B_assumes (Qed)
[wp] doomed_pre.i:37: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_bhv_requires_assumes_wp_smoke_B_requires (Qed)
+[wp] [Failed (Doomed)] typed_bhv_requires_assumes_wp_smoke_B_requires (Qed)
[wp] doomed_pre.i:48: Warning: Failed smoke-test
-[wp] [Failed (Doomed)] typed_reqs_massumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
-[wp] [Passed (Invalid)] typed_reqs_massumes_wp_smoke_B1_assumes (Qed)
-[wp] doomed_pre.i:56: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_reqs_massumes_wp_smoke_B2_assumes (Qed)
+[wp] [Passed (Timeout)] typed_reqs_massumes_wp_smoke_default_requires (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_reqs_massumes_wp_smoke_B1_assumes (Qed)
[wp] doomed_pre.i:56: Warning: Failed smoke-test
+[wp] [Failed (Doomed)] typed_reqs_massumes_wp_smoke_B2_assumes (Qed)
[wp] Proved goals: 5 / 13
Qed: 0 (failed: 8)
Alt-Ergo: 5
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
index c8694f081d6..4b67d9a83d0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ko.res.oracle
@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
[wp] doomed_report_ko.i:29: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
[wp] doomed_report_ko.i:29: Warning: Failed smoke-test
-[wp] [Passed (Invalid)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
+[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] doomed_report_ko.i:30: Warning: Failed smoke-test
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
index 1a708a992ad..10bb9690dc0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_report_ok.res.oracle
@@ -3,9 +3,9 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_foo_wp_smoke_dead_loop_s2 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_foo_wp_smoke_dead_code_s7 (Alt-Ergo) (Cached)
+[wp] [Passed (Timeout)] typed_foo_wp_smoke_dead_code_s9 (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_A_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_A_established (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_B_preserved (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
index 3264f7d6554..f08449c5713 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unreach.res.oracle
@@ -6,9 +6,9 @@
[wp] doomed_unreach.i:22: Warning: Failed smoke-test
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
-[wp] [Failed (Doomed)] typed_job_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_job_wp_smoke_dead_code_s5 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_job_wp_smoke_dead_code_s8 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_job_wp_smoke_dead_code_s4 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_job_wp_smoke_dead_code_s5 (Alt-Ergo) (Cached)
+[wp] [Passed (Stepout)] typed_job_wp_smoke_dead_code_s8 (Alt-Ergo) (Cached)
[wp] [Valid] typed_job_assigns_part1 (Qed)
[wp] [Valid] typed_job_assigns_part2 (Qed)
[wp] [Valid] typed_job_assigns_part3 (Qed)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
index 44f4519c1fc..7b37e132c51 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/doomed_unroll.res.oracle
@@ -5,9 +5,9 @@
[wp] doomed_unroll.i:15: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 5 goals scheduled
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s27 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
-[wp] [Failed (Doomed)] typed_foo_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_foo_wp_smoke_dead_code_s27 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_foo_wp_smoke_dead_code_s31 (Alt-Ergo) (Cached)
+[wp] [Passed (Unknown)] typed_foo_wp_smoke_dead_code_s35 (Alt-Ergo) (Cached)
[wp] [Valid] typed_foo_loop_invariant_preserved (Qed)
[wp] [Valid] typed_foo_loop_invariant_established (Qed)
[wp] Proved goals: 5 / 5
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
index 03e42c0b78e..1d90715d28d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.res.oracle
@@ -4,7 +4,7 @@
[wp] Warning: Missing RTE guards
[wp] unroll.i:21: Warning: Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
-[wp] [Valid] typed_unrolled_loop_ensures_zero (Script)
+[wp] [Valid] typed_unrolled_loop_ensures_zero (Script 2) (Qed 18/18)
[wp] Proved goals: 1 / 1
Qed: 0
Script: 1
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
index def71a156f5..4418f56a90d 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -105,7 +105,6 @@
Prove: P_S(42).
------------------------------------------------------------
-[wp] [Unknown] typed_clear_in_step_check (Script)
[wp:script:allgoals]
typed_clear_ensures subgoal:
@@ -143,5 +142,4 @@
Prove: P_S(a + b).
------------------------------------------------------------
-[wp] [Unknown] typed_clear_ensures (Script)
[wp] Proved goals: 0 / 2
diff --git a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
index d56e54307ac..544ecdb4041 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
@@ -54,7 +54,6 @@
Prove: false.
------------------------------------------------------------
-[wp] [Unknown] typed_function_loop_invariant_X_preserved (Script)
[wp:script:allgoals]
typed_function_loop_invariant_X_preserved subgoal:
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
index 7db5771084a..9730b99da41 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
@@ -14,7 +14,6 @@
Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_us_255 (Script)
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
@@ -56,7 +55,4 @@
Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_u (Script)
-[wp] Proved goals: 2 / 2
- Qed: 0
- Script: 2
+[wp] Proved goals: 0 / 2
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
index 7db5771084a..9730b99da41 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
@@ -14,7 +14,6 @@
Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_us_255 (Script)
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
@@ -56,7 +55,4 @@
Prove: exists i : Z. (lsl(1, i) = lsl(1, shift_0)) /\ (0 <= i).
------------------------------------------------------------
-[wp] [Valid] typed_check_lemma_and_modulo_u (Script)
-[wp] Proved goals: 2 / 2
- Qed: 0
- Script: 2
+[wp] Proved goals: 0 / 2
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
index 9d27fa46879..6fb2156c63f 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
@@ -201,7 +201,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_branch_ensures (Script)
[wp:script:allgoals]
typed_test_step_branch_ensures subgoal:
@@ -224,7 +223,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_or_ensures (Script)
[wp:script:allgoals]
typed_test_step_or_ensures subgoal:
@@ -256,7 +254,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_and_ensures (Script)
[wp:script:allgoals]
typed_test_step_peq_ensures subgoal:
@@ -265,7 +262,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_peq_ensures (Script)
[wp:script:allgoals]
typed_test_step_peq_ensures subgoal:
@@ -282,7 +278,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_pneq_ensures (Script)
[wp:script:allgoals]
typed_test_step_pneq_ensures subgoal:
@@ -299,7 +294,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_neq_ensures (Script)
+[wp] [Unknown] typed_test_step_neq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_neq_ensures subgoal:
@@ -324,7 +319,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_leq_ensures (Script)
+[wp] [Unknown] typed_test_step_leq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_leq_ensures subgoal:
@@ -354,7 +349,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_lt_ensures (Script)
+[wp] [Unknown] typed_test_step_lt_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_step_lt_ensures subgoal:
@@ -379,7 +374,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_if_ensures (Script)
[wp:script:allgoals]
typed_test_step_if_ensures subgoal:
@@ -405,7 +399,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_fa_if_ensures (Script)
[wp:script:allgoals]
typed_test_step_fa_if_ensures subgoal:
@@ -427,7 +420,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_fa_or_ensures (Script)
[wp:script:allgoals]
typed_test_step_fa_or_ensures subgoal:
@@ -448,7 +440,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unknown] typed_test_step_fa_and_ensures (Script)
[wp:script:allgoals]
typed_test_inside_leq_ensures subgoal:
@@ -463,7 +454,7 @@
Prove: P_Q.
------------------------------------------------------------
-[wp] [Unknown] typed_test_inside_leq_ensures (Script)
+[wp] [Unknown] typed_test_inside_leq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_inside_leq_ensures subgoal:
@@ -494,7 +485,7 @@
Prove: P_Q.
------------------------------------------------------------
-[wp] [Unknown] typed_test_inside_lt_ensures (Script)
+[wp] [Unknown] typed_test_inside_lt_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_inside_lt_ensures subgoal:
@@ -525,7 +516,7 @@
Prove: P_Q.
------------------------------------------------------------
-[wp] [Unknown] typed_test_inside_neq_ensures (Script)
+[wp] [Unknown] typed_test_inside_neq_ensures (Tactic) (Qed)
[wp:script:allgoals]
typed_test_inside_neq_ensures subgoal:
@@ -556,7 +547,6 @@
Prove: P_P.
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_and_ensures (Script)
[wp:script:allgoals]
typed_test_goal_and_ensures subgoal:
@@ -581,7 +571,6 @@
Prove: (L_LP=true).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_eq_ensures (Script)
[wp:script:allgoals]
typed_test_goal_eq_ensures subgoal:
@@ -598,7 +587,6 @@
Prove: (L_LP=false).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_neq_ensures (Script)
[wp:script:allgoals]
typed_test_goal_neq_ensures subgoal:
@@ -620,7 +608,6 @@
Prove: P_P.
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_if_ensures (Script)
[wp:script:allgoals]
typed_test_goal_if_ensures subgoal:
@@ -642,7 +629,6 @@
Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_ex_and_ensures (Script)
[wp:script:allgoals]
typed_test_goal_ex_and_ensures subgoal:
@@ -659,7 +645,6 @@
Prove: P_P \/ P_Q \/ (exists i : Z. P_Pi(i)) \/ (exists i : Z. P_Qi(i)).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_ex_or_ensures (Script)
[wp:script:allgoals]
typed_test_goal_ex_if_ensures subgoal:
@@ -674,7 +659,6 @@
Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_ex_if_ensures (Script)
[wp:script:allgoals]
typed_test_goal_ex_if_ensures subgoal:
@@ -702,5 +686,4 @@
Prove: exists i : Z. P_Qi(i).
------------------------------------------------------------
-[wp] [Unknown] typed_test_goal_ex_imply_ensures (Script)
[wp] Proved goals: 0 / 23
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
index 4d3c4e24423..efa47216f89 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing induction.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] [Valid] typed_lemma_ByInd (Script)
+[wp] [Valid] typed_lemma_ByInd (Script) (Alt-Ergo 3/3) (Cached)
[wp] Proved goals: 1 / 1
Qed: 0
Script: 1
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle
index 7cd2f2e1245..e85db6d3a63 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.res.oracle
@@ -2,8 +2,8 @@
[kernel] Parsing overflow.i (no preprocessing)
[wp] Running WP plugin...
[wp] 2 goals scheduled
-[wp] [Valid] typed_lemma_j_incr_char (Script)
-[wp] [Valid] typed_lemma_j_incr_short (Script)
+[wp] [Valid] typed_lemma_j_incr_char (Script) (Qed 1/3) (Alt-Ergo 2/3) (Cached)
+[wp] [Valid] typed_lemma_j_incr_short (Script) (Qed 1/3) (Alt-Ergo 2/3) (Cached)
[wp] Proved goals: 2 / 2
Qed: 0
Script: 2
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle
index a515c1fc7f8..7d03fba0ca5 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle
@@ -2,9 +2,9 @@
[kernel] Parsing unroll.i (no preprocessing)
[wp] Running WP plugin...
[wp] 3 goals scheduled
-[wp] [Valid] typed_lemma_LEFT (Script)
-[wp] [Valid] typed_lemma_RIGHT (Script)
-[wp] [Valid] typed_lemma_SUM (Script)
+[wp] [Valid] typed_lemma_LEFT (Script) (Qed 2/2)
+[wp] [Valid] typed_lemma_RIGHT (Script) (Qed 2/2)
+[wp] [Valid] typed_lemma_SUM (Script) (Qed 2/2)
[wp] Proved goals: 3 / 3
Qed: 0
Script: 3
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
index e67a634d8b1..4b470149e63 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
@@ -4,28 +4,28 @@
[wp] Warning: Missing RTE guards
[wp] 23 goals scheduled
[wp] [Valid] typed_init_t2_v2_loop_assigns_part1 (Qed)
-[wp] [Valid] typed_init_t2_v2_loop_assigns_part2 (Script)
-[wp] [Valid] typed_init_t2_v2_loop_assigns_part3 (Script)
+[wp] [Valid] typed_init_t2_v2_loop_assigns_part2 (Script) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_v2_loop_assigns_part3 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_v2_loop_assigns_2_part1 (Qed)
-[wp] [Valid] typed_init_t2_v2_loop_assigns_2_part2 (Script)
-[wp] [Valid] typed_init_t2_v2_loop_assigns_2_part3 (Script)
+[wp] [Valid] typed_init_t2_v2_loop_assigns_2_part2 (Script) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_v2_loop_assigns_2_part3 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_v2_assigns_part1 (Qed)
-[wp] [Valid] typed_init_t2_v2_assigns_part2 (Script)
+[wp] [Valid] typed_init_t2_v2_assigns_part2 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_v3_loop_assigns_part1 (Qed)
-[wp] [Valid] typed_init_t2_v3_loop_assigns_part2 (Script)
-[wp] [Valid] typed_init_t2_v3_loop_assigns_part3 (Script)
+[wp] [Valid] typed_init_t2_v3_loop_assigns_part2 (Script) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_v3_loop_assigns_part3 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_v3_loop_assigns_2_part1 (Qed)
[wp] [Valid] typed_init_t2_v3_loop_assigns_2_part2 (Qed)
[wp] [Valid] typed_init_t2_v3_assigns_part1 (Qed)
-[wp] [Valid] typed_init_t2_v3_assigns_part2 (Script)
+[wp] [Valid] typed_init_t2_v3_assigns_part2 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part1 (Qed)
-[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part2 (Script)
-[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part3 (Script)
+[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part2 (Script) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part3 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part1 (Qed)
-[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part2 (Script)
+[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part2 (Script) (Alt-Ergo 2/2) (Cached)
[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part3 (Qed)
[wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part1 (Qed)
-[wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part2 (Script)
+[wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part2 (Script) (Alt-Ergo 2/2) (Cached)
[wp] Proved goals: 23 / 23
Qed: 11
Script: 12
--
GitLab