If the Frama-C kernel is the heart of the platform, the Graphical User Interface (GUI) is its head: it enables exploring the 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.

Architecture

The Frama-C GUI is implemented in OCaml, using a GTK-based graphical framework (lablgtk) written in OCaml.

It is implemented as a plug-in, albeit a special one; it is enabled by running a different binary than the command line Frama-C.

AST Code Browsing

The most basic usage of the Frama-C GUI consists in providing a navigable view of the source code. The Frama-C kernel, after preprocessing and normalizing the code, produces an internal representation (called an Abstract Syntax Tree, AST for short) which is slightly different from the original source code. The Frama-C GUI displays both versions side-to-side, as in the screenshot below.

The internal code representation seen by Frama-C, often called normalized code, or CIL code (see Kernel for details), is presented in the left panel, which is typically in the center of the graphical interface. The original code is presented in the right.

This simple, hello world!-style code allows us to see some operations performed by Frama-C:

• Code normalization: loop normalization, a single return point per function, pointer dereferencing (e.g. i[s] becomes *(s+i));
• Implicit conversions are made explicit (e.g. the string literal of type const char * is cast to char *).
• Code understanding: selecting an expression in the GUI (highlighted in green in the above screenshot) displays its syntatic properties (Information tab) and the corresponding line in the source code.

Plug-in Integration

Many Frama-C plug-ins are integrated into the GUI: they add panels, controls and displays, to bring useful information to the user in the most efficient way possible.

In the screenshot above, we see, on the left, the file tree panel, which displays the list of globals (functions and variables) in the program. In this case, the Metrics and Eva plug-ins were enabled, and the file tree display includes three extra columns: percentage of dead code, number of dead statements, and total number of statements per function.

The user can sort by any of these columns, and a right-click enables a series of filters on them. Ctrl+F enables textual search. Unreachable function names are crossed out.

All of this information can be obtained via reports and in textual form, but their tight integration in the GUI greatly increases productivity and the semantic understanding of a code base. The screenshot below showcases several plug-ins having graphical components integrated into the GUI.

Parametrization of Analyses

The Frama-C GUI allows parametrizing and re-running analyses.

Deep Semantic Analysis

Besides the syntactic facilities, the Frama-C GUI is especially useful to handle the semantic properties which are the specialty of the Frama-C framework.

All properties of interest (runtime errors, function contracts, etc.) are displayed in the GUI as ACSL annotations interspersed with the code, with colored markers indicating their current status in the platform (valid, invalid, unknown, no proof attempted, etc.). A filterable list allows inspecting them and quickly navigating the code to find the points of interest.

In the example above, the original code contained a call to a COPY macro, which in fact calls the library function memcpy. That function, along with several others in the standard C library, has an ACSL specification provided by the Frama-C team. That specification establishes some properties which must be verified to ensure the absence of runtime errors (e.g., the destination must point to valid memory). These properties are displayed by the GUI at the point where they must be verified. They have a green circle next to them, indicating that at least one Frama-C plug-in was able to prove them.

Conversely, the yellow circle before the if, at the beginning of the function, indicates that a plug-in (Eva, in this case) attempted to prove the property but was unable to; another plug-in may try it and update the status accordingly.

Technical Notes

• The GUI is not an editor; it allows code inspection and navigation, including to the original source (e.g. Ctrl+clicking the original source), but not live-editing.
• Initial source preparation and parsing (before obtaining a valid AST) is more suitable for the command-line Frama-C interface. Frama-C’s session mechanism allows loading the result to combine it with other analyses and displaying the result in the GUI.