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-server.core/Server/Data/Record/index.html

Module Data.RecordSource

Record factory.

You shall start by declaring a (ghost) type r and call Record.signature to create a signature of type r, which will be your container to register your record fields.

Then, populate the signature with Record.field or Record.option. Finally, you shall call Record.publish to pack the record signature and obtain a new data module of type Record with type r = r, which gives you a Data with an opaque type t = r record with fields of type (r,a) field.

  (* ---- Exemple of Record Data --- *)
  type r
  let s = Record.signature () in
  let fd_a = Record.field s ~name:"a" ~descr:"..." (module A) in
  let fd_b = Record.field s ~name:"b" ~descr:"..." (module B) in
  let r = Record.publish s ~page ~kind ~name ~descr
  module M = (val r) : Record with type r = r)

  let make a b = M.default |> M.set fd_a a |> M.set fd_b b
Sourcetype 'a record

Records of type 'a.

Sourcetype 'a signature

Opened signature for record of type 'a.

Sourcetype ('a, 'b) field

Field of type 'b for a record of type 'a.

Sourcemodule type S = sig ... end

Data with type t = r record. Also contains getters and setters for fields.

Sourceval signature : unit -> 'a signature

Create a new, opened record type.

Sourceval field : 'r signature -> name:string -> descr:Frama_c_kernel.Markdown.text -> ?default:'a -> 'a data -> ('r, 'a) field

Adds a field to an opened record.

Sourceval option : 'r signature -> name:string -> descr:Frama_c_kernel.Markdown.text -> 'a data -> ('r, 'a option) field

Adds a optional field to an opened record.

Sourceval publish : package:Package.package -> name:string -> ?descr:Frama_c_kernel.Markdown.text -> 'a signature -> (module S with type r = 'a)

Publish and close an opened record.