Module Frama_c_kernel.Dynamic

Value accesses through dynamic typing.

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.

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.

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