--- layout: plugin title: Spare code description: Removes "spare code", code that does not contribute to the final results of the program. key: code ---
The plug-in can be invoked through the command line using the options :
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:
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.
This plug-in uses the results of the Value analysis plug-in and of the function dependencies computation (documented together with the value analysis).