Spare code

Overview

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.

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.

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.

Technical Notes

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