Astrée release 13.10

General

  • 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.
  • dSPACE logo
    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-specific

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

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.

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.