Astrée Release 11.12

New features
* Reorganization of analysis options
  All analysis options are now available via a single options view in the GUI.
  The number of options has been reduced in order to simplify the setup.

* Analysis time statistics
  The GUI can now display analysis time statistics. The statistics are updated
  online during a running analysis. Thus, it becomes possible to identify 
  hot-spot functions in long-running analyses.

* Detection of field escapes
  Astrée can track pointers that escape structure fields as long as 
  the pointers stay in the same variable. While this behavior enables 
  a low number of false alarms, it can sometimes be interesting to detect 
  such field escapes. The new option "warn-on-field-overflows=[yes|no]" 
  controls whether Astrée should report alarms in such cases.

* Full text search
  The Search view now provides an alternative full text search 
  over the entire project.

* Automatic tuning hints
  Astrée can now emit hints what to do in case of an alarm.

* Improved user manual
  An additional Quick Startup Guide now offers a simple introduction 
  for novice users.

* Qualification Support Kit
  A Qualification Support Kit (QSK) for Astrée is now available.

* Individual source files can now be excluded 
  from the computation of the total coverage.
* Code that is removed by constant folding (with "simplify=yes") 
  is now marked in the editor.
* The parser-view feature "Identifiers to ignore" has been superceded 
  by "Expressions to ignore" which accepts regular expressions.
* The "Global directives" and "Analysis start" views have been merged 
  into a new "Analysis entry" view. The new view features a full-fledged editor
  for editing wrapper and stub code.
* Includes for the shipped C library stubs are only used for preprocessing
  when the option "Use stubs for the standard C library" is enabled.
* The preprocessor now supports adding a directory with all its subdirectories 
  to the include path with a single command.
* Notifications from the analyzer regarding performance issues and semantic 
  assumptions are no longer classified as warnings in order to avoid confusion
  with alarms (potential runtime errors).

C frontend/parser
* Relaxed scoping rules to allow more valid C99 programs.
* Added support for function declarations within functions.
* The parser now accepts non-standard strings containing newline.
* The frontend no longer stops on array declarations without size. 
  All such arrays are reported and the analyzer only stops 
  if such an array is actually used.
* Astrée can now handle functions that are declared 
  using the inline function specifier.
* Astrée can now ignore assembly blocks marked by "#pragma asm/endasm".
  This feature can be controlled via the parser view of the GUI.

* Improved precision of computations that explicitly check 
  for NaN or infinity.
* Added warnings about repeated volatile input directives 
  for the same variable.
* Digital filter domain now supports 1st order filters 
  with non-constant filter parameters.
* Improved precision of digital filter domain for second-order 
  filters with real roots.
* Taking the address of a string literal is now allowed.

* New option "dump-invariants-with-unroll=[yes|no]" which behaves like 
 "dump-invariants" but outputs the joined invariants for unrollings 
  and iterations with widening.
* New option "dump-unused-suppress=[yes|no]" enables warnings about 
  unused suppress or comment directives.
* The option key "warn-undef-intializers" has been renamed into 
* New option "cache-iterates=N" for controlling the size 
  of a loop invariant cache. Enabling the cache can lead 
  to a significant speedup in the analysis of nested loops.

* Renamed the directive "__ASTREE_import_types(())" into "__ASTREE_import(())".
  The new directive can import global types, functions, and variables.
* The directives "__ASTREE_comment(())" and "__ASTREE_suppress(())" 
  can now be inserted with relative scopes using the annotation language AAL. 
  Alarms can therefore be commented or suppressed depending on their location 
  in the code structure.
* The directive "__ASTREE_initialize(())" can now also be used within 
  function scope to eliminate false alarms about uninitialized variables.

* The server now writes a log file which eases the debugging 
  of server configuration issues.
* The tray icon for the server controller has been removed.
* The server now accepts a new command line option --name 
  for setting its name as seen by clients.

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