Commit bff858cb authored by Loïc Correnson's avatar Loïc Correnson Committed by Allan Blanchard
Browse files

[wp] refine cache statistics

parent 06ff8189
......@@ -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
......
......@@ -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
......
......@@ -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
(* -------------------------------------------------------------------------- *)
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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 ;
......
......@@ -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)
......
......@@ -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)
......
......@@ -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)
......
......@@ -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
......
......@@ -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
------------------------------------------------------------
......
......@@ -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
......
......@@ -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
------------------------------------------------------------
......
......@@ -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
------------------------------------------------------------
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment