Frama-C API - Record

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