Astrée Release 12.04

New features
* 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 report
  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.

  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 has been adapted 
  to better reflect the alarm severity. The new semantics is:
    - 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
  An alarm is a potential runtime error with either:
  - an unpredictable result (Type A), or 
  - a predictable result (Type C)
  An error is 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.

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

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

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

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

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

* Added tests for validating that value ranges computed by Astrée are correct.

* The new extended XML report is now also validated.

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

Last modified on 10 April 2012 by
Copyright 2012 AbsInt.
An HTML version of these release notes is available at