Frama-C API - WpContext
Model Registration
type hypotheses = MemoryContext.partition -> MemoryContext.partition
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
val compute_hypotheses : model -> Frama_c_kernel.Kernel_function.t -> MemoryContext.partition
type t = context
module S : sig ... end
module MODEL : sig ... end
module SCOPE : sig ... end
val on_context : context -> ('a -> 'b) -> 'a -> 'b
val get_model : unit -> model
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
projectified, depend on the model, not serialized
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