Download the Plugin Development Guide - Frama-C

5.3. MAKEFILES
UNPACKED_DIRS
which should be extended by a plug-in developer if he uses les which
do not belong to the plug-in directory (that is if variable
PLUGIN_TYPES_CMO
is set, see
Section 5.3.3).
2.
Installation paths denes where Frama-C has to be installed.
3.
Ocaml stu
4.
Libraries denes variables for libraries required by Frama-C.
5.
Miscellaneous commands denes some additional commands.
6.
Miscellaneous variables denes some additional variables.
7.
Variables for plug-ins
denes the OCaml compilers and specic related ags.
Frama-C (and using the
8.
9.
denes some variables used by plug-ins distributed within
configure
of Frama-C).
Flags denes some variables setting compilation ags.
Verbosing sets how make prints the command. In particular, it denes the variable
VERBOSEMAKE which must be set yes in order to see the full make commands in the user
console. The typical use is
$ make VERBOSEMAKE= y e s
10.
Shell commands sets all the shell commands eventually executed while calling make.
11.
Command pretty printing sets all the commands to be used for pretty printing.
Example 5.1
foo : bar
Consider the following target
foo
in a plug-in specic Makele.
$( PRINT_CP ) $@
$( CP ) $ < $@
Executing
$ make f o o
prints
Copying t o
foo
while executing
$ make f o o VERBOSEMAKE= y e s
prints
cp - f bar f o o
If one of the two commands is missing for the target
VERBOSEMAKE=yes
12.
13.
either
make foo
or
make foo
Tests denes a generic template for testing plug-ins.
Generic rules contains rules in order to automatically produces dierent kinds of les
(e.g.
14.
foo,
will not work as expected.
.cm[iox]
from
.ml
or
.mli
for OCaml les)
Global plug-in variables declares some plug-in specic variables used throughout the
makele.
99