package frama-c

  1. Overview
  2. Docs
Platform dedicated to the analysis of source code written in C

Install 

dune-project
 Dependency

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

Authors

  1. M
    Michele Alberti
  2. T
    Thibaud Antignac
  3. G
    Gergö Barany
  4. P
    Patrick Baudin
  5. T
    Thibaut Benjamin
  6. A
    Allan Blanchard
  7. L
    Lionel Blatter
  8. F
    François Bobot
  9. R
    Richard Bonichon
  10. Q
    Quentin Bouillaguet
  11. D
    David Bühler
  12. Z
    Zakaria Chihani
  13. L
    Loïc Correnson
  14. J
    Julien Crétin
  15. P
    Pascal Cuoq
  16. Z
    Zaynah Dargaye
  17. B
    Basile Desloges
  18. J
    Jean-Christophe Filliâtre
  19. P
    Philippe Herrmann
  20. M
    Maxime Jacquemin
  21. F
    Florent Kirchner
  22. A
    Alexander Kogtenkov
  23. T
    Tristan Le Gall
  24. J
    Jean-Christophe Léchenet
  25. M
    Matthieu Lemerre
  26. D
    Dara Ly
  27. D
    David Maison
  28. C
    Claude Marché
  29. A
    André Maroneze
  30. T
    Thibault Martin
  31. F
    Fonenantsoa Maurica
  32. M
    Melody Méaulle
  33. B
    Benjamin Monate
  34. Y
    Yannick Moy
  35. P
    Pierre Nigron
  36. A
    Anne Pacalet
  37. V
    Valentin Perrelle
  38. G
    Guillaume Petiot
  39. D
    Dario Pinto
  40. V
    Virgile Prevosto
  41. A
    Armand Puccetti
  42. F
    Félix Ridoux
  43. V
    Virgile Robles
  44. J
    Jan Rochel
  45. M
    Muriel Roger
  46. J
    Julien Signoles
  47. N
    Nicolas Stouls
  48. K
    Kostyantyn Vorobyov
  49. B
    Boris Yakobowski

Maintainers

  1. F
    frama-ci-bot@frama-c.com

Sources

frama-c-28.1-Nickel.tar.gz
sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

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

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. cachemiss : int;
    (*

    number of non-cached prover results

    *)
}

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