package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Performance Reporting

type 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

type stats = {
  1. verdict : VCS.verdict;
    (*

    global verdict

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

    meaningfull provers

    *)
  3. tactics : int;
    (*

    number of tactics

    *)
  4. proved : int;
    (*

    number of proved sub-goals

    *)
  5. trivial : int;
    (*

    number of proved sub-goals with Qed or No-prover time

    *)
  6. timeout : int;
    (*

    number of resulting timeouts and stepouts

    *)
  7. unknown : int;
    (*

    number of resulting unknown

    *)
  8. noresult : int;
    (*

    number of no-result

    *)
  9. failed : int;
    (*

    number of resulting failures

    *)
  10. cached : int;
    (*

    number of cached (non-trivial) results

    *)
}

Cumulated Stats

Remark: for each sub-goal, only the _best_ prover result is kept

val pp_pstats : Format.formatter -> pstats -> unit
val pp_stats : shell:bool -> cache:Cache.mode -> 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
val proofs : stats -> int
val complete : stats -> bool
OCaml

Innovation. Community. Security.