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.

Quick Start

frama-c-gui -eva studia.c

Right-click on an expression in the code and choose the Studia context menu to access its features.

Studia plug-in screenshot

You can use the example code below to test its features.

Example code

#include <string.h>
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) {

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

  • Maturity: industrialized

  • Automatically enabled after running Eva and opening the GUI.