Impact analysis

Overview

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.

Usage

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

Dependencies

This plug-in depends on results of the Eva plug-in.