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. A
    Anne Pacalet
  36. V
    Valentin Perrelle
  37. G
    Guillaume Petiot
  38. D
    Dario Pinto
  39. V
    Virgile Prevosto
  40. A
    Armand Puccetti
  41. F
    Félix Ridoux
  42. V
    Virgile Robles
  43. M
    Muriel Roger
  44. J
    Julien Signoles
  45. N
    Nicolas Stouls
  46. K
    Kostyantyn Vorobyov
  47. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-27.0-beta-Cobalt.tar.gz
sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

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_scope : unit -> scope
Sourceval get_context : unit -> context

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