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:
i[s]
becomes *(s+i)
);const char *
is cast to char *
).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.
The Frama-C GUI allows parametrizing and re-running analyses.
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.