Download User Manual - Frama-C

3.3.
FRAMA-C COMMAND LINE AND GENERAL OPTIONS
batch version can be made to launch the value analysis on the
frama-c -val foo.c.
interactively, the command
on the le
foo.c
foo.c
le with the command
Although the GUI allows to select les and to launch the value analysis
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
value
must be used when
starts with a minus sign.
Most parameterless options have an opposite option, often written by prexing the option
-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
no-.
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
accordingly to the read options.
option
-then:
then
accordingly,
occurrence of
unspecied
order and runs its actions
To enforce an order of execution, you have to use the
Frama-C parses its command line until the option
-then
and runs its actions
it parses its command line from this option to the end (or to the next
-then)
and runs its actions accordingly 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,
[5]) 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
or
-kernel-h.
The options of a plug-in are displayed by using either the option
or
-<plug-in shortname>-h.
Furthermore, either the option
-help
or
-h
or
short names.
19
--help
-<plug-in shortname>-help
lists all available plug-ins and their