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 (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

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 = {

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
*)

}

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 proofs : stats -> int

Sourceval complete : stats -> bool

On This Page

Performance Reporting