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

[wp] improved global stats

parent fa041e2e
......@@ -52,6 +52,8 @@ val pp_stats : shell:bool -> updating:bool -> Format.formatter -> stats -> unit
val pretty : Format.formatter -> stats -> unit
val empty : stats
val add : stats -> stats -> stats
val results : smoke:bool -> (VCS.prover * VCS.result) list -> stats
val tactical : qed:float -> stats list -> stats
val script : stats -> VCS.result
......
......@@ -127,70 +127,24 @@ let pp_warnings fmt wpo =
(* --- Prover Stats --- *)
(* ------------------------------------------------------------------------ *)
module PM =
Map.Make(struct
type t = VCS.prover
let compare = VCS.cmp_prover
end)
type pstat = {
mutable proved : int ;
mutable unknown : int ;
mutable interrupted : int ;
mutable incache : int ;
mutable failed : int ;
mutable n_time : int ; (* nbr of measured times *)
mutable a_time : float ; (* sum of measured times *)
mutable u_time : float ; (* max time *)
mutable d_time : float ; (* min time *)
mutable steps : int ;
}
module GOALS = Wpo.S.Set
let scheduled = ref 0
let exercised = ref 0
let session = ref GOALS.empty
let provers = ref PM.empty
let global = ref Stats.empty
let clear_scheduled () =
begin
scheduled := 0 ;
exercised := 0 ;
session := GOALS.empty ;
provers := PM.empty ;
global := Stats.empty ;
CfgInfos.trivial_terminates := 0 ;
WpReached.unreachable_proved := 0 ;
WpReached.unreachable_failed := 0 ;
end
let get_pstat p =
try PM.find p !provers with Not_found ->
let s = {
proved = 0 ;
unknown = 0 ;
interrupted = 0 ;
failed = 0 ;
steps = 0 ;
incache = 0 ;
n_time = 0 ;
a_time = 0.0 ;
u_time = 0.0 ;
d_time = max_float ;
} in provers := PM.add p s !provers ; s
let add_step s n =
if n > s.steps then s.steps <- n
let add_time s t =
if t > 0.0 then
begin
s.n_time <- succ s.n_time ;
s.a_time <- t +. s.a_time ;
if t < s.d_time then s.d_time <- t ;
if t > s.u_time then s.u_time <- t ;
end
let do_list_scheduled goals =
Bag.iter
(fun goal ->
......@@ -268,55 +222,34 @@ let do_report_cache_usage mode =
(* --- Prover Results --- *)
(* -------------------------------------------------------------------------- *)
let do_wpo_stat goal prover res =
let s = get_pstat prover in
let open VCS in
if res.cached then s.incache <- succ s.incache ;
let smoke = Wpo.is_smoke_test goal in
let verdict = VCS.verdict ~smoke res in
match verdict with
| NoResult | Computing _ | Unknown ->
s.unknown <- succ s.unknown
| Stepout | Timeout ->
s.interrupted <- succ s.interrupted
| Failed | Invalid ->
s.failed <- succ s.failed
| Valid ->
s.proved <- succ s.proved ;
add_step s res.prover_steps ;
add_time s res.prover_time ;
if prover <> Qed then
add_time (get_pstat Qed) res.solver_time
let do_wpo_result goal prover res =
if VCS.is_verdict res then
begin
if prover = VCS.Qed then do_progress goal "Qed" ;
do_wpo_stat goal prover res ;
end
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 status =
if smoke then
match stats.verdict with
| Valid -> "Failed (Doomed)"
| Failed -> "Unknown (Failure)"
| NoResult | Computing _ -> "Unknown (Incomplete)"
| Unknown -> "Passed (Unknown)"
| Timeout -> "Passed (Timeout)"
| Stepout -> "Passed (Stepout)"
| Invalid -> "Passed (Invalid)"
| Valid -> "[Failed] (Doomed)"
| Failed -> "[Unknown] (Failure)"
| NoResult | Computing _ -> "[Unknown] (Incomplete)"
| (Unknown | Timeout | Stepout) when shell -> "[Passed] (Unsuccess)"
| Unknown -> "[Passed] (Unknown)"
| Timeout -> "[Passed] (Timeout)"
| Stepout -> "[Passed] (Stepout)"
| Invalid -> "[Passed] (Invalid)"
else
match stats.verdict with
| NoResult | Computing _ -> ""
| Valid -> "Valid"
| Invalid -> "Invalid"
| Failed -> "Failure"
| Unknown -> "Unknown"
| Timeout -> "Timeout"
| Stepout -> "Stepout"
| Valid -> "[Valid]"
| Invalid -> "[Invalid]"
| Failed -> "[Failure]"
| (Unknown | Timeout | Stepout) when shell -> "[Unsuccess]"
| Unknown -> "[Unknown]"
| Timeout -> "[Timeout]"
| Stepout -> "[Stepout]"
in if status <> "" then
Wp_parameters.feedback "[%s] %s%a%a"
Wp_parameters.feedback "%s %s%a%a"
status (Wpo.get_gid goal) (Stats.pp_stats ~shell ~updating) stats
pp_warnings goal
......@@ -329,9 +262,11 @@ let do_wpo_success ~shell ~updating goal success =
"[Generated] Goal %s (%a)" (Wpo.get_gid goal) VCS.pp_prover prover
else
let smoke = Wpo.is_smoke_test goal in
let gstats = Stats.results ~smoke @@ Wpo.get_results goal in
let stats = ProofEngine.consolidated goal in
let proof, target = Wpo.get_proof goal in
begin
global := Stats.add !global gstats ;
if shell || proof <> `Passed then
do_report_stats ~shell ~updating goal ~smoke stats ;
if smoke && proof <> `Passed then
......@@ -341,67 +276,6 @@ let do_wpo_success ~shell ~updating goal success =
end ;
end
let do_report_time fmt s =
begin
if s.n_time > 0 &&
s.u_time > Rformat.epsilon &&
not (Wp_parameters.has_dkey VCS.dkey_shell)
then
let mean = s.a_time /. float s.n_time in
let epsilon = 0.05 *. mean in
let delta = s.u_time -. s.d_time in
if delta < epsilon then
Format.fprintf fmt " (%a)" Rformat.pp_time mean
else
let middle = (s.u_time +. s.d_time) *. 0.5 in
if abs_float (middle -. mean) < epsilon then
Format.fprintf fmt " (%a-%a)"
Rformat.pp_time s.d_time
Rformat.pp_time s.u_time
else
Format.fprintf fmt " (%a-%a-%a)"
Rformat.pp_time s.d_time
Rformat.pp_time mean
Rformat.pp_time s.u_time
end
let do_report_steps fmt s =
begin
if s.steps > 0 &&
not (Wp_parameters.has_dkey VCS.dkey_shell)
then
Format.fprintf fmt " (%d)" s.steps ;
end
let do_report_stopped fmt s =
if Wp_parameters.has_dkey VCS.dkey_shell then
begin
let n = s.interrupted + s.unknown in
if n > 0 then
Format.fprintf fmt " (unsuccess: %d)" n ;
end
else
begin
if s.interrupted > 0 then
Format.fprintf fmt " (interrupted: %d)" s.interrupted ;
if s.unknown > 0 then
Format.fprintf fmt " (unknown: %d)" s.unknown ;
if s.incache > 0 then
Format.fprintf fmt " (cached: %d)" s.incache ;
end
let do_report_prover_stats pp_prover fmt (p,s) =
begin
let name = VCS.title_of_prover p in
Format.fprintf fmt "%a %4d " pp_prover name s.proved ;
do_report_time fmt s ;
do_report_steps fmt s ;
do_report_stopped fmt s ;
if s.failed > 0 then
Format.fprintf fmt " (failed: %d)" s.failed ;
Format.fprintf fmt "@\n" ;
end
let do_report_scheduled () =
if Wp_parameters.Generate.get () then
let plural = if !exercised > 1 then "s" else "" in
......@@ -414,24 +288,47 @@ let do_report_scheduled () =
!CfgInfos.trivial_terminates in
if total > 0 then
begin
let passed =
!WpReached.unreachable_proved + !CfgInfos.trivial_terminates
in
let gstats = !global in
let unreachable = !WpReached.unreachable_proved in
let terminating = !CfgInfos.trivial_terminates in
let passed = GOALS.fold
(fun g n ->
if Wpo.is_passed g then succ n else n
) !session passed in
) !session (unreachable + terminating) in
let mode = Cache.get_mode () in
if mode <> Cache.NoCache then do_report_cache_usage mode ;
let shell = Wp_parameters.has_dkey VCS.dkey_shell in
let lines = ref [] in
let none = fun _fmt -> () in
let add_line title count pp =
lines := (title,count,pp) :: !lines in
if terminating > 0 then add_line "Terminating" terminating none ;
if unreachable > 0 then add_line "Unreachable" unreachable none ;
List.iter
(fun (p,s) ->
let name = VCS.title_of_prover p in
let success = truncate s.Stats.success in
if success > 0 || (not shell && p = Qed) then
add_line name success (fun fmt ->
if shell then Stats.pp_pstats fmt s
)
) gstats.provers ;
if gstats.failed > 0 then add_line "Failed" gstats.failed none ;
if not shell then
begin
if gstats.timeout > 0 then add_line "Timeout" gstats.timeout none ;
if gstats.unknown > 0 then add_line "Unknown" gstats.unknown none ;
end ;
let iter f = List.iter f (List.rev !lines) in
let title (p,_,_) = p in
let pp_title fmt p = Format.fprintf fmt "%s:" p in
let pp_item pp fmt (a,n,msg) =
Format.fprintf fmt "%a %4d%t@\n" pp a n msg in
Wp_parameters.result "%t"
begin fun fmt ->
Format.fprintf fmt "Proved goals: %4d / %d@\n" passed total ;
Pretty_utils.pp_items
~min:12 ~align:`Left
~title:(fun (prover,_) -> VCS.title_of_prover prover)
~iter:(fun f -> PM.iter (fun p s -> f (p,s)) !provers)
~pp_title:(fun fmt a -> Format.fprintf fmt "%s:" a)
~pp_item:do_report_prover_stats fmt ;
~min:12 ~align:`Left ~title ~iter ~pp_title ~pp_item fmt ;
end ;
end
......
......@@ -7,9 +7,8 @@
[wp] bad_cast_call.i:8: Warning:
Cast with incompatible pointers types (source: sint8*) (target: char**)
[wp] 1 goal scheduled
[wp] [Unknown] typed_foo_assert_MUST_FAIL (Alt-Ergo) (Cached) (Stronger)
[wp] [Unsuccess] typed_foo_assert_MUST_FAIL (Alt-Ergo) (Cached) (Stronger)
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo - - 1 0.0%
......
......@@ -5,9 +5,8 @@
[wp] default-stmt-assigns.i:2: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
[wp] [Unknown] typed_automaton_state_accessor_assert (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_automaton_state_accessor_assert (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
automaton_state_accessor - - 1 0.0%
......
......@@ -5,10 +5,9 @@
Neither code nor specification for function bar, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Unknown] typed_foo_ensures (Alt-Ergo) (Cached)
[wp] [Unknown] typed_foo_exits (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_foo_ensures (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_foo_exits (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 2
Alt-Ergo: 0 (unsuccess: 2)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
foo - - 2 0.0%
......
......@@ -5,7 +5,6 @@
[wp] 1 goal scheduled
[wp] [Valid] typed_f_ensures (Alt-Ergo) (Cached)
[wp] Proved goals: 1 / 1
Qed: 0
Alt-Ergo: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
......@@ -16,29 +16,29 @@
[wp] [Valid] typed_some_seq_assert_2 (Qed)
[wp] [Valid] typed_main_ensures_result_assert (Qed)
[wp] [Valid] typed_main_assert (Qed)
[wp] [Timeout] typed_not_main_assert_bad (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_not_main_assert_bad (Alt-Ergo) (Cached)
[wp] [Valid] typed_main_assigns_global_assert (Qed)
[wp] [Valid] typed_main_assigns_global_assert_2 (Qed)
[wp] [Timeout] typed_main_assigns_global_assert_bad (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_main_assigns_global_assert_bad (Alt-Ergo) (Cached)
[wp] [Valid] typed_zloop_ensures (Qed)
[wp] [Timeout] typed_zloop_loop_invariant_preserved (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_zloop_loop_invariant_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_zloop_loop_invariant_established (Qed)
[wp] [Valid] typed_zloop_assert (Qed)
[wp] [Valid] typed_zloop_assert_2 (Qed)
[wp] [Timeout] typed_zloop_assert_3 (Alt-Ergo) (Cached)
[wp] [Timeout] typed_zloop_assert_bad (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_zloop_assert_3 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_zloop_assert_bad (Alt-Ergo) (Cached)
[wp] [Valid] typed_behavior2_assert (Qed)
[wp] [Valid] typed_behavior3_assert (Qed)
[wp] [Valid] typed_behavior4_assert (Qed)
[wp] [Unknown] typed_behavior5_assert_bad (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_behavior5_assert_bad (Alt-Ergo) (Cached)
[wp] [Valid] typed_if_assert_assert (Alt-Ergo) (Cached)
[wp] [Timeout] typed_if_assert_assert_2 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_if_assert_assert_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_if_assert_assert_3 (Qed)
[wp] [Timeout] typed_if_assert_assert_missing_return (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_if_assert_assert_missing_return (Alt-Ergo) (Cached)
[wp] [Valid] typed_compare_assert (Qed)
[wp] Proved goals: 19 / 27
Qed: 18
Alt-Ergo: 1 (unsuccess: 8)
Qed: 18
Alt-Ergo: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
empty 1 - 1 100%
......
......@@ -17,16 +17,16 @@
[wp] [Valid] typed_bhv_complete_neg_pos (Alt-Ergo) (Cached)
[wp] [Valid] typed_bhv_pos_ensures_qed_ok (Qed)
[wp] [Valid] typed_bhv_neg_ensures_qed_ok (Qed)
[wp] [Timeout] typed_assert_needed_assert_ko (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_assert_needed_assert_ko (Alt-Ergo) (Cached)
[wp] [Valid] typed_assert_needed_assert_qed_ok_ok_with_hyp (Qed)
[wp] [Unknown] typed_bts0513_ensures_ko1 (Alt-Ergo) (Cached)
[wp] [Unknown] typed_bts0513_ensures_ko2 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_bts0513_ensures_ko1 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_bts0513_ensures_ko2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_razT_loop_invariant_qed_ok_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_razT_loop_invariant_qed_ok_established (Qed)
[wp] [Timeout] typed_razT_b1_ensures_e1 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_razT_b1_ensures_e1 (Alt-Ergo) (Cached)
[wp] Proved goals: 15 / 19
Qed: 13
Alt-Ergo: 2 (unsuccess: 4)
Qed: 13
Alt-Ergo: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f 5 - 5 100%
......
......@@ -3,13 +3,12 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
[wp] [Stepout] typed_f_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Unknown] typed_f_x1_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Unknown] typed_f_x2_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Stepout] typed_min_bx_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Timeout] typed_min_by_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_f_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_f_x1_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_f_x2_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_min_bx_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_min_by_ensures_qed_ko (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 5
Alt-Ergo: 0 (unsuccess: 5)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f - - 3 0.0%
......
......@@ -5,7 +5,6 @@
[wp] 1 goal scheduled
[wp] [Valid] typed_f_ensures (Alt-Ergo) (Cached)
[wp] Proved goals: 1 / 1
Qed: 0
Alt-Ergo: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
......
......@@ -4,13 +4,12 @@
[rte:annot] annotating function bts0513_bis
[wp] Running WP plugin...
[wp] 4 goals scheduled
[wp] [Unknown] hoare_bts0513_ensures_qed_ko_ko1 (Alt-Ergo) (Cached)
[wp] [Unknown] hoare_bts0513_ensures_qed_ko_ko2 (Alt-Ergo) (Cached)
[wp] [Timeout] hoare_bts0513_bis_assert_qed_ko_ko1 (Alt-Ergo) (Cached)
[wp] [Unsuccess] hoare_bts0513_ensures_qed_ko_ko1 (Alt-Ergo) (Cached)
[wp] [Unsuccess] hoare_bts0513_ensures_qed_ko_ko2 (Alt-Ergo) (Cached)
[wp] [Unsuccess] hoare_bts0513_bis_assert_qed_ko_ko1 (Alt-Ergo) (Cached)
[wp] [Valid] hoare_bts0513_bis_assert_qed_ok_ok (Qed)
[wp] Proved goals: 1 / 4
Qed: 1
Alt-Ergo: 0 (unsuccess: 3)
Qed: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
bts0513 - - 2 0.0%
......
......@@ -28,7 +28,7 @@
[wp] [Valid] typed_uchar_range_assert_qed_ok_A1 (Qed)
[wp] [Valid] typed_uchar_range_assert_qed_ok_A2 (Qed)
[wp] Proved goals: 24 / 24
Qed: 23
Qed: 23
Alt-Ergo: 1
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
......
......@@ -3,9 +3,8 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Stepout] typed_cast_sgn_usgn_ensures_qed_ko_KO (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_cast_sgn_usgn_ensures_qed_ko_KO (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
cast_sgn_usgn - - 1 0.0%
......
......@@ -9,36 +9,36 @@
[wp] [Valid] typed_initialize_loop_assigns_part1 (Qed)
[wp] [Valid] typed_initialize_loop_assigns_part2 (Qed)
[wp] [Valid] typed_initialize_loop_assigns_part3 (Qed)
[wp] [Timeout] typed_range_check_FAILS (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_range_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_range_loop_assigns_part1 (Qed)
[wp] [Valid] typed_range_loop_assigns_part2 (Qed)
[wp] [Valid] typed_range_loop_assigns_part3 (Qed)
[wp] [Timeout] typed_field_check_FAILS (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_field_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_field_loop_assigns_part1 (Qed)
[wp] [Valid] typed_field_loop_assigns_part2 (Qed)
[wp] [Timeout] typed_array_check_FAILS (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_array_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_array_loop_assigns_part1 (Qed)
[wp] [Valid] typed_array_loop_assigns_part2 (Qed)
[wp] [Valid] typed_array_loop_assigns_part3 (Qed)
[wp] [Timeout] typed_index_check_FAILS (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_index_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_index_loop_assigns_part1 (Qed)
[wp] [Valid] typed_index_loop_assigns_part2 (Qed)
[wp] [Valid] typed_index_loop_assigns_part3 (Qed)
[wp] [Timeout] typed_descr_check_FAILS (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_descr_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_descr_loop_assigns_part1 (Qed)
[wp] [Valid] typed_descr_loop_assigns_part2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_descr_loop_assigns_part3 (Qed)
[wp] [Valid] typed_descr_loop_assigns_part4 (Qed)
[wp] [Valid] typed_descr_loop_assigns_part5 (Qed)
[wp] [Timeout] typed_comp_check_FAILS (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_comp_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_comp_loop_assigns_part1 (Qed)
[wp] [Valid] typed_comp_loop_assigns_part2 (Qed)
[wp] [Valid] typed_comp_loop_assigns_part3 (Qed)
[wp] [Unknown] typed_assigned_glob_check_FAILS (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_assigned_glob_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_assigned_glob_loop_invariant_CHECK_preserved (Alt-Ergo) (Cached)
[wp] [Valid] typed_assigned_glob_loop_invariant_CHECK_established (Qed)
[wp] [Timeout] typed_assigned_glob_check_FAILS_2 (Alt-Ergo) (Cached)
[wp] [Timeout] typed_assigned_glob_check_FAILS_3 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_assigned_glob_check_FAILS_2 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_assigned_glob_check_FAILS_3 (Alt-Ergo) (Cached)
[wp] [Valid] typed_assigned_glob_loop_assigns_part1 (Qed)
[wp] [Valid] typed_assigned_glob_loop_assigns_part2 (Qed)
[wp] [Valid] typed_assigned_glob_loop_assigns_part3 (Qed)
......@@ -46,8 +46,8 @@
[wp] [Valid] typed_assigned_glob_loop_assigns_2_part2 (Qed)
[wp] [Valid] typed_assigned_glob_loop_assigns_2_part3 (Qed)
[wp] Proved goals: 33 / 42
Qed: 29
Alt-Ergo: 4 (unsuccess: 9)
Qed: 29
Alt-Ergo: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
initialize 4 2 6 100%
......
......@@ -12,11 +12,11 @@
[wp] [Valid] typed_range_check_CHECK (Qed)
[wp] [Valid] typed_range_loop_assigns_part1 (Qed)
[wp] [Valid] typed_range_loop_assigns_part2 (Qed)
[wp] [Timeout] typed_field_check_FAILS (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_field_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_field_loop_assigns (Qed)
[wp] [Timeout] typed_array_check_FAILS (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_array_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_array_loop_assigns (Qed)
[wp] [Timeout] typed_index_check_FAILS (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_index_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_index_loop_assigns_part1 (Qed)
[wp] [Valid] typed_index_loop_assigns_part2 (Qed)
[wp] [Valid] typed_descr_loop_invariant_CHECK_preserved (Alt-Ergo) (Cached)
......@@ -27,11 +27,11 @@
[wp] [Valid] typed_descr_loop_assigns_part3 (Qed)
[wp] [Valid] typed_descr_loop_assigns_part4 (Qed)
[wp] [Valid] typed_descr_loop_assigns_part5 (Qed)
[wp] [Timeout] typed_comp_check_FAILS (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_comp_check_FAILS (Alt-Ergo) (Cached)
[wp] [Valid] typed_comp_loop_assigns (Qed)
[wp] Proved goals: 22 / 26
Qed: 15
Alt-Ergo: 7 (unsuccess: 4)
Qed: 15
Alt-Ergo: 7
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
initialize 2 2 4 100%
......
......@@ -3,18 +3,17 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Timeout] typed_atomic_check_FAIL (Alt-Ergo) (Cached)
[wp] [Timeout] typed_comp_check_FAIL (Alt-Ergo) (Cached)
[wp] [Timeout] typed_array_check_FAIL (Alt-Ergo) (Cached)
[wp] [Timeout] typed_assigned_glob_atomic_check_FAIL (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_atomic_check_FAIL (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_comp_check_FAIL (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_array_check_FAIL (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_assigned_glob_atomic_check_FAIL (Alt-Ergo) (Cached)
[wp] [Valid] typed_assigned_glob_atomic_check_OK (Alt-Ergo) (Cached)
[wp] [Timeout] typed_assigned_glob_comp_check_FAIL (Alt-Ergo) (Cached)
[wp] [Timeout] typed_assigned_glob_comp_check_FAIL_2 (Alt-Ergo) (Cached)
[wp] [Timeout] typed_assigned_glob_array_check_FAIL (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_assigned_glob_comp_check_FAIL (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_assigned_glob_comp_check_FAIL_2 (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_assigned_glob_array_check_FAIL (Alt-Ergo) (Cached)
[wp] [Valid] typed_assigned_glob_array_check_OK (Alt-Ergo) (Cached)
[wp] Proved goals: 2 / 9
Qed: 0
Alt-Ergo: 2 (unsuccess: 7)
Alt-Ergo: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
atomic - - 1 0.0%
......
......@@ -3,11 +3,10 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Timeout] typed_atomic_check_FAIL (Alt-Ergo) (Cached)
[wp] [Timeout] typed_comp_check_FAIL (Alt-Ergo) (Cached)
[wp] [Timeout] typed_array_check_FAIL (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_atomic_check_FAIL (Alt-Ergo) (Cached)