Studia

Overview

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.

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) {
    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

• Maturity: industrialized

• Automatically enabled after running Eva and opening the GUI.