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. J
    Jean-Christophe Léchenet
  28. M
    Matthieu Lemerre
  29. D
    Dara Ly
  30. D
    David Maison
  31. C
    Claude Marché
  32. A
    André Maroneze
  33. T
    Thibault Martin
  34. F
    Fonenantsoa Maurica
  35. M
    Melody Méaulle
  36. B
    Benjamin Monate
  37. Y
    Yannick Moy
  38. P
    Pierre Nigron
  39. A
    Anne Pacalet
  40. V
    Valentin Perrelle
  41. G
    Guillaume Petiot
  42. D
    Dario Pinto
  43. V
    Virgile Prevosto
  44. A
    Armand Puccetti
  45. F
    Félix Ridoux
  46. V
    Virgile Robles
  47. J
    Jan Rochel
  48. M
    Muriel Roger
  49. J
    Julien Signoles
  50. N
    Nicolas Stouls
  51. K
    Kostyantyn Vorobyov
  52. B
    Boris Yakobowski

Maintainers

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

Sources

frama-c-29.0-Copper.tar.gz
sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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.