Astrée Release 11.08

New features
* External directives
  Directives can now be separated from the source code. The new 
  AAL annotation language allows to identify source code locations 
  based on the program structure.

* 64-bit integers
  64-bit integer types are now fully supported by Astrée.
* Gotos
  The restrictions on gotos have been removed. Astrée can now also 
  analyze code that contains backward gotos. 
* Detection of uninitialized variables
  Astrée finds and reports read accesses to uninitialized variables. 
  The corresponding alarms can be enabled and disabled by the option 
* Full-range warnings
  The analyzer can now produce warnings whenever a variable changes 
  its value to full range. This feature is controlled by the new option 

* Improved TargetLink support
  Astrée now takes into account TargetLink's /* CTO */ comments 
  in order to improve the detection of compute-through-overflow computations
  and to reduce the number of false alarms in TargetLink-generated code. 
  This feature is controlled by the new option honor-cto-comments=[yes|no].

* The "__ASTREE_partition_control" directive 
  now also works for switch statements.
* The "__ASTREE_known_fact" directive has been generalized for pointers.
* Alarms can be commented and classified as "true", "false", and "undecided"
  using the new "__ASTREE_comment" directive.
* The "__ASTREE_loop_unroll" directive now also works for for-loops with 
  variable declarations.
* The new directive "__ASTREE_import_types" allows to import types from 
  project source files into the Global directives view. This significantly
  simplifies specifying global directives.

* The new option "warn-volatile-ignore=[yes|no]" controls whether Astrée 
  issues a warning whenever the C volatile keyword is ignored. The new option 
  is disabled by default to avoid too many warnings.
* The new option "quick-widening=[yes|no]" controls whether the analyzer 
  may enter the quick widening mode.

* The user space and system space server modes have been integrated 
  into a single server executable.
* Server data directories are now locked. The locking prevents inconsistencies 
  that could arise if running more than one server on the same data.
* Server access can be restricted to a set of registered users.
* Servers now announce their existence on the local network 
  and can be found automatically by the Astrée GUI.

* It is now possible to detach open editor views into separate windows.
* Added launcher for managing multiple installed client and server versions.
* All unanalyzed code is now listed in the Summary/F view. It is possible 
  to step through that list to traverse all unanalyzed code fragments.
* The current project name is now displayed in the title bar of the GUI.
* Code that has been discarded by the frontend based on the settings 
  in the Parser view is now marked light gray in the editor.

* Functions with code that uses non-standard syntax extensions 
  or inline assembly can be completely ignored by the frontend.
* The parser can now guess the types of unknown functions, 
  thus simplifying the analysis of incomplete software projects.

* Added two new XML reports in which alarms and errors are ordered 
  by category or source file, respectively.
* All XML reports list the analysis options and semantic hypotheses.

* Optimized the raw analyzer output to reduce disc-space and network-bandwidth
* Improved precision of the analyzer when checking for division by zero.

Bug fixes (already delivered with patches for release 11.04)
* Fixed the handling of temporary data in the Astrée client 
 (client reports "Unable to write to the temporary directory").
* Fixed inadvertent removal of required integer cast operators.
* Fixed cases where the analyzer stopped unexpectedly 
  when evaluating a condition.
* Fixed missing updates of the Summary/C window in the output area of the GUI.
* Corrected strcpy implementation in the example C stub library.

Last modified on 12 August 2011 by
Copyright 2011 AbsInt.
An HTML version of these release notes is available at