Astrée Release 11.04

New features
* Source navigation
  After parsing a project with Astrée, the sources can be navigated
  using a type-sensitive search for identifiers like function definitions,
  function calls, variable definitions, or type declarations.

* Generalized representation of pointers
  The new representation allows casts between function pointers, data pointers,
  and integers. Pointer information is preserved over cast operations. This also
  holds for function pointers.

* Support for non-standard keywords
  A list of additional keywords can be specified to allow parsing code
  with compiler-specific extensions.

* Server access control
  Access can be restricted to a list of valid users. This disables
  the anonymous-user and the automatic-user creation feature.

* For each line in the preprocessed-source editor it is possible to go
  to the corresponding line in the original source.
* The Summary window has been split into two windows to simplify navigation
  of the two different summary views (Files and Categories).
* The Graph view can display the context in which an alarm occurs
  as well as all contexts in which a function is called.

* Added support for unnamed structs and unions.
* Added support for initializers with cyclic dependencies.
* Added support for variable declarations in for loops.
* Added support for binary constants (e.g. "0b010").
* Bitfields can be specified using enum types.
* Improved the verbosity of parse errors.

* The semantics of integer division by zero can now be configured.
  An integer division by zero either stops execution (default)
  or the execution continues but the result of the division is unknown.
* The warnings about possible side effects in expressions can be disabled.
* The domain for analyzing compute-through-overflow arithmetics
  can be disabled.
* The precision of pointer comparisons can be reduced
  to improve analyzer performance.

* "__ASTREE_partition_begin" accepts an optional argument
  that overrides the maximum number of partitions.
* "__ASTREE_suppress" accepts an optional argument
  that specifies the type of alarm to be suppressed.

* The built-in preprocessor no longer strips comments.
  This feature is controlled by an option.
* The Preprocessing view allows easier editing and adjustment of files,
  includes, and defines.
* Improved the Preprocessing dialog to give a better overview of errors
  and simplify navigating the output of the preprocessor.

Report files
* Added a new report type that creates a compressed analyzer log,
  useful for archiving results or sending them via email.
* Added the alarm category to the Messages XML report.

Other improvements
* The analyzer no longer stops after invalid or recursive function calls.
  Such calls are still reported as errors.
* Invariants can be omitted when exporting a project. This speeds up
  the export and reduces file size. The omitted invariants are only used
  to display information in the Watch window.
* Improved interaction with analyses that are owned by other users.
* Simplified installation.

Bug fixes (already delivered with patches for release 10.12)
* Fixed partitioning heuristic to avoid inadvertent value partitioning
  over floats.
* Fixed handling of long double. This type can be used if its size is
  restricted to at most 8 bytes in the ABI.
* Fixed rare issue with type propagation in switch statements.
* Corrected case-sensitive auto completion in the find/replace bar.
* Fixed issues with lost project-wizard options.
* Improved detection of disconnected clients.

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