Download the Plugin Development Guide - Frama-C

4.12. PROJECT MANAGEMENT SYSTEM
1. To declare a new internal state, apply one of the predened functors in modules
State_builder
Cil_state_builder (see interfaces of these modules for the list of
available modules). Here we use Cil_state_builder.Stmt_hashtbl which provides an
or
hashtable indexed by statements. The type of values associated to statements is a pair
of
Kernel_function.t
and
Cil_types.varinfo.
The rst argument of the functor is
then the datatype corresponding to this type (see Section 4.9.2). The second argument
provides some additional information: the initial size of the hashtable (an integer similar
to the argument of
Hashtbl.create),
an unique name for the resulting state and its
dependencies. This list of dependencies is built upon values
self which are called state
kind (or simply kind ) and are part of any state's module (part of the signature of the
low-level functor
State_builder.Register).
This value represents the state itself as
rst-class value (like type values for OCaml types, see Section 4.9.1).
2. From outside, a state actually hides its internal representation in order to ensure some
invariants: operations on states implementing hashtable does not take an hashtable in
argument because they implicitly use the hidden hashtable. In our example, a predened memo function is used in order to memoize the computation of
compute_info.
This memoization function implicitly operates on the hashtable hidden in the internal
representation of
State.
Postponed dependencies
Sometimes, you want to access to a state kind before dening it.
That is usually the case when you have two mutually-dependent states: the dependencies of
the rst one providing when registering it must contain the state kind of the second one which
is created by registering it. But this second registration also requires a list of dependencies
containing the rst state kind.
For solving this issue, it is possible to postpone the addition of a state kind to dependencies
until all modules have been initialized. However, dependencies must be correct before anything serious is computed by Frama-C. So the right way to do this is the use of the function
Cmdline.run_after_extended_stage
(see Section 4.14 for advanced explanation about the
way Frama-C is initialized).
Example 4.25
Plug-in
from
puts a reference to its state kind in the following way.
reference is initialized at module initialization time.
File src/kernel/db.mli
module From = s t r u c t
...
val s e l f : State . t r e f
end
File src/kernel/db.ml
module From = s t r u c t
...
v a l s e l f = r e f S t a t e .dummy
end
( * postponed * )
File src/from/functionwise.ml
module Tbl =
K e r n e l _ f u n c t i o n .Make_Table
( Function_Froms )
( struct
71
This