Astrée release 11.12

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 on-line 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.

Interface

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

Analyzer

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

Options

  • 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 warn-undef-functions.
  • 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.

Directives

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

Server

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