Frama-C 25 includes a preview version of Ivette, the new Frama-C GUI

The Frama-C GUI, based on GTK, is undergoing a retirement process; Ivette, the new graphical interface, will replace it in a few versions. The first public preview of Ivette has shipped with Frama-C 25.0 (Manganese). This post will briefly present how to compile and run it. It also illustrates some features with screenshots.

Compiling Ivette from the Frama-C source archive

This preview release of Ivette is present in the .tar.gz archive of the Frama-C 25.0 (Manganese) release, but it is not installed via the opam package. After installing Frama-C (either via opam or by manually compiling the sources via ./configure && make -j && make install), you need to download the Frama-C archive and install Ivette. The recommended way to do so on most Linux distributions is:

1. Install node 16 and yarn:

    curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.34.0/install.sh | bash
    nvm install 16 && nvm use 16
    npm install yarn

2. Install Ivette from the root directory of the Frama-C sources:

    ./configure && make -C ivette dist
    [sudo] make -C ivette install

The above instructions, and some variations for different distributions and OSes, are available in ivette/INSTALL.md. For a more detailed explanation of the above steps, and to help with troubleshooting, we provide the instructions below (tested on a Ubuntu 22.04):

• Install a recent version of Node.js, such as 16.x.x. Note that, even on recent Ubuntus (such as 22.04), if you install it via apt (e.g. apt install nodejs), you will get a relatively old version such as 12. The Node.js website has some recommendations on how to install a more recent version, either by downloading a binary, or using tools such as nvm (Node Version Manager). In any case, at the end you should be able to run node --version and get something similar to v16.13.0.
• After the previous step, install the Yarn package manager, via npm install -g yarn. Warning: there is a yarn package on Debian/Ubuntu that can be installed via apt, but it has nothing to do with the yarnpkg package, which is the one we want. Do not install any of them: the first one is useless for Ivette, and the other depends on old Node.js packages. This is why we recommend the npm-based method.
• You will likely have to restart the terminal after running the previous command.
• Go to the subdirectory ivette. You can finally run make dist to compile Ivette and produce a binary distribution, which can then be installed via make install (sudo may be needed at this step). If you prefer not to install it, you can run the ivette script from the bin directory, that is, ivette/bin/ivette from the toplevel directory containing the Frama-C source code.

Running Ivette

Ivette is an Electron-based application. When run, it starts a Frama-C process (forwarding command-line options if needed) with the Server plugin, which communicates requests back and forth from the Electron interface.

Ivette’s interface is currently based on views. They allow switching between tasks, such as navigating the source code, viewing alarms, using pivot tables, etc. Each view is an arrangement of one or more Components. The user can add, modify or remove components from any view.

The screenshot below presents the high-level parts of Ivette:

The central area of the interface is entirely defined by the current view; in the above screenshot, it contains a view similar to the one from the traditional Frama-C GUI: the CIL (normalized) source on the left, the original source code on the right, and the bottom panel with the list of properties.

However, if we click on a different view, such as Eva Summary, then all of these components are replaced with a different set of windows. Compared to the old GUI, this offers much more versatility, without having to use “dialog”-like windows, such as the old callgraph. Components are usually aware of each other: clicking on a location in a component will update others to match it.

Coming back to the overview: on the top left corner we have a few buttons which control the server, that is, the status of the Server plugin of the underlying Frama-C process. Hovering on a button displays its function. The most useful buttons in this corner are “Previous location” and “Next location”, which serve the same purpose as the “History” buttons in the old GUI: they allow going back and forth between parts of the source code.

The left corner of the screen is used by the Functions list, similar to the Globals view of the old GUI. It also includes a button to configure some filters (e.g. hiding standard library functions).

The top right corner of the GUI contains a few buttons: two for zooming (currently, they only affect the font size from the source code components, but they will allow general scaling of the interface in the future), and a search bar, which appears when you hover on the magnifying glass icon: it allows searching functions by name.

Finally, on the right hand corner of the screen, we have the Views and Components. As mentioned before, Views are simply an arrangement of components; you can customize them as you wish. You can duplicate an existing view to use it as a base configuration, rename it, and re-arrange the components as you prefer. Note that the original views cannot be erased (indicated by the “closed padlock” icon next to them).

Each Component is provided by the Frama-C Kernel or by a plugin. Components already displayed are grayed out (you cannot have two copies of a component). To add a component, drag and drop it into the main view.

Ivette is currently for Eva; WP and others will follow later

The current preview version of Ivette is focused on the Eva plugin and its derivatives (such as Dive). In this section, we present some of its features.

The Eva Summary view is useful for an overview of the analysis, including number of alarms, code coverage per function, and the messages emitted during the analysis.

You can combine components from the Eva Summary view with the AST, so that clicking on them will show the relevant source code. You can also switch views after clicking on a location/message; the new components will remember which location was selected.

The Eva Values view offers the value inspection capabilities which are Eva’s trademark. There are some significant differences w.r.t. the old GUI; for instance, when selecting an if expression, the Eva Values component will show three states: the one before the branch, the one after the then branch, and the state after the else branch, as in the screenshot below.

Another new feature is that, when there are several callstacks, Ivette can show them in a breadcrumb navigation-style widget; the screenshot below shows an example. Note that, in order to show per-callstack values, you need to click the Show values by callstack button in the Eva Values component (see screenshot below), and then click on the callstack of interest. The navigation widget at the bottom shows the name of the callers, as well as the location of the call. If you hover on the location, a tooltip displays the statement itself. Finally, clicking the node navigates to that statement. You can navigate back by clicking the Previous location button in the top left corner of Ivette.

If nothing is shown, look for errors in the Console view

Currently, Ivette does not display a modal dialog in case of errors, like the old GUI. Instead, it is a bit too subtle in such cases. If you only see blank components (especially the AST and source code), consider switching to the Console view to see if there are any error messages explaining what happened.

You can also use the Console component to change the Frama-C command line: it has a button in the top right corner that switches to an editable command line, where you can add/remove options given to Frama-C. It includes a play button that will re-run Frama-C with the new command-line options. This will evolve in time towards a more ergonomic interface, but for now, it replaces the Analysis panel of the GTK-based GUI.

Conclusion

Ivette, the new Frama-C GUI, will allow us to modernize and evolve the graphical interface towards novel kinds of interactions and visualizations that will help understand the code, the alarms, and the proofs. It is currently in a preview state, but it already offers new features, especially for Eva. The traditional GTK-based GUI is still the default one, but it will be retired in a few Frama-C releases. Feedback is welcome, be it to suggest new features, request old features to be preserved, or report issues.