Slicing plug-in

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).