---
layout: plugin
title: Slicing
description: This plug-in slices the code according to a user-provided criterion.
key: code
---
- 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.
- Slicing criteria for code observation
-
The slicing criterion can be specified with one or several
command-line option. Each of the following options specify 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 observation are the
following:
- -slice-calls f1,...,fn
- Selects every call to the functions f1,...,fn, and all
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
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 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 the value
analysis) 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 do not affect the slicing result.
The behavior of the Slicing plug-in is controlled by the
following options:
- -slice-print
- This option is now deprecated. Since [Carbon 20101001], the nominal way to print the
resulting AST is:
<normal slicing command> -then-on 'Slicing export'
-print.
If you want to redirect the output into a file, adds
-ocode option:
<normal slicing command> -then-on 'Slicing export' -print
-ocode <output file>.
- -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: |
doesn't slice the called functions, |
1: |
allows slicing of the called functions, but doesn't perform
specialization of these functions, |
2: |
allows slicing and specialization of the called functions, but
at most one slice/specialization by function, |
3: |
allows several slice/specializations by 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 Value
analysis plug-in and of the function dependencies computation
(documented with the value analysis).