package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c-server.core/Server/Data/Record/index.html

Module `Data.Record`Source

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.

Source

val 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.

Source

val 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.

Source

val 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.

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-server.core/Server/Data/Record/index.html

Module Data.RecordSource

Module `Data.Record`Source