Newer
Older
Andre Maroneze
committed
---
layout: plugin
title: Slicing
description: Slices the code according to user-provided criteria.
key: code
additional:
- name: "Documentation"
link: /download/frama-c-slicing-documentation-french.pdf
lang: FR
- name: "PDG Documentation"
link: /download/frama-c-pdg-documentation-french.pdf
lang: FR
Andre Maroneze
committed
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
distrib_mode: main
---
## Overview
The **Slicing** plug-in produces an output program which is made of a subset of
the statements of the analyzed program, in the same order as in the analyzed
program. The statements are selected according to a user-provided
*slicing criterion*. The output program is guaranteed to be compilable C code,
and to have the same behavior as the analyzed program from the point of view of
the provided slicing criterion.
## Usage
### Slicing criteria for code observation
The slicing criteria can be specified with one or several command-line options.
Each of the options described below specifies an observable element to be
preserved in the resulting code. For instance, with the option
`-slice-return f`, the plug-in ensures that, each time the function `f`
terminates in the original code, it terminates in the sliced code, and that the
returned value is the same in both cases. Slicing criteria related to code
observations are the following:
- `-slice-calls f1,...,fn`: Selects every call to the functions `f1,...,fn`,
and all of their effects.
- `-slice-return f1,...,fn`: Selects the result (returned value) of functions
`f1,...,fn`.
- `-slice-value v1,...,vn`: Selects the result of left-values `v1,...,vn`
at the end of the function given as entry point.
- `-slice-wr v1,...,vn`: Selects the write accesses to left-values `v1,...,vn`.
- `-slice-rd v1,...,vn`: Selects the read accesses to left-values `v1,...,vn`.
The slicing criterion can also be specified into the source code using
*slicing pragmas* and the following command line option:
- `-slice-pragma f1,...,fn`: Uses the slicing pragmas in the code of functions
`f1,...,fn` as slicing criteria.
The syntax of slicing pragmas is as follows:
- `/*@ slice pragma ctrl; */`: Preserves the reachability of this control-flow
point.
- `/*@ slice pragma expr e; */`: Preserves the value of the [ACSL](acsl.html)
expression `e` at this control-flow point.
- `/*@ slice pragma stmt; */`: Preserves the effects of the next statement.
### Slicing criteria for proving properties
The slicing criterion can also be relative to [ACSL](acsl.html) annotations.
In this case, the **Slicing** plug-in ensures that if a property is verified by
the sliced code, it implies that the corresponding property is satisfied by the
initial code. The command-line options related to that feature are:
- `-slice-assert f1,...,fn`: Selects the assertions of functions `f1,...,fn`.
- `-slice-loop-inv f1,...,fn`: Selects the loop invariants of functions
`f1,...,fn`.
- `-slice-loop-var f1,...,fn`: Selects the loop variants of functions
`f1,...,fn`.
- `-slice-threat f1,...,fn`: Selects the threats (emitted by [Eva](eva.html))
of functions `f1,...,fn`.
### Slicing options
Several of the above options can be used simulaneously to specify an intricate
slicing criterion. Note that the order of the options does not affect the
slicing result. The behavior of the **Slicing** plug-in is controlled by the
following options:
- `-slice-undef-functions`: Allows the use of the `-slicing-level` option for
calls to undefined functions, *i.e.* for function prototypes (by default,
prototypes of undefined functions are never specialized).
- `-slicing-level n`: Sets the level of slicing/specialization used for
function calls. The possible values for `n` are:
- 0: does not slice the called functions;
- 1: allows slicing of the called functions, but does not perform
specialization of these functions;
- 2: allows slicing and specialization of the called functions, but at most
one slice/specialization per function;
- 3: allows several slice/specializations per function.
The default value is 2. Except when `-slice-undef-functions` option is set,
undefined functions are never specialized.
- `-slicing-keep-annotations`: Keeps annotations as long as the used variables
are declared and the accessibility of the program point is preserved (even if
the value of the data is not preserved).
## Dependencies
This plug-in uses the results of the [Eva](eva.html) plug-in and of the
function dependencies computation (documented with Eva).
## Further Reading
- The **Slicing** plug-in has some
[documentation (in French only)](/download/frama-c-slicing-documentation-french.pdf)
based on a technical report, but no user manual _per se_.
- The **Slicing** plug-in is based on another plug-in, **PDG**
(for *Program Dependence Graph). It also has some
[documentation (in French only)](/download/frama-c-pdg-documentation-french.pdf)
based on a technical report.