package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct