Plugins Kernel Specification Ivette (GUI)

Ivette: a Graphical User Interface for Frama-C

Several screenshots of Ivette stacked

Ivette is the Graphical User Interface (GUI) of Frama-C. It enables exploring code, augmented with several navigation tools and highlighting modes; it allows launching, parametrizing and visualizing analyses; and it allows combining them seamlessly, taking full advantage of the multi-paradigm approach.

Quickstart

The executable ivette can be used instead of frama-c when running an anlysis to display the results inside Ivette. For instance, to run an anlysis on a source file file.c with the Eva plug-in and display its results in the GUI: ivette file.c -eva -eva-precision 5. The GUI can also be run independently of any analysis by running ivette without any arguments.

The internal documentation of Ivette is available through the menu “Help > Documentation”, and each component’s help is available through the “?” icon in the component’s titlebar.

Ivette works independently from Frama-C and interacts with a Frama-C server to run analyses and retrieve results. As a result some controls are available in the GUI to monitor the state of the server and start or stop analyses.

Overview

A screenshot of Ivette with the different parts of the UI annotated

The main window of Ivette consists of several components:

  1. The menu bar organizes the highest-level functions of the tool into structured categories. Among other features, the “File” menu can be used to save or load a Frama-C session, or the “Help” menu can be used to open the internal documentation.
  2. The sidebars can be used to navigate between the different views and plug-ins of the platform. The large icons on the left-most side of the screen switch which sidebar is displayed.
  3. The toolbar provides shortcuts to selected views and frequently used actions.
  4. The status bar displays general feedback on currently running tasks and the list of docked components.
  5. The laboratory central area is where the different views and Frama-C components are displayed. It consists of one to four panels that can be arranged as needed.

Documentation

The full documentation of Ivette is accessible directly from the tool by opening the menu “Help” and selecting “Documentation”.

Some use-cases on how to use Ivette to conduct analyses are also available in Frama-C’s user manual and Eva’s user manual, depending on which plug-in you intend to use.

Architecture

The technical stack we have chosen consists of the following frameworks:

  • A GUI desktop application using the HTML5 and NodeJS JavaScript runtime engine of the Electron platform.
  • A GUI code base written in TypeScript with the Reactive Programming framework ReactJS.
  • A Frama-C/Server plug-in written in OCaml, that provides an asynchronous, JSON-based, strongly typed Request System.
  • Each Frama-C plug-in will then register new requests in the Server plug-in, independently of any communication protocol with any external User Environment.
  • A collection of middlewares and protocols written in different languages to specifically connect the Frama-C/Server plug-in and the ReactJS code with each other.

The GUI code itself is entirely written in TypeScript and is split into three parts:

  • The Dome framework, which is a collection of carefully designed and themed high-level components, offering a predefined choice of features.
  • The Ivette framework, which is an application built with Electron and Dome featuring the main GUI environment and managing the connection with Frama-C.
  • The Frama-C plug-in components for Ivette are built from Dome components and interact with the Frama-C static analyzer plug-ins.

More details can be found in this article.