Spare code plug-in

The Spare code plug-in helps in removing unnecessary code in a program.

Usage

The plug-in can be invoked through the command line using the options :

-sparecode-analysis
Removes statements and functions that are not useful to compute the result of the program.
-rm-unused-globals
Removes unused types and global variables.

Behavior

The Spare code plug-in produces an output program which is guaranteed to be compilable C code, and to have the same behavior as the analyzed program from the point of view of the values assigned to the output variables of the main function.

By default, the reachable ACSL annotations are preserved, and the statements that are necessary to compute the values of the program variables used in these annotations are retained. This behavior can be toggled off using the -sparecode-no-annot option.

To prevent elimination of some statements, slicing pragmas can be inserted into the source code. The syntax of these 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.

Known restrictions

Only the annotations found inside the body of a function (e.g. assertions) are processed at the moment. Function specifications such as pre and post-conditions are not taken into account, and are omitted from the resulting program.

Dependencies

This plug-in uses the results of the Value analysis plug-in and of the function dependencies computation (documented together with the value analysis).