Index of modules

B
Basic_alloc
Basic_blocks
C
Calloc
E
Enabled [Instantiator_builder.Instantiator]

Plugin option that allows to check whether the instantiator is enabled.

Enabled [Options]

Instantiate transformation enabled

F
Free
G
Global_context
Global_context [Instantiate]
H
Hashtbl [Instantiator_builder.Generator_sig]

Hashtbl module used by the Make_instantiator module to generate the function cache.

Hashtbl [Instantiate.Instantiator_builder.Generator_sig]

Hashtbl module used by the Make_instantiator module to generate the function cache.

I
Instantiate
Instantiator_builder
Instantiator_builder [Instantiate]
K
Key [Datatype.Hashtbl]

Datatype for the keys of the hashtbl.

Kfs [Options]

Set of kernel function provided for transformation

M
Make [Mem_utils]
Make [Datatype.Hashtbl]

Build a datatype of the hashtbl according to the datatype of values in the hashtbl.

Make_instantiator [Instantiator_builder]

Generates a Instantiator from a Generator_sig adding all necessary stuff for cache and function definition generation, as well as specification registration.

Malloc
Mem_utils
Memcmp
Memcpy
Memmove
Memset
N
NewInstantiator [Options]

Used by Instantiator_builder to generate options.

O
Options
R
Register

Register the plugin in the Frama-C kernel.

T
Transform

Module for AST transformation

Transform [Instantiate]