Added full support for C file scope rules.
It is now possible to analyze programs in which
different global variables and types have identical
names in different C source files.
Added support for line directives of the form “#line <num> <string>”.
Server
The Astrée server can now be started as a Windows service,
making it independent from user sessions.
Improved the synchronization of multiple clients that access
the same analysis project on the same server.
GUI
New Astrée icon.
Increased speed and reduced memory consumption when handling large analyzer logs.
All long running operations can now be aborted by the user.
The preprocessed source code that is analyzed on the server can now be downloaded
into a local directory on a client machine. The downloaded files can also be synchronized
with the server files.
Astrée is now shipped with several pre-configured ABIs
which can be loaded in the “ABI” view.
Reorganization of the analysis results views:
Removed the separate views “Errors”, “Alarms”, and “Warnings”.
This information can now be found under “Output”.
Display the call graph using the aiSee graph viewer.
The graph can be used for navigating the sources. It also comprises statistical
information about the distribution of alarms. See screenshot.
Reorganization of the Output area:
“Output” window renamed into “Log”.
Extended the “Summary” window. It is now possible
to view alarms, errors, and coverage statistics per file, as well as
alarms and errors grouped by categories. See screenshot.
Improved the precision of coverage information. Lines outside
of functions are no longer taken into account.
Added a navigation panel to the “Log” and “Summary” windows,
enabling easy navigation through alarms and errors.
Added a separate “Warnings” window which collects all warning messages.
Added new “Messages” window to display and navigate all analyzer messages
for a code location that has been selected in the editor view.
Project browser:
Added new status area below the left-hand menu. It provides stats
about the analysis results including errors, alarms, warnings, coverage,
and analysis time. A traffic light summarizes the analysis stats,
enabling a quick assessment of the analysis results. See screenshot.
Interactive result exploration:
Astrée now also exports invariants at the end points of blocks and functions.
The exported invariants can be displayed in the “Watch” window.
Loop contexts in the “Watch” window are now sorted in the order
of loop iterations.
Exported invariants are now also displayed as tooltips in the editor.
The displayed invariants hold for all contexts. See screenshot.
Editor:
Non-analyzed code is always colored automatically. See screenshot.
Added syntax highlighting and auto-completion for analysis directives.
