Slicing

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 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 Eva) 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 plug-in and of the function dependencies computation (documented with Eva).