Astrée release 11.04

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.

Interface

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

Parser

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

Options

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

Directives

  • __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.

Preprocessor

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