Astrée Release 10.12

New preprocessor support
It is now possible to specify a list of original source files and preprocessor
settings (include paths and defines). 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 guides the user through
the basic analysis settings. The wizard also 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 allows to display only the relevant
program parts and to investigate modules individually.

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 analyis, 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. 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 tooltip.
* Modified projects can now be explicitly saved on the server
 (new Project menu entry).

Enhanced configuration possibilities
Several 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.

Bug fixes
* 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.

Last modified on 15 December 2010 by
Copyright 2010 AbsInt.
An HTML version of these release notes is available at