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.
When creating a new project, a wizard dialog now guides you through the basic analysis settings and provides online help for each of the configured options.
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 individually.
Analysis results can be exported in XML format. The XML reports comprise:
The generated XML reports can be displayed in a web browser or imported into Microsoft Excel and Word using the included XSLT stylesheet.
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
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.
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).
The default values for the options “
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.
Adding/removing many files to/from a project works much faster.
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.
A number of options for configuring the user interface have been added, including:
share directory of the installation contains a new
astree.h with macros for stripping the Astrée
directives during compilation.
--dropto properly delete projects from the server.
partition-allwhen partitioning loops.