Small improvements to the Frama-C GUI

The Frama-C GUI received a few quality-of-life improvements that have not been announced during the Magnesium release. This post presents some of them, along with general GUI tips.

We focus on general-purpose UI improvements, while another post will discuss new Value-specific features, related to the new Values tab.

These UI features should be discoverable via menus or other signifiers in the UI, but we decided to keep them hidden until stabilization, to avoid breaking existing workflows in case we decided to remove them. They are still not 100% mature, but since we have been pleasantly using them for several months, we feel confident enough to disclose their existence.

The features mentioned here are:

• textual search;
• message/property counters;
• types in the Information tab;
• property filters;
• reverse source mapping.

Textual search

It is now possible to perform a textual search in most Frama-C panels using Ctrl+F. Here is the list of panels where this works:

• List of globals (upper-left panel, which displays filenames and global definitions);
• CIL code (central panel);
• Original source code (upper-right panel);
• Information tab (lower panel);
• Console tab (lower panel).

When you press Ctrl+F, the currently focused panel will display a small search window (if it accepts textual search) like this one:

Notice that the window mentions in which panel the search will be performed. Also, the search is case-sensitive.

Click on Find to search for the string. You can type F3 to perform a “Repeat search”, that is, advance to the next occurrence of the text without opening a new panel. If you reach the end of the text, this dialog will notify you:

Also, if the search text is not found, you’ll be presented a different dialog:

Message/Property counters

The Messages and Properties tabs now display the total amount of items they contain. This summary is useful for a quick comparison between short analyses. The Messages tab always display the amount of items, while the Properties tab, because of its “lazy” nature (items are only updated after clicking the Refresh button), initially does not display anything, but after selecting the set of desired filters, the Refresh button will update the total count, as illustrated in the figures below (click on the orange circles to switch images).

• 
• 
• 
• 
• 
• 

​

Note that the font in the Refresh button becomes bold to indicate that an update is needed, and returns to normal afterwards.

Types in the Information tab

The Information tab has been modified to include some typing information about variables, as shown in the example below.

In the example, the user clicked on the res expression, which displays some information (rectangle 1) such as the current function, statement id (used internally), source code line (with a clickable link to focus it in the original source panel), the type of the variable (with a clickable link), and some extra details.

By clicking on the variable type, we obtain more information (rectangle 2):

• sizeof;
• Source code line where the type is defined (if it is not a predefined type), with a clickable link;
• Expanded type information (in the case of composite types). If a field is defined via yet another composite type, a link to the type information of that type will also be displayed.

This is very useful when exploring new code bases.

Note that some information that was previously displayed in this tab (e.g. the results computed by the Value plug-in) has been moved to the Values tab, which will be described in a later post.

Property filters and filtersets

One common issue for new users is to properly set the filters in the Properties tab, to avoid displaying too much information. Advanced users also had some difficulties defining a precise set of filters that matched their needs.

To help both kinds of users, the Properties tab had two minor improvements: first, some filter categories were defined (Kind, Status, RTE-related), to allow folding/unfolding of sets of filters.

Second, a few recommended filter sets were defined, corresponding to the most often used filter combinations. A small “Filter” button (a pointing hand clicking on a square) has been added next to the Refresh button, as indicated in the screenshot below:

The “Reset all filters to default” menu consists in:

• Hiding properties with status Considered valid, Untried or Dead;

• Hiding statuses that are useful only in some specific situations: this includes Behaviors, Axiomatic and Reachable.

These statuses are not included by default for two reasons: Axiomatic and Behaviors are redundant w.r.t. the contents of other filters, while Reachable properties such as the ones produced by Value may generate noise, e.g. dead code detected by Value may show up as “Reachable Invalid” status (i.e. “unreachable”)¸ when its actual consolidated status is Valid but dead.

In most circumstances, these properties are not relevant for an analysis of potential alarms. Filtering them by default reduces noise, but it is still possible to select them when necessary.

A more restrictive view can be obtained by selecting the menu “Reset ‘Status’ filters to show only unproven/invalid”. This further eliminates Valid and Valid under hypotheses, leaving only orange/red bullets, which are often the only ones we are interested in.

Note that the Current function filter is independent of these buttons.

(Approximate) mapping from original to CIL source

A much-requested functionality is the mapping from the original source (right panel) to the CIL code, to synchronize the views of both panels.

Before Magnesium, clicking on the original source code did not move the cursor on the CIL code. Now, an approximate mapping allows the user to click on the original source and have the CIL source scrolled to the approximate corresponding location, as in the example below, in which the user clicked on the macro IEEE_1180_1990_ABS.

Note that this feature is not 100% reliable because the mapping between both sources is not always invertible. For instance, consider syntactic unrolling of loops, or multiple expansion of macros. In some cases the mapping fails (no location is found) or moves the CIL code to a distant part; e.g. some parts of expressions, when clicked, scroll to the variable declaration instead. Also, static variables and macro definitions are particularly problematic. But overall, this feature is a net benefit, especially when trying to find a specific location in a large function. If you find unintuitive behaviors, do not hesitate to tell us; there may be some patterns which have not yet been considered.

Tip: In some cases, different parts of an expression give different results, so it may be worth trying a few nearby clicks.

Conclusion

Each modification to the Frama-C GUI in itself is a minor, almost imperceptible improvement, but together these features greatly contribute to our comfort and productivity when using the GUI. We hope you’ll enjoy using them as well!