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

Maintainers

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

Sources

frama-c-30.0-beta-Zinc.tar.gz
sha256=93a291a8764644df2f3618d7ea18258b5fbe0912ec98dfdfd180967afdf24474

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

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