Astrée Release 12.10

New features
* Global assertions
  Astrée can now check global invariants that are specified by the new 
  directive __ASTREE_global_assert((V; [l;h]));, where V is a global variable 
  of integer or float type and [l;h] is an interval. The analyzer raises 
  an alarm whenever the assertion is violated by assigning V a value 
  that is not in the range [l;h].

* Data and control flow reports
  Astrée now collects

  - all called functions per function
  - all functions calling a given function
  - which global/static variables are read/modified per function
  - which functions read/modify a given global/static variable

  The collected information is displayed in the GUI and can be exported 
  into two dedicated summary files.

* Analysis project revisions
  It is now possible to create multiple revisions of an analysis project. 
  Thus, one can go back to earlier versions of an analysis and trace back 
  modifications of the configuration or the code.

* Visualization of the alarm density
  The density of alarms, i.e., the number of alarms per function relative 
  to the number of alarms in other functions is now visualized in the GUI.

* Wrapper generator
  The analysis wrapper code can now be generated from a specification of 
  the program's input variables, initialization functions, and periodic tasks.

* Automatic consistency checks for AAL annotations
  It is now possible to define a reference AAL insertion. Astrée can then 
  check that the annotations are inserted in exactly the same way in further 
  analysis runs. If a check fails, e.g. because the source code has been 
  modified, Astrée will notify the user that the annotation has to be reviewed.

* Scenario builder
  The scenario builder allows selecting a number of functions and main 
  loop invariants for which to generate a "scenario". A scenario is a 
  derived analysis project which inherits the original project's settings
  but analyzes only the selected functions. During the analysis of the 
  scenario, the selected invariants are enforced using directives.

  Please note that this feature is not part of the basic license. 
  Contact if you wish to enable this feature.

* The option verbose-uninitialized-alarm has been replaced by the new option
  verbose-variable-alarm which also controls whether variable names are 
  printed in full range warnings.
* The option "Simplify the source code by evaluating constant expressions" 
  is now deactivated by default (simplify=no).

The __ASTREE_absolute_address directive can now also be used with a type 
instead of a variable name. Accesses to the specified memory region become 
valid but the memory is not tied to a specific variable.

* Astrée no longer requires that the analysis starts from a function without 
  parameters. If a function with parameters is chosen as an entry point, 
  the analyzer assumes that all parameters have full range.

* __ASTREE_initialize directives are now printed in the list of semantic 

* Improved reachability information in the presence of goto statements.

* Improved the handling of invalid pointer comparisons that could stop 
  the analysis.

* Improved the precision of the analyzer when detecting overflows.

* Improved the precision when analyzing multiplication operations.

* The parser now accepts the special control characters form feed, 
  horizontal tab, and vertical tab.

* The parser now accepts line directives without file names as produced 
  by some compilers.

* Fixed exceptions when handling large integer constants on 32-bit platforms.

* The call graph can now be exported to Pdf from the context menu.

* The Annotations view now allows selecting and deleting multiple annotations 
  at once.

* The algorithm for searching the original source files has been changed. 
  The view "Mapping to original sources" makes it possible to automatically 
  generate suggestions for includes and replacements needed to find any missing
  original source files.
* Search operations in the Output view now start at the first character that is
  currently visible.

* The automatic synchronization of files between the server and the local 
  machine can now be disabled.

* The encoding of non-UTF-8 files can now be configured in the preferences 
  in order to properly display Chinese or Japanese characters in the editor.

* The global text search can now be configured to be case sensitive or to
  interpret the search string as a regular expression.

* The GUI now displays information about the memory consumption 
 (RAM and hard disk) of an analysis.

* Improved the network communication.

* When changing the server data directory, analyses from the old data directory
  that have not been copied into the new directory are no longer displayed 
  in the list of available analyses.
* Fixed the --max-local option so that the server does not start additional 
  analyzer processes if the value 0 is passed.
* Fixed server controller connection issues on Windows computers without 
  network connection.

Bug fixes
* Fixed cases where conditional expressions with division operators 
  would cause the analysis to stop.

* Fixed missing highlighting of completely not analyzed functions 
  in the original source editor.

* Fixed the loading of options that have no effect on the analysis 
  because they depend on other disabled options.

* Added missing timing statistics for functions taking less than one second.

* Fixed issue with deeply nested expression using ternary operators (?:)
  leading to very high memory consumption (issue #10520).

* Fixed issue with multiple master analyzer processes being started 
  for distributed parallel analysis.

* Fixed invalid integer to pointer conversion in the standard 
  C-library function wctrans.

* Fixed issue with spurious overflow alarms triggered 
  by warn-on-uninitialized=yes.

* Fixed evaluation of side effects in conditions of if and switch statements.

Bug fixes already delivered with patches for release 12.04
* Fixed missing highlighting of completely not analyzed functions 
  in the original editor.

* Fixed problem with files missing from the Summary/F view (issue #10612).

* Reduced memory consumption of the parser when filtering the code 
  using regular expressions.

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