Download the Plugin Development Guide - Frama-C

4.16. VISITORS
B Type-checking:
a normal
Cabs.file (i.e.
not obtained through a custom parsing func-
tion) can be transformed before being type-checked. Transformation hooks are registered
through
C Frontc.add_syntactic_transformation.
After linking:
Once all source les have been processed, they are all linked together in
a single AST. Transformations can be performed on the resulting AST at two stages:
1. before clean-up (i.e. removal of useless temporary variables and prototypes that are
never called). At that stage, global tables indexing information related to the AST
(see gure 5.4) have not yet been lled.
2. after clean-up. At this stage, index tables are lled, and can thus be used. On the
other hand, the transformation must take care itself of keeping in sync the AST and
the tables
Registering
a
transformation
for
this
stage
is
done
through
the
func-
File.add_code_transformation_before_cleanup
(respectively
File.add_code_transformation_after_cleanup). If such a transformation modify the control-ow graph of a function f, in particular by adding statements, it must
call File.must_recompute_cfg, in order to have the graph recomputed afterwards.
tion
4.16 Visitors
Prerequisite:
knowledge of OCaml object programming.
Cil oers a visitor,
Cil.cilVisitor
that allows to traverse (parts of ) an AST. It is a class
with one method per type of the AST, whose default behavior is simply to call the method
corresponding to its children.
This is a convenient way to perform local transformations
Cil_types.file
by inheriting from it and redening a few methods. However,
over a whole
the original Cil visitor is of course not aware of the internal state of Frama-C itself. Hence,
there exists another visitor,
Visitor.generic_frama_c_visitor,
which handles projects in
a transparent way for the user. There are very few cases where the plain Cil visitor should be
used.
Basically, as soon as the initial project has been built from the C source les (i.e. one of
the functions
File.init_∗
has been applied), only the Frama-C visitor should occur.
There are a few dierences between the two (the Frama-C visitor inherits from the Cil one).
These dierences are summarized in Section 4.16.6, which the reader already familiar with Cil
is invited to read carefully.
4.16.1 Entry Points
Cil oers various entry points for the visitor. They are functions called
Cil.visitCilAstType
where astType is a node type in the Cil's AST. Such a function takes as argument an instance of a
cilVisitor
and an astType and gives back an astType transformed according to
Cil_types.file (Cil.visitCilFileCopy,
Cil.visitCilFile and visitCilFileSameGlobals) are slightly dierent and do not support
all kinds of visitors. See the documentation attached to them in cil.mli for more details.
the visitor. The entry points for visiting a whole
81