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 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
-slice-value v1,...,vn: Selects the result of left-values
v1,...,vnat the end of the function given as entry point.
-slice-wr v1,...,vn: Selects the write accesses to left-values
-slice-rd v1,...,vn: Selects the read accesses to left-values
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,...,fnas 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
eat 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
-slice-loop-inv f1,...,fn: Selects the loop invariants of functions
-slice-loop-var f1,...,fn: Selects the loop variants of functions
-slice-threat f1,...,fn: Selects the threats (emitted by Eva) of functions
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-leveloption 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
- 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-functionsoption 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).
This plug-in uses the results of the Eva plug-in and of the function dependencies computation (documented with Eva).