Notice that the window mentions in which panel the search will be performed. Also, the search is case-sensitive.
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:
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.
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):
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.
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.
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
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.
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!André Maroneze