package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Registration
Access
Dedicated access to plug-in parameters
Dynamically Loaded Modules

Module `Frama_c_kernel.Dynamic`

Value accesses through dynamic typing.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

Registration

val register : 
  ?comment:string ->
  plugin:string ->
  string ->
  'a Type.t ->
  'a ->
  'a

register ~plugin name ty v registers v with the name name, the type ty and the plug-in plugin.

raises Type.AlreadyExists
if name already exists. In other words you cannot register a value with the same name twice.

before 26.0-Iron
there was a labeled argument journalized, that has been removed when Journalization has been removed.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

Access

exception Incompatible_type of string

exception Unbound_value of string

val get : plugin:string -> string -> 'a Type.t -> 'a

get ~plugin name ty returns the value registered with the name name, the type ty and the plug-in plugin. This plug-in will be loaded if required.

raises Unbound_value
if the name is not registered

raises Incompatible_type
if the name is not registered with a compatible type

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val iter : (string -> 'a Type.t -> 'a -> unit) -> unit

val iter_comment : (string -> string -> unit) -> unit

since Oxygen-20120901

Dedicated access to plug-in parameters

module Parameter : sig ... end

Module to use for accessing parameters of plug-ins. Assume that the plug-in is already loaded.

Dynamically Loaded Modules

val load_packages : string list -> unit

loads a list of Findlib packages

since 23.0-Vanadium

val load_module : string -> unit

Load the module specification. See -load-module option.

val load_plugin : string -> unit