Astrée release 10.12

New preprocessor support

It is now possible to specify a list of original source files and preprocessor settings. The specified files can be automatically preprocessed and analyzed by Astrée using a built-in preprocessor. The installation also includes a sample C library implementation that uses Astrée directives for stubbing frequently used functions.

New project wizard

When creating a new project, a wizard dialog now guides you through the basic analysis set­tings and provides online help for each of the configured options.

New call graph browser

The new browser provides a better overview of the alarm distribution in the analyzed software. It enables viewing only the relevant program parts and investigating modules indi­vidually.

New XML reports

Analysis results can be exported in XML format. The XML reports comprise:

  • a summary of the analysis results;
  • a list of all error and alarm messages including location information in preprocessed and original source code;
  • detailed coverage information for all analyzed source files.

The generated XML reports can be displayed in a web browser or imported into Microsoft Excel and Word using the included XSLT stylesheet.

New batch mode option --files

When running in batch mode, the Astrée client recognizes the new option

--files <file list>

Before running the analysis, the list of files to be analyzed is updated to match the files given in <file list>.

New directive __ASTREE_exit((expr))

This new directive enables implementing program exits that are not errors, e.g. calls to the exit(int) function. Exit codes are reported by the analyzer.

Improved user handling

Specifying a user name for a server connection is now mandatory. The default user “anonymous” can be used to create analyses without access restriction. User data and the local settings of analysis projects are now stored in the server working directory. As a consequence, the local settings of an analysis project are preserved when installing new versions of Astrée. Also, the local settings of one user at a certain client can now be transferred to another user at a different client (via export and import).

Modified defaults

The default values for the options “volatile-global” and “volatile-auto” have changed. By default, the analyzer no longer assumes that the values of variables that are declared using the C keyword “volatile” may change asynchronously. The new default behavior matches the semantics of the keyword in most programs. Volatile behavior of individual variables or at certain program points can be expressed using Astrée directives.

Faster server operations

Adding/removing many files to/from a project works much faster.

Improved coverage information

Coverage information is now computed as the percentage of analyzed statements rather than lines. The Summary window features a new column that displays the number of statements that have not been analyzed.

Analyzer enhancements

  • Computing pointers with negative offsets no longer causes false alarms. An alarm is only raised if a pointer with a negative offset is dereferenced.
  • The analyzer no longer stops when evaluating an array of function pointers that contains a pointer to a function with missing definition as long as no attempt is made to call the missing function.
  • In cases of recursive function calls, the analyzer now always stops with an unhandled-recursion error.

Interface enhancements

  • The Log window can now display even very large analyzer outputs. Large projects are also loaded faster.
  • The displayed duration of the analysis now corresponds to the total time elapsed instead of the analysis time of the main function only.
  • In the Analysis Options views the options that differ from the defaults are highlighted (see screenshot). Tooltips show the default option values.
  • Arrays and structures in the Watch view are now displayed hierarchically. Type information is available at the uppermost and lowermost levels.
  • The Summary, Watch and Message windows now support filtering (press Ctrl+F).
  • The sorting order of messages in the Summary view has been reverted to match the user intuition.
  • All output area windows except the graph browser can now be fully navigated using only the keyboard.
  • The project file tree has been changed to a list to simplify navigating projects with deep hierarchies. Path information is displayed as a tool tip.
  • Modified projects can now be explicitly saved on the server (new Project menu entry).

Enhanced configuration possibilities

A number of options for configuring the user interface have been added, including:

  • actions at client start (whether to start a local server);
  • actions at analysis start;
  • editor defaults and warnings.

New file astree.h

The share directory of the installation contains a new header file astree.h with macros for stripping the Astrée directives during compilation.

  • Fixed batch mode option --drop to properly delete projects from the server.
  • Fixed inconsistent line breaks in the Log window when running the analyzer on Windows.
  • Corrected rare problems concerning the loading of the original source code.
  • Fixed rare cases of unreachable code not being marked gray in the editor.
  • Corrected the behavior of the expert option partition-all when partitioning loops.
  • Corrected the naming of watch window columns when loading invariants.
  • Fixed error message about incompatible types.
  • Corrected issues with the constant propagation of enum values.
  • Fixed the global directives editor to accept tabulator characters.