The Occurrence plugin is integrated with the Frama-C kernel:
The Occurrence module aims at highlighting the occurrence of any variable in the Frama-C GUI. Details about the use of this plugin may be found in the user documentation.
The code of this plug-in is quite simple. It is splitted into the analysis itself and the extension to the GUI.
The code of this plug-in is quite short but uses most advanced Frama-C
features (visitor, projects, journalisation, log, gui). So it is a good
complete not-toy example of a (kernel-integrated) Frama-C plug-in.