Astrée release 12.04

Analysis queue

Analysis requests can now be queued. Requests in the queue run automatically as soon as they reach the first position, i.e., when all previous requests are finished, and the server has free resources.

Extended XML export

Astrée can now generate an extended XML report that contains all relevant information of an analysis run in a form that is convenient for machine processing. The report can be generated in batch mode as well. The extended XML export is also covered by the qualification support kit (QSK) for Astrée.

QSLCD

Released QSLCD (Qualification Support Life Cycle Data) report documenting compliance of tool development to safety standards.

Automatic extraction of directives

Astrée now supports the automatic extraction of directives that have been inserted into the source code and their conversion into external AAL directives.

General improvements

  • Alarm type B has been removed. Such alarms are now classified as type A alarms.
  • The semantics of the traffic lights have been adapted to better reflect the alarm severity. The new semantics are:
    red at least one error
    yellow no errors, but at least one alarm of Type A
    yellow and green no errors and no Type A alarms,
    but at least one alarm of Type C
    green no errors and no alarms
    • Alarm: a potential runtime error with either an unpredictable result (Type A),
      or a predictable result (Type C)
    • Error: either a Type A alarm that definitely occurs in some context,
      or a fatal error in the analysis (e.g., a parse error due to incorrect input)
  • The message category “WARNING” has been replaced by the new category “NOTE” in order to avoid confusion between user notifications and messages about potential runtime errors (“ALARM”).
  • Improved error handling for AAL annotations.
  • Parser filters are no longer applied to the wrapper and stubs file.

Options

  • The option warn-sideeffects is now deactivated by default.
  • New batch mode option --xml-report-file <filename> for generating the extended XML export.
  • In batch mode, the parameters --id and --import can now be used simultaneously for overwriting an existing analysis project with an analysis imported from an aaf file.

Directives

  • The __ASTREE_partition_control directive now also works for assignments.
    This is useful for assignments of the form “bool_var=condition” that are equivalent to “if (condition) bool_var=1; else bool_var=0”.
  • The __ASTREE_initialize directive now removes NaN when used on floating point variables.
  • The __ASTREE_exit directive now also reports the context in which the directive is reached.

Analyzer

  • The automatic zero initialization of large global variables has become much faster.
  • Improved the detection of some digital filters.
  • Added support for pointer type conversions in ternary expressions.
  • Improved support for struct initializers.
  • Astrée now also raises alarms when NaN floats are used in comparisons (==, !=, <, >, <=, >=).
  • Function calls with argument mismatch are now analyzed instead of just reporting an alarm. This improves the coverage of the analysis. The analyzer still reports alarms for such cases.

GUI

  • Newly imported AAL annotations can now also be appended to an existing list of annotations.
  • Pointer values are now displayed in hexadecimal format if they may point to at least one absolute address. This applies to the display of pointers in tooltips and in the watch window.
  • The results of filters (accessible via Ctrl+F in some views) can now be inverted to display only items that do not match the filter criteria.
  • The Parser view has been reorganized to allow more convenient filtering.
  • Filtered regular expressions are now marked in the editor.

Server

Added support for the administration of multiple Astrée servers on the same machine using the server controller interface.

QSK

  • Added tests for validating that value ranges computed by Astrée are correct.
  • The new extended XML report is now also validated.
  • Fixed intermediate representation to handle multiple for loops with declarations in the same function.
  • Fixed cases of missing source line information in error messages.
  • Fixed corner cases in the parser filter.
  • Fixed cases where the original source line information was lost.
  • Fixed analyzer crashes in cases of missing function declarations.
  • Fixed constant propagation and the handling of bit fields.
  • Fixed handling of special characters in regular expressions of parser filters.
  • Fixed report file generation in batch mode.
  • Deprecated option keys have been removed from the output of the analyzer.