Astrée release 16.04

Astrée screenshot

Improved side bar

The project side bar has been re-arranged to improve usability.

  • The sections Local Settings and Server Settings have been replaced by a Confi­guration section, with the subsections Preprocessor, Parser, Analyzer, and Annotations.
  • The new Results section contains the new Findings view that replaces the old Result Viewer.
  • The preprocessed file list now automatically shows the list of functions in the currently displayed file for faster navigation.
  • The wrapper-and-stubs file and the analysis entry point are now configured by the new analyzer options config-file=filename and analysis-entry=function-name, respectively. The configured wrapper-and-stubs file appears at the beginning of the preprocessed files list.
  • The Wrapper Generator and Model Link settings have moved to the Tools menu.

The new Project Summary area provides more information than before, listing the totals for:

  • Errors
  • Run-time errors
  • Data-flow anomalies
  • Rule violations
  • Data races
  • Reached code
  • Analysis duration

The traffic lights are now displayed horizontally to better accomodate the more detailed Summary.


Astrée screenshot

Improved result views

  • The new Results area comprises interactive tabular and graphical overviews for Findings per category, Findings per file/function, Rule violations, Reachability, Code metrics, and Data and control flow information.
  • For faster access of individual results, the single button Show results has been replaced by five buttons: Output, Findings, Not reached, Watch, and Search.
  • A new Findings view replaces the former Result Viewer. All run-time errors and MISRA-C violations are listed here, and can be classified or commented on. The view can be filtered by various criteria, such as the type of findings or a certain code line selected from the editor view. Thus, this view also replaces the former Line Summary view.
  • Variables with race conditions are marked in the Data flow tab. The Findings view can be filtered to display all alarms about race conditions related to a particular variable.
  • A new Not Reached view displays all code locations that have not been reached by the analyzer.
  • The lists in the Findings and Not Reached views can be filtered in the Results overview and exported as CSV files to create custom reports.
Screenshot

Code metrics

Screenshot

Reachability stats

Screenshot

Data races

Astrée screenshot

Program slicer

The new inter-procedural program slicer computes a reduced version of the analyzed code that contains all statements on which the value of a certain variable at a certain program point depends.

The program point and variable to slice for are selected by invoking “Slice from here” from the context menu in the editor view.

The computed program slice can then be investigated in Astrée or stored as a C source file.