package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Wp.StatsSource

Performance Reporting

Sourcetype pstats = {
  1. tmin : float;
    (*

    minimum prover time (non-smoke proof only)

    *)
  2. tval : float;
    (*

    cummulated prover time (non-smoke proof only)

    *)
  3. tmax : float;
    (*

    maximum prover time (non-smoke proof only)

    *)
  4. tnbr : float;
    (*

    number of non-smoke proofs

    *)
  5. time : float;
    (*

    cumulated prover time (smoke and non-smoke)

    *)
  6. success : float;
    (*

    number of success (valid xor smoke)

    *)
}

Prover Stats

Sourcetype stats = {
  1. best : VCS.verdict;
    (*

    provers best verdict (not verdict of the goal)

    *)
  2. provers : (VCS.prover * pstats) list;
    (*

    meaningfull provers

    *)
  3. tactics : int;
    (*

    number of tactics

    *)
  4. proved : int;
    (*

    number of proved sub-goals

    *)
  5. timeout : int;
    (*

    number of timeouts and stepouts sub-goals

    *)
  6. unknown : int;
    (*

    number of unknown sub-goals

    *)
  7. noresult : int;
    (*

    number of no-result sub-goals

    *)
  8. failed : int;
    (*

    number of failed sub-goals

    *)
  9. cached : int;
    (*

    number of cached prover results

    *)
  10. 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
Sourceval 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct