Download User Manual - Frama-C

Chapter 8
General Kernel Services
This chapter presents some important services oered by the Frama-C platform.
8.1 Projects
A Frama-C project groups together one source code with the states (parameters, results,
of the Frama-C kernel and analyzers.
current
etc
)
In one Frama-C session, several projects may exist at the same time, while there is always one
and only one so-called
project in which analyses are performed. Thus projects help
to structure a code analysis session into well-dened entities. For instance, it is possible to
perform an analysis on the same code with dierent parameters and to compare the obtained
results. It is also possible to extract a program
the results of an analysis run separately on
p
p0
from an initial program
p
and to compare
0
and p .
8.1.1 Creating Projects
A new project is created in the following cases:
•
at initialization time, a default project is created; or
•
via
•
a source code transforming analysis has been made. The analyzer then creates a new
an explicit user action in the GUI; or
project based on the original project and containing the modied source code. A typical
example is code slicing which tries to simplify a program by preserving a specied
behaviour.
8.1.2 Using Projects
The list of existing projects of a given session is visible in the graphical mode through the
Project
etc
menu (see Section 9.2).
removing, saving,
the same session.
Among other actions on projects (duplicating, renaming,
), this menu allows the user to switch between dierent projects during
In batch mode, the only way to handle a multi-project session is through the command line
option
-then-on
(see Section 3.3.1).
37