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. N
    Nicolas Bellec
  6. T
    Thibaut Benjamin
  7. A
    Allan Blanchard
  8. L
    Lionel Blatter
  9. F
    François Bobot
  10. R
    Richard Bonichon
  11. V
    Vincent Botbol
  12. Q
    Quentin Bouillaguet
  13. D
    David Bühler
  14. Z
    Zakaria Chihani
  15. S
    Sylvain Chiron
  16. L
    Loïc Correnson
  17. J
    Julien Crétin
  18. P
    Pascal Cuoq
  19. Z
    Zaynah Dargaye
  20. B
    Basile Desloges
  21. J
    Jean-Christophe Filliâtre
  22. P
    Philippe Herrmann
  23. M
    Maxime Jacquemin
  24. B
    Benjamin Jorge
  25. F
    Florent Kirchner
  26. A
    Alexander Kogtenkov
  27. R
    Remi Lazarini
  28. T
    Tristan Le Gall
  29. K
    Kilyan Le Gallic
  30. J
    Jean-Christophe Léchenet
  31. M
    Matthieu Lemerre
  32. D
    Dara Ly
  33. D
    David Maison
  34. C
    Claude Marché
  35. A
    André Maroneze
  36. T
    Thibault Martin
  37. F
    Fonenantsoa Maurica
  38. M
    Melody Méaulle
  39. B
    Benjamin Monate
  40. Y
    Yannick Moy
  41. P
    Pierre Nigron
  42. A
    Anne Pacalet
  43. V
    Valentin Perrelle
  44. G
    Guillaume Petiot
  45. D
    Dario Pinto
  46. V
    Virgile Prevosto
  47. A
    Armand Puccetti
  48. F
    Félix Ridoux
  49. V
    Virgile Robles
  50. J
    Jan Rochel
  51. M
    Muriel Roger
  52. C
    Cécile Ruet-Cros
  53. J
    Julien Signoles
  54. N
    Nicolas Stouls
  55. K
    Kostyantyn Vorobyov
  56. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-31.0-Gallium.tar.gz
sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

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

Module Wp.ProverTaskSource

Sourceclass printer : Format.formatter -> string -> object ... end
Sourceval pp_file : message:string -> file:Frama_c_kernel.Filepath.t -> unit
Sourceclass type pattern = object ... end

never fails

Sourceval p_group : string -> string

Put pattern in group \(p\)

Sourceval p_int : string

Int group pattern \([0-9]+\)

Sourceval p_float : string

Float group pattern \([0-9.]+\)

Sourceval p_string : string

String group pattern "\(...\)"

Sourceval p_until_space : string

No space group pattern "\\(^ \t\n*\\)"

Sourceval location : string -> int -> Lexing.position
Sourcetype logs = [
  1. | `OUT
  2. | `ERR
  3. | `BOTH
]
Sourceclass virtual command : string -> object ... end
Sourceval server : ?procs:int -> unit -> Frama_c_kernel.Task.server

If provided, the number of procs is forwarded to the Why3 and the server

Sourceval schedule : 'a Frama_c_kernel.Task.task -> unit
Sourceval spawn : ?monitor:('a option -> unit) -> ?pool:Frama_c_kernel.Task.pool -> all:bool -> smoke:bool -> ('a * bool Frama_c_kernel.Task.task) list -> unit

Spawn all the tasks over the server and retain the first 'validated' one. The callback monitor is called with Some at first success, and None if none succeed. An option pool task can be passed to register the associated threads.