package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

doc/frama-c.kernel/Frama_c_kernel/Dynamic/index.html

Module `Frama_c_kernel.Dynamic`

Value accesses through dynamic typing.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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
Plug-in Development Guide

Access

exception Incompatible_type of string

exception Unbound_value of string

exception Unloadable of string

Exception that a plug-in can throw if it detects that it can't be loaded. It is caught by Dynamic.load_module and Dynamic.load_script

since Oxygen-20120901

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

raises Failure
_ in the -no-obj mode

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf
Plug-in Development Guide

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

On This Page

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