Download User Manual - Frama-C

3.3.
3.3
Frama-C
FRAMA-C COMMAND LINE AND GENERAL OPTIONS
Command Line and General Options
The batch and interactive versions of Frama-C obey a number of command-line options. Any
option that exists in these two modes has the same meaning in both.
batch version can be made to launch the value analysis on the
frama-c -val foo.c.
foo.c
For instance, the
le with the command
Although the GUI allows to select les and to launch the value analysis
interactively, the command
on the le
foo.c
frama-c-gui -val foo.c can be used to launch the value analysis
and immediately start displaying the results in the GUI.
Any option requiring an argument may use the following format:
-option_name value
If the option's argument is a string (that is, neither an integer nor a oat,
format is also possible:
etc
), the following
-option_name=value.
This last format
must be used when
value
starts with a minus sign.
Most parameterless options have an opposite option, often written by prexing the option
no-.
-unicode for using the Unicode character set in
-no-unicode for limiting the messages to ACSII. Plugins options with a name of the form -<plug-in name>-<option name> have their opposite
option named -<plug-in name>-no-<option name>. For instance, the opposite of option
-ltl-acceptance is -ltl-no-acceptance.
name with
For instance, the option
messages has an opposite option
3.3.1 Splitting a Frama-C Execution into Several Steps
By default, Frama-C parses its command line in an
unspecied
order and runs its actions
according to the read options. To enforce an order of execution, you have to use the option
-then:
ingly,
of
then
Frama-C parses its command line until the option
-then
and runs its actions accord-
it parses its command line from this option to the end (or to the next occurrence
-then) and runs its actions according to the read options.
Note that this second run starts
with the results of the rst one.
Consider for instance the following command.
$
frama
-c - val - ulevel 4 file .c - t h e n - ulevel 5
It rst runs the value analysis plug-in (option
-ulevel,
Section 5.3).
-val,
[7]) with an unrolling level of 4 (option
Then it re-runs the value analysis plug-in (option
-val
is still set)
with an unrolling level of 5.
It is also possible to specify a project (see Section 8.1) on which the actions applied thanks
to the option
$
frama
-then-on.
Consider for instance the following command.
-c - semantic - const - fold main file .c - t h e n - on propagated - val
main of file.c (option -semantic-const-fold)
propagated. Then it runs the value analysis plug-in on
It rst propagates constants in function
which generates a new project called
this new project.
3.3.2 Getting Help
The options of the Frama-C kernel,
i.e.
printed out through either the option
those which are not specic to any plug-in, can be
-kernel-help
19
or
-kernel-h.