Astrée Release 13.10
--------------------
New features
------------
* Safety Manual for Astrée, aiT, and StackAnalyzer released.
The manual gives a detailed overview of DO-178B, DO-178C, and ISO-26262
with respect to runtime error checking, as well as to timing and
storage-space constraints. The verification objectives met by Astrée,
aiT, and StackAnalyzer are listed. The tool qualification strategy
for these tools based on QSK and QSLCD is detailed and shown to satisfy
the requirements of the respective standards. The Safety Manual is linked
from the Welcome page and the Help menu.
* Tool coupling between Astrée and TargetLink from dSPACE released.
The information stored in the TargetLink Data Dictionary is automatically
exploited to provide information about interface and environment
to AbsInt’s analyzers. This improves analysis precision and reduces
manual effort. Astrée alarm messages are directly linked
to the Matlab/Simulink model.
* The new AbsInt Tool Box lets Matlab/Simulink users launch Astrée, aiT,
or StackAnalyzer analyses from TargetLink with a single mouse click.
* Implemented support for OSLC export of analysis results.
* Astrée now supports the analysis of asynchronous programs.
To this end, the analyzer automatically detects potentially shared
variables and considers all possible interferences between tasks. The feature
is enabled by the new directive "__ASTREE_asynchronous_loop". An additional
directive "__ASTREE_shared_variable" allows the explicit specification
of shared variables. Shared variables can also be detected automatically
during the analysis when the option "automatic-shared-variables" is enabled.
Finally, the list of automatically detected shared variables can be reported
by enabling the option "report-shared-variables".
* New XML-based interface for defining analyses. The DAX format (Definition
of Analyses in XML) allows the specification of all features that are also
provided by the graphical user interface. It can be used in batch mode
for the complete automation of Astrée analyses (e.g. in CASE tools).
* The size of "enum" types can now be configured in the ABI. It can either be
"sizeof(int)" or the size of the smallest possible integer type that can hold
all "enum" values. The latter may be chosen either among signed integers only
or among signed and unsigned integers.
* The new option "cut-invalid-pointer" controls whether or not
the analyzer stops on computations with invalid pointers.
With "cut-invalid-pointers=no", the analyzer
continues assuming that the result of such an operation
is again an invalid pointer. Read accesses to invalid
pointers are assumed to return unknown values whereas
write accesses are treated as "nop" (doing nothing).
Analyzer
--------
* The analyzer now also lists directives which are not semantic
hypotheses (e.g. "__ASTREE_unroll" or "__ASTREE_partition_control")
in log and report files. These directives appear right after
the list of semantic hypotheses in the output.
* Fixed crashes in parallel analysis mode on code with recursive
type definitions.
* Fixed parsing of analysis wrapper files ("astree.cfg")
that end with a comment.
* The bounds of range specifications in "__ASTREE_volatile_input"
and "__ASTREE_global_assert" directives can now be written
as constant expressions, including hexadecimal and binary values.
* Directives that are syntactically but not semantically correct --
e.g., because they refer to non-existing variables -- no longer cause
the analyzer to stop. Instead an error is reported and the erroneous
directive is ignored for the analysis.
* Improved the precision of octagons when analyzing conditionals
in combination with other abstract domains.
* Improved the packing strategy for boolean packs,
so that the analysis is more precise.
Client/server
-------------
* The original, non-preprocessed source files corresponding to the analyzed
preprocessed files, can now also be added to an analysis project.
* Improved coloring and formatting of analyzer messages to improve
readability of text in the output window.
* The text in the output window is now divided into sections. The GUI
enables jumping directly to the different sections.
* By default the result area is hidden when a view belonging
to the "Local settings" or "Analysis configuration" is active.
A "Show results" buttom allows to display the result area.
* Improved performance when inserting or removing a large number
of AAL annotations.
* Projects now feature a name that is shared by all revisions.
* The annotations view now supports multiple selection of AAL annotations
so that several annotations can be enabled or disabled with a single click.
* The automatic extraction of annotations can now ignore a user-specified list
of files. It can also be adjusted to prefer "insert before" or "insert after"
annotations, or to create annotations with a minimal distance of lines
between annotation target and the original position of the directive.
* The options section "Verbosity" has been renamed into "Output".
* The XML report file now also contains notification messages.
* Fixed escaping of symbols in the XML summary and report files.
* XML summaries are now updated when re-running analyses in batch mode.
They can also be newly created in batch mode when specifying them
in the new DAX format.
Compatibility notice
--------------------
The output of analyses with version number ≤ 6 can no longer be displayed
by release 13.10. When converting such analyses to a more recent analysis,
old analysis results are deleted. To prevent data loss, we recommend exporting
all analyses with version number ≤ 6 using an older release of Astrée.
==============================================================================
Last modified on 30 October 2013 by alex@absint.com.
Copyright 2013 AbsInt. http://www.absint.com/
==============================================================================
An HTML version of these release notes is available at
http://www.absint.com/releasenotes/astree/13.10/