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).

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

* 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
Copyright 2013 AbsInt.
An HTML version of these release notes is available at