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/WpContext/index.html

Module Wp.WpContextSource

Model Registration

Sourcetype model
Sourcetype scope =
  1. | Global
  2. | Kf of Frama_c_kernel.Kernel_function.t
Sourcetype rollback = unit -> unit
Sourceval register : id:string -> ?descr:string -> configure:(unit -> rollback) -> ?hypotheses:hypotheses -> unit -> model

Model registration. The model is identified by id and described by descr (that defaults to id). The configure function is called on WpContext.on_context call, it must prepare and set the different Context.values related to the model. It must return the function that allows to rollback on the original state. The hypotheses function must return the hypotheses made by the model.

Sourceval get_descr : model -> string
Sourcetype context = model * scope
Sourcetype t = context
Sourcemodule S : sig ... end
Sourcemodule MODEL : sig ... end
Sourcemodule SCOPE : sig ... end
Sourcemodule MINDEX : Hashtbl.S with type key = model
Sourceval is_defined : unit -> bool
Sourceval on_context : context -> ('a -> 'b) -> 'a -> 'b
Sourceval get_model : unit -> model
Sourceval get_ident : unit -> string
Sourceval get_scope : unit -> scope
Sourceval get_context : unit -> context
Sourceval directory : unit -> Frama_c_kernel.Filepath.t

Current model in "-wp-out" directory

Sourcemodule type Entries = sig ... end
Sourcemodule type Registry = sig ... end
Sourcemodule Index (E : Entries) : Registry with module E = E

projectified, depend on the model, not serialized

Sourcemodule Static (E : Entries) : Registry with module E = E

projectified, independent from the model, not serialized

Sourcemodule type Key = sig ... end
Sourcemodule type Data = sig ... end
Sourcemodule type IData = sig ... end
Sourcemodule type Generator = sig ... end
Sourcemodule Generator (K : Key) (D : Data with type key = K.t) : Generator with type key = D.key and type data = D.data

projectified, depend on the model, not serialized

Sourcemodule StaticGenerator (K : Key) (D : Data with type key = K.t) : Generator with type key = D.key and type data = D.data

projectified, independent from the model, not serialized

Sourcemodule GeneratorID (K : Key) (D : IData with type key = K.t) : Generator with type key = D.key and type data = D.data

projectified, depend on the model, not serialized

Sourcemodule StaticGeneratorID (K : Key) (D : IData with type key = K.t) : Generator with type key = D.key and type data = D.data

projectified, independent from the model, not serialized