Occurrence analysis


The Occurrence analysis plug-in shows the uses of a variable in a C program. This analysis highlights the left-values that may access the selected variable. As shown by the example, the analysis takes aliases into account.

It is available through a contextual menu at each variable in the Frama-C graphical user interface. Invoking this analysis on a variable displays the occurrences of this variable in the program:

Screenshot of Occurrence in the GUI


The plug-in can be used both with the graphical user interface and in batch mode. In batch mode, the command is:

frama-c -occurrence file1.c file2.c

This prints all occurrences of each variable to the standard output.


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