Frama-C API - Stats
Performance Reporting
type pstats = {
tmin : float;
(*minimum prover time (non-smoke proof only)
*)tval : float;
(*cummulated prover time (non-smoke proof only)
*)tmax : float;
(*maximum prover time (non-smoke proof only)
*)tnbr : float;
(*number of non-smoke proofs
*)time : float;
(*cumulated prover time (smoke and non-smoke)
*)success : float;
(*number of success (valid xor smoke)
*)
}
Prover Stats
type stats = {
best : VCS.verdict;
(*provers best verdict (not verdict of the goal)
*)provers : (VCS.prover * pstats) list;
(*meaningfull provers
*)tactics : int;
(*number of tactics
*)proved : int;
(*number of proved sub-goals
*)timeout : int;
(*number of timeouts and stepouts sub-goals
*)unknown : int;
(*number of unknown sub-goals
*)noresult : int;
(*number of no-result sub-goals
*)failed : int;
(*number of failed sub-goals
*)cached : int;
(*number of cached prover results
*)cacheable : int;
(*number of prover results that can be cached
*)
}
Cumulated Stats
Remark: for each sub-goal, only the _best_ prover result is kept
val pp_pstats : Stdlib.Format.formatter -> pstats -> unit
val pp_stats : shell:bool -> cache:Cache.mode -> Stdlib.Format.formatter -> stats -> unit
val pretty : Stdlib.Format.formatter -> stats -> unit
val empty : stats
val results : smoke:bool -> (VCS.prover * VCS.result) list -> stats
val script : stats -> VCS.result
val subgoals : stats -> int
val complete : stats -> bool