package frama-c

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

Model Registration

type model
type scope =
  1. | Global
  2. | Kf of Frama_c_kernel.Kernel_function.t
type rollback = unit -> unit
val 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.

val get_descr : model -> string
val get_emitter : model -> Frama_c_kernel.Emitter.t
type context = model * scope
type t = context
module S : sig ... end
module MODEL : sig ... end
module SCOPE : sig ... end
module MINDEX : Stdlib.Hashtbl.S with type key = model
val is_defined : unit -> bool
val on_context : context -> ('a -> 'b) -> 'a -> 'b
val get_model : unit -> model
val get_ident : unit -> string
val get_scope : unit -> scope
val get_context : unit -> context
val directory : unit -> Frama_c_kernel.Datatype.Filepath.t

Current model in "-wp-out" directory

module type Entries = sig ... end
module type Registry = sig ... end
module Index (E : Entries) : Registry with module E = E

projectified, depend on the model, not serialized

module Static (E : Entries) : Registry with module E = E

projectified, independent from the model, not serialized

module type Key = sig ... end
module type Data = sig ... end
module type IData = sig ... end
module type Generator = sig ... end
module 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

module 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

module 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

module 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