From bff858cb400f7708478f22a062bd748e786585c0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 20 Jul 2022 14:00:11 +0200
Subject: [PATCH] [wp] refine cache statistics
---
src/plugins/wp/Cache.ml | 7 +-
src/plugins/wp/Cache.mli | 3 +-
src/plugins/wp/Stats.ml | 82 +++++++++++--------
src/plugins/wp/Stats.mli | 29 ++++---
src/plugins/wp/VCS.ml | 2 +-
src/plugins/wp/VCS.mli | 1 +
src/plugins/wp/register.ml | 21 +++--
.../wp_acsl/oracle_qualif/arith.0.res.oracle | 2 +-
.../oracle_qualif/div_mod.0.res.oracle | 22 ++---
.../oracle_qualif/div_mod.1.res.oracle | 22 ++---
.../wp_acsl/oracle_qualif/e_imply.res.oracle | 68 +++++++--------
.../wp_acsl/oracle_qualif/sizeof.res.oracle | 2 +-
.../wp_bts/oracle_qualif/bts0843.res.oracle | 4 +-
.../wp_bts/oracle_qualif/issue_447.res.oracle | 2 +-
.../wp_typed/oracle_qualif/mvar.res.oracle | 2 +-
15 files changed, 147 insertions(+), 122 deletions(-)
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index 9ecfc2f038f..efa8e17c58c 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -136,8 +136,11 @@ module MODE = WpContext.StaticGenerator(Datatype.Unit)
let get_mode = MODE.get
let set_mode m = MODE.clear () ; Wp_parameters.Cache.set (mode_name m)
-let is_updating () =
- match MODE.get () with
+let is_active = function
+ | NoCache -> false
+ | Replay | Offline | Update | Rebuild | Cleanup -> true
+
+let is_updating = function
| NoCache | Replay | Offline -> false
| Update | Rebuild | Cleanup -> true
diff --git a/src/plugins/wp/Cache.mli b/src/plugins/wp/Cache.mli
index b1bfe4c451c..61665faceda 100644
--- a/src/plugins/wp/Cache.mli
+++ b/src/plugins/wp/Cache.mli
@@ -30,7 +30,8 @@ val get_hits : unit -> int
val get_miss : unit -> int
val get_removed : unit -> int
-val is_updating : unit -> bool
+val is_active : mode -> bool
+val is_updating : mode -> bool
val cleanup_cache : unit -> unit
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index ff81afab526..eeeb9c95e4c 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -40,6 +40,7 @@ type stats = {
provers : (VCS.prover * pstats) list ;
tactics : int ;
proved : int ;
+ trivial : int ;
timeout : int ;
unknown : int ;
noresult : int ;
@@ -102,6 +103,7 @@ let empty = {
unknown = 0 ;
noresult = 0 ;
failed = 0 ;
+ trivial = 0 ;
cached = 0 ;
}
@@ -112,33 +114,33 @@ let choose_worst a b =
if VCS.leq (snd b) (snd a) then a else b
let consolidated_valid = function
- | [] -> NoResult, 0, []
+ | [] -> NoResult, 0, 0, []
| u::w as results ->
let p,r = List.fold_left choose_best u w in
+ let trivial = p = Qed || VCS.is_trivial r in
let cached =
- p = Qed ||
- if VCS.is_valid r then r.cached else
- List.for_all
- (fun (_,r) -> r.VCS.cached || not (VCS.is_verdict r))
- results in
+ List.for_all
+ (fun (_,r) -> r.VCS.cached || not (VCS.is_verdict r))
+ results in
r.VCS.verdict,
+ (if trivial then 1 else 0),
(if cached then 1 else 0),
if p = Qed then [Qed,pqed r]
else pmerge [Qed,psolver r] [p,presult r]
let valid_stats prs =
- let verdict, cached, provers = consolidated_valid prs in
+ let verdict, trivial, cached, provers = consolidated_valid prs in
match verdict with
| Valid ->
- { empty with verdict ; provers ; cached ; proved = 1 }
+ { empty with verdict ; provers ; trivial ; cached ; proved = 1 }
| Timeout | Stepout ->
- { empty with verdict ; provers ; cached ; timeout = 1 }
+ { empty with verdict ; provers ; trivial ; cached ; timeout = 1 }
| Unknown ->
- { empty with verdict ; provers ; cached ; unknown = 1 }
+ { empty with verdict ; provers ; trivial ; cached ; unknown = 1 }
| NoResult | Computing _ ->
- { empty with verdict ; provers ; cached ; noresult = 1 }
+ { empty with verdict ; provers ; trivial ; cached ; noresult = 1 }
| Failed | Invalid ->
- { empty with verdict ; provers ; cached ; failed = 1 }
+ { empty with verdict ; provers ; trivial ; cached ; failed = 1 }
let results ~smoke prs =
if not smoke then valid_stats prs
@@ -150,6 +152,9 @@ let results ~smoke prs =
if doomed <> [] then
valid_stats doomed
else
+ let trivial = List.fold_left
+ (fun c (p,r) -> if p = Qed || VCS.is_trivial r then succ c else c)
+ 0 passed in
let cached = List.fold_left
(fun c (_,r) -> if r.VCS.cached then succ c else c)
0 passed in
@@ -167,7 +172,7 @@ let results ~smoke prs =
| u::w -> (snd @@ List.fold_left choose_worst u w).verdict in
let proved = List.length passed in
let failed = List.length missing in
- { empty with verdict ; provers ; cached ; proved ; failed }
+ { empty with verdict ; provers ; trivial ; cached ; proved ; failed }
let add a b =
if a == empty then b else
@@ -181,6 +186,7 @@ let add a b =
unknown = a.unknown + b.unknown ;
noresult = a.noresult + b.noresult ;
failed = a.failed + b.failed ;
+ trivial = a.trivial + b.trivial ;
cached = a.cached + b.cached ;
}
@@ -192,7 +198,7 @@ let tactical ~qed children =
List.fold_left add { empty with verdict ; provers ; tactics = 1 } children
let script stats =
- let cached = stats.cached = stats.proved in
+ let cached = (stats.trivial + stats.cached = stats.proved) in
let solver = List.fold_left
(fun t (p,s) -> if p = Qed then t +. s.time else t) 0.0 stats.provers in
let time = List.fold_left
@@ -228,45 +234,53 @@ let pp_pstats fmt p =
Rformat.pp_time mean
Rformat.pp_time p.tmax
-let pp_stats ~shell ~updating fmt s =
- let vp = s.proved in
- let np = proofs s in
+let pp_stats ~shell ~cache fmt s =
+ let total = proofs s in
+ let valids = s.proved in
+ let cached = s.trivial + s.cached in
if s.tactics > 1 then
Format.fprintf fmt " (Tactics %d)" s.tactics
else if s.tactics = 1 then
Format.fprintf fmt " (Tactic)" ;
- let print_cache =
- 0 < s.cached && List.exists (fun (p,_) -> p <> Qed) s.provers in
- let print_perfo =
- not shell || (print_cache && not updating && s.cached < np) in
+ let updating = Cache.is_updating cache in
+ let cache_miss = Cache.is_active cache && not updating && cached < total in
let qed_only =
- match s.provers with [Qed,_] -> vp = np | _ -> false in
+ match s.provers with [Qed,_] -> valids = total | _ -> false in
+ let print_cache =
+ not qed_only && Cache.is_active cache && 0 < cached in
List.iter
(fun (p,pr) ->
let success = truncate pr.success in
- let print_perfo = print_perfo && pr.time > Rformat.epsilon in
- let print_proofs = success > 0 && np > 1 in
- let print_qed = qed_only && s.verdict = Valid && vp = np in
- if p != Qed || print_qed || print_perfo || print_proofs then
+ let print_perfo =
+ pr.time > Rformat.epsilon &&
+ (not shell || cache_miss) in
+ let print_proofs = success > 0 && total > 1 in
+ let print_qed = qed_only && s.verdict = Valid && valids = total in
+ if p != Qed || print_qed || print_perfo || print_proofs
+ then
begin
let title = VCS.title_of_prover ~version:false p in
Format.fprintf fmt " (%s" title ;
if print_proofs then
- Format.fprintf fmt " %d/%d" success np ;
+ Format.fprintf fmt " %d/%d" success total ;
if print_perfo then
Format.fprintf fmt " %a" Rformat.pp_time pr.time ;
Format.fprintf fmt ")"
end
) s.provers ;
+ if shell && cache_miss then
+ Format.fprintf fmt " (Cache miss %d)" (total - cached)
+ else
if print_cache then
- if s.cached = np || updating then
- Format.fprintf fmt " (Cached)"
- else
- if shell then
- Format.fprintf fmt " (Cache miss %d)" (np - s.cached)
+ if s.trivial = total then
+ Format.fprintf fmt " (Trivial)"
else
- Format.fprintf fmt " (Cached %d/%d)" s.cached np
+ let cacheable = total - s.trivial in
+ if updating || s.cached = cacheable then
+ Format.fprintf fmt " (Cached)"
+ else
+ Format.fprintf fmt " (Cached %d/%d)" s.cached cacheable
-let pretty = pp_stats ~shell:false ~updating:false
+let pretty = pp_stats ~shell:false ~cache:NoCache
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Stats.mli b/src/plugins/wp/Stats.mli
index a5b0a21fdc9..3fd10260de6 100644
--- a/src/plugins/wp/Stats.mli
+++ b/src/plugins/wp/Stats.mli
@@ -34,21 +34,28 @@ type pstats = {
success : float ; (** number of success (valid xor smoke) *)
}
-(** Cumulated Stats *)
+(** Cumulated Stats
+
+ Remark: for each sub-goal, only the _best_ prover result is kept *)
type stats = {
- verdict : VCS.verdict ;
- provers : (VCS.prover * pstats) list ;
- tactics : int ;
- proved : int ;
- timeout : int ;
- unknown : int ;
- noresult : int ;
- failed : int ;
- cached : int ;
+ verdict : VCS.verdict ; (** global verdict *)
+ provers : (VCS.prover * pstats) list ; (** meaningfull provers *)
+ tactics : int ; (** number of tactics *)
+ proved : int ; (** number of proved sub-goals *)
+ trivial : int ; (** number of proved sub-goals with Qed or No-prover time *)
+ timeout : int ; (** number of resulting timeouts and stepouts *)
+ unknown : int ; (** number of resulting unknown *)
+ noresult : int ; (** number of no-result *)
+ failed : int ; (** number of resulting failures *)
+ cached : int ; (** number of cached (non-trivial) results *)
}
val pp_pstats : Format.formatter -> pstats -> unit
-val pp_stats : shell:bool -> updating:bool -> Format.formatter -> stats -> unit
+val pp_stats :
+ shell:bool ->
+ cache:Cache.mode ->
+ Format.formatter -> stats -> unit
+
val pretty : Format.formatter -> stats -> unit
val empty : stats
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 966f598859e..fe3442257a4 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -207,8 +207,8 @@ let is_result = function
| NoResult | Computing _ -> false
let is_verdict r = is_result r.verdict
-
let is_valid = function { verdict = Valid } -> true | _ -> false
+let is_trivial r = is_valid r && r.prover_time = 0.0
let is_not_valid r = is_verdict r && not (is_valid r)
let is_computing = function { verdict=Computing _ } -> true | _ -> false
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 2a1ac1be832..1270a6a0724 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -114,6 +114,7 @@ val is_auto : prover -> bool
val is_result : verdict -> bool
val is_verdict : result -> bool
val is_valid: result -> bool
+val is_trivial: result -> bool
val is_not_valid: result -> bool
val is_computing: result -> bool
val is_proved: smoke:bool -> result -> bool
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index e48365f094d..0ab24ee3c0a 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -296,7 +296,7 @@ let do_wpo_result goal prover res =
if VCS.is_verdict res && prover = VCS.Qed then
do_progress goal "Qed"
-let do_report_stats ~shell ~updating ~smoke goal (stats : Stats.stats) =
+let do_report_stats ~shell ~cache ~smoke goal (stats : Stats.stats) =
let status =
if smoke then
match stats.verdict with
@@ -320,10 +320,10 @@ let do_report_stats ~shell ~updating ~smoke goal (stats : Stats.stats) =
| Stepout -> "[Stepout]"
in if status <> "" then
Wp_parameters.feedback "%s %s%a%a"
- status (Wpo.get_gid goal) (Stats.pp_stats ~shell ~updating) stats
+ status (Wpo.get_gid goal) (Stats.pp_stats ~shell ~cache) stats
pp_warnings goal
-let do_wpo_success ~shell ~updating goal success =
+let do_wpo_success ~shell ~cache goal success =
if Wp_parameters.Generate.get () then
match success with
| None -> ()
@@ -340,7 +340,7 @@ let do_wpo_success ~shell ~updating goal success =
if cstats.tactics > 0 then
script_stats := Stats.add !script_stats cstats ;
if shell || proof <> `Passed then
- do_report_stats ~shell ~updating goal ~smoke cstats ;
+ do_report_stats ~shell ~cache goal ~smoke cstats ;
if smoke && proof <> `Passed then
begin
let source = fst (Property.location target) in
@@ -367,9 +367,8 @@ let do_report_scheduled () =
(fun g n ->
if Wpo.is_passed g then succ n else n
) !session (unreachable + terminating) in
- let mode = Cache.get_mode () in
- let updating = Cache.is_updating () in
- if mode <> Cache.NoCache then do_report_cache_usage mode ;
+ let cache = Cache.get_mode () in
+ if Cache.is_active cache then do_report_cache_usage cache ;
let shell = Wp_parameters.has_dkey VCS.dkey_shell in
let lines = ref [] in
let none = fun _fmt -> () in
@@ -384,7 +383,7 @@ let do_report_scheduled () =
if success > 0 || (not shell && p = Qed) then
add_line name success (fun fmt ->
if p = Tactical then
- Stats.pp_stats ~shell ~updating fmt !script_stats
+ Stats.pp_stats ~shell ~cache fmt !script_stats
else
if not shell then Stats.pp_pstats fmt s
)
@@ -441,7 +440,7 @@ let spawn_wp_proofs ~script goals =
let server = ProverTask.server () in
ignore (Wp_parameters.Share.get_dir "."); (* To prevent further errors *)
let shell = Wp_parameters.has_dkey VCS.dkey_shell in
- let updating = Cache.is_updating () in
+ let cache = Cache.get_mode () in
Bag.iter
(fun goal ->
if script.tactical
@@ -458,7 +457,7 @@ let spawn_wp_proofs ~script goals =
~start:do_wpo_start
~progress:do_progress
~result:do_wpo_result
- ~success:(do_wpo_success ~shell ~updating)
+ ~success:(do_wpo_success ~shell ~cache)
goal
else
Prover.spawn goal
@@ -466,7 +465,7 @@ let spawn_wp_proofs ~script goals =
~start:do_wpo_start
~progress:do_progress
~result:do_wpo_result
- ~success:(do_wpo_success ~shell ~updating)
+ ~success:(do_wpo_success ~shell ~cache)
script.provers
) goals ;
Task.on_server_wait server do_wpo_wait ;
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle
index 6ddd0931f34..a8581030a4f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle
@@ -3,7 +3,7 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 24 goals scheduled
-[wp] [Valid] typed_lemma_ASSOC_land_qed_ok (Alt-Ergo)
+[wp] [Valid] typed_lemma_ASSOC_land_qed_ok (Alt-Ergo) (Trivial)
[wp] [Valid] typed_lemma_L01_lnot_qed_ok (Qed)
[wp] [Valid] typed_lemma_L10_land_neutral_qed_ok (Qed)
[wp] [Valid] typed_lemma_L11_land_absorbant_qed_ok (Qed)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle
index a5060678d1e..d5cde66a39e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle
@@ -3,22 +3,22 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 22 goals scheduled
-[wp] [Valid] typed_f_ensures_d0_div_pos_pos (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_d1_div_neg_pos (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_d2_div_pos_neg (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_d3_div_neg_neg (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_d4_div_x_1 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_d5_div_x_minus1 (Alt-Ergo)
+[wp] [Valid] typed_f_ensures_d0_div_pos_pos (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_d1_div_neg_pos (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_d2_div_pos_neg (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_d3_div_neg_neg (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_d4_div_x_1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_d5_div_x_minus1 (Alt-Ergo) (Trivial)
[wp] [Valid] typed_f_ensures_d6_div_0_x (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_sd0_div_pos_pos (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_sd1_div_neg_pos (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_sd2_div_pos_neg (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_sd3_div_neg_neg (Alt-Ergo) (Cached)
-[wp] [Valid] typed_f_ensures_m0_mod_pos_pos (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_m1_mod_neg_pos (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_m2_mod_pos_neg (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_m3_mod_neg_neg (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_m4_mod_x_1 (Alt-Ergo)
+[wp] [Valid] typed_f_ensures_m0_mod_pos_pos (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_m1_mod_neg_pos (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_m2_mod_pos_neg (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_m3_mod_neg_neg (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_m4_mod_x_1 (Alt-Ergo) (Trivial)
[wp] [Valid] typed_f_ensures_m5_mod_x_minus1 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_m6_mod_0_x (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_sm0_mod_pos_pos (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
index a5060678d1e..d5cde66a39e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle
@@ -3,22 +3,22 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 22 goals scheduled
-[wp] [Valid] typed_f_ensures_d0_div_pos_pos (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_d1_div_neg_pos (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_d2_div_pos_neg (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_d3_div_neg_neg (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_d4_div_x_1 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_d5_div_x_minus1 (Alt-Ergo)
+[wp] [Valid] typed_f_ensures_d0_div_pos_pos (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_d1_div_neg_pos (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_d2_div_pos_neg (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_d3_div_neg_neg (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_d4_div_x_1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_d5_div_x_minus1 (Alt-Ergo) (Trivial)
[wp] [Valid] typed_f_ensures_d6_div_0_x (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_sd0_div_pos_pos (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_sd1_div_neg_pos (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_sd2_div_pos_neg (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_sd3_div_neg_neg (Alt-Ergo) (Cached)
-[wp] [Valid] typed_f_ensures_m0_mod_pos_pos (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_m1_mod_neg_pos (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_m2_mod_pos_neg (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_m3_mod_neg_neg (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_m4_mod_x_1 (Alt-Ergo)
+[wp] [Valid] typed_f_ensures_m0_mod_pos_pos (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_m1_mod_neg_pos (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_m2_mod_pos_neg (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_m3_mod_neg_neg (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_m4_mod_x_1 (Alt-Ergo) (Trivial)
[wp] [Valid] typed_f_ensures_m5_mod_x_minus1 (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_m6_mod_0_x (Alt-Ergo) (Cached)
[wp] [Valid] typed_f_ensures_sm0_mod_pos_pos (Alt-Ergo) (Cached)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
index d81a58058fb..7220f33e5bb 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle
@@ -3,48 +3,48 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 42 goals scheduled
-[wp] [Valid] typed_f_ensures_p0 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_p1 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_p2 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_p3 (Alt-Ergo)
+[wp] [Valid] typed_f_ensures_p0 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_p1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_p2 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_p3 (Alt-Ergo) (Trivial)
[wp] [Valid] typed_f_ensures_p4 (Qed)
-[wp] [Valid] typed_f_ensures_p5 (Alt-Ergo)
+[wp] [Valid] typed_f_ensures_p5 (Alt-Ergo) (Trivial)
[wp] [Valid] typed_f_ensures_p6 (Qed)
-[wp] [Valid] typed_f_ensures_p7 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_p8 (Alt-Ergo)
+[wp] [Valid] typed_f_ensures_p7 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_p8 (Alt-Ergo) (Trivial)
[wp] [Valid] typed_f_ensures_p9 (Qed)
[wp] [Valid] typed_f_ensures_i0 (Qed)
-[wp] [Valid] typed_f_ensures_i1 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_i2 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_i3 (Alt-Ergo)
+[wp] [Valid] typed_f_ensures_i1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_i2 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_i3 (Alt-Ergo) (Trivial)
[wp] [Valid] typed_f_ensures_i4 (Qed)
[wp] [Valid] typed_f_ensures_i5 (Qed)
-[wp] [Valid] typed_f_ensures_i6 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_i7 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_i8 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_i9 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_a0 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_a1 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_a2 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_a3 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_a4 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_a5 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_a6 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_a7 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_a8 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_a9 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_o0 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_o1 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_o2 (Alt-Ergo)
+[wp] [Valid] typed_f_ensures_i6 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_i7 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_i8 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_i9 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_a0 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_a1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_a2 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_a3 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_a4 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_a5 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_a6 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_a7 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_a8 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_a9 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_o0 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_o1 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_o2 (Alt-Ergo) (Trivial)
[wp] [Valid] typed_f_ensures_o3 (Qed)
[wp] [Valid] typed_f_ensures_o4 (Qed)
-[wp] [Valid] typed_f_ensures_o5 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_o6 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_o7 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_o8 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_o9 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_f0 (Alt-Ergo)
-[wp] [Valid] typed_f_ensures_f1 (Alt-Ergo)
+[wp] [Valid] typed_f_ensures_o5 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_o6 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_o7 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_o8 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_o9 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_f0 (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_f_ensures_f1 (Alt-Ergo) (Trivial)
[wp] Proved goals: 42 / 42
Qed: 8
Alt-Ergo: 34
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle
index dbd9f8b4b0c..8bf423bc3d8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle
@@ -4,7 +4,7 @@
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_foo_assert_A (Alt-Ergo) (Cached)
-[wp] [Valid] typed_foo_assert_B (Alt-Ergo)
+[wp] [Valid] typed_foo_assert_B (Alt-Ergo) (Trivial)
[wp] Proved goals: 2 / 2
Alt-Ergo: 2
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
index 0d08a88a9eb..f95573ce220 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle
@@ -4,8 +4,8 @@
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Valid] typed_f3_assigns (Qed)
-[wp] [Valid] typed_g3_assigns_exit (Alt-Ergo)
-[wp] [Valid] typed_g3_assigns_normal (Alt-Ergo)
+[wp] [Valid] typed_g3_assigns_exit (Alt-Ergo) (Trivial)
+[wp] [Valid] typed_g3_assigns_normal (Alt-Ergo) (Trivial)
[wp] [Valid] typed_g3_call_f3_requires (Qed)
[wp] Proved goals: 4 / 4
Qed: 2
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
index 6921707a0c6..b61eb16b985 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing issue_447.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] [Valid] typed_lemma_foo (Alt-Ergo)
+[wp] [Valid] typed_lemma_foo (Alt-Ergo) (Trivial)
[wp] Proved goals: 1 / 1
Alt-Ergo: 1
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
index f567293cdba..b6eb918828a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
@@ -5,7 +5,7 @@
No code nor implicit assigns clause for function Write, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
-[wp] [Valid] typed_Job_ensures (Alt-Ergo)
+[wp] [Valid] typed_Job_ensures (Alt-Ergo) (Trivial)
[wp] Proved goals: 1 / 1
Alt-Ergo: 1
------------------------------------------------------------
--
GitLab