Plugins
Studia
- Studia, for case studies
-
The Studia plug-in helps tracking the origin of alarms reported by EVA, adding useful shortcuts in the Frama-C GUI for navigation between an expression and its uses/definitions.
Maturity: Mature
- Quick Start
-
$ frama-c-gui -val studia.c
Right-click on an expression in the code and choose the Studia context menu to access its features.
Use the example code below.
- Example
-
#include typedef struct { int id; char msg[16]; } person; void disable(person *p) { if (p->id == 2) strcat(p->msg, "_disabled"); } void set_state(person *p, int on) { if (p->id > 0 && !on) { disable(p); } } void main() { person p = {2, "john_doe"}; set_state(&p, 0); }
Other plug-ins derived from EVA, such as Impact, Occurrence and Scope, also include menus in the GUI which complement Studia.
- Technical Notes
-
Automatically enabled after running EVA and opening the GUI.