package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/Stats/index.html

Module `Wp.Stats`Source

Performance Reporting

Sourcetype 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

Sourcetype 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

Sourceval pp_pstats : Format.formatter -> pstats -> unit

val pp_stats : 
  shell:bool ->
  cache:Cache.mode ->
  Format.formatter ->
  stats ->
  unit

Sourceval pretty : Format.formatter -> stats -> unit

Sourceval empty : stats

Sourceval add : stats -> stats -> stats

Sourceval results : smoke:bool -> (VCS.prover * VCS.result) list -> stats

Sourceval tactical : qed:float -> stats list -> stats

Sourceval script : stats -> VCS.result

Sourceval subgoals : stats -> int

Sourceval complete : stats -> bool

On This Page

Performance Reporting