The Slicing plugin is integrated with the Frama-C kernel:
To have more details about what we are trying to do, you may have a look to the specification report (in French).
The internal types module (SlicingTypes.Internals
)
can give a pretty good idea of the kind of objects that we deal with in this
module.
You can also find some general information below.
The project was the global repository of the results obtained so far. If is mainly composed of a list of actions waiting to be applied, and the already computed slices.
More precisely, see its type definition
SlicingTypes.Internals.t_project
if you want to know what it is composed of,
and the module SlicingProject
of the functions to handle it.
This computation is not part of this module anymore. See the API of Pdg module.
It is enough to know that the PDG of a function is a graph composed of nodes that represent the elements of a function (declarations, statements, and so on) and of edges that represent the dependencies relations between those elements.
A sliced function contains a mapping between the PDG nodes of a function and the some marks that are computed by the application of the actions. It also has a mapping between the function calls and the function called by the slice that can be either some other slices, or the source function (or nothing if the call is invisible in that slice).
There can be more than one slice for a source function.
See their type SlicingTypes.Internals.t_fct_slice
,
and the associated functions in Fct_slice
.
See also SlicingMarks
for more information about the low level marks computation.
The actions are the way of giving an order to modify the current application.
There are many kinds of actions, but only one is really used to build the slice which is a list of nodes from the PDG of a function, and their associated marks. All the other actions dealing with the marks are first decomposed before being applied.
Some other actions are can be used to manage the interprocedural part, ie. which slice to call where.
See the top type SlicingTypes.Internals.t_criterion
or
the functions in SlicingActions
.
The propagation of the marks to the function call depend on a
SlicingTypes.Internals.t_call_option
.
Chosing this level makes it possible to obtain a more or less precise result.
The module SlicingCmds
is a bit external because it only uses
the slicing API to define higher level function
that are only a composition of the basic functions.
When there are non more actions in the task list,
the project can be exported. This is done in
SlicingTransform
module
by building a new CIL application.