Impact analysis plug-in
The Impact analysis plug-in allows the automatic computation of the set of statements impacted by the side effects of a statement of a C program. Statements not appearing in this set are guaranteed not to be impacted by the selected statement.
Impact analysis is available through a contextual menu at each statement in the Frama-C graphical user interface. Invoking this analysis on a statement displays the impact of the statement on the rest of the program.
The plug-in can be used both with the graphical user interface and in batch mode. In batch mode, you must put pragmas on the statements you want to analyze:
/*@ impact pragma stmt; */
Then, the following command line computes the impact from the pragma statements in the code of functions f1,...,fn:
frama-c -impact-pragma f1,...,fn file1.c file2.c
To print the list of impacted statements on the standard output:
frama-c -impact-print file1.c file2.c
This plug-in depends on results of the Value analysis plug-in.