Astrée release 11.08

External directives

Directives can now be separated from the source code. The new AAL annotation language allows to identify source code locations based on the program structure.

64-bit integers

64-bit integer types are now fully supported by Astrée.

Gotos

The restrictions on gotos have been removed. Astrée can now also analyze code that contains backward gotos.

Detection of uninitialized variables

Astrée finds and reports read accesses to uninitialized variables. The corresponding alarms can be enabled and disabled by the option warn-on-uninitialized=[yes|no].

Full-range warnings

The analyzer can now produce warnings whenever a variable changes its value to full range. This feature is controlled by the new option warn-on-fullrange=[yes|no].

Improved TargetLink support

Astrée now takes into account TargetLink’s /* CTO */ comments in order to improve the detection of compute-through-overflow computations and to reduce the number of false alarms in TargetLink-generated code. This feature is controlled by the new option honor-cto-comments=[yes|no].

Directives

  • The __ASTREE_partition_control directive now also works for switch statements.
  • The __ASTREE_known_fact directive has been generalized for pointers.
  • Alarms can be commented and classified as true, false, and undecided using the new __ASTREE_comment directive.
  • The __ASTREE_loop_unroll directive now also works for for-loops with variable declarations.
  • The new directive __ASTREE_import_types allows to import types from project source files into the Global directives view. This significantly simplifies specifying global directives.

Options

  • The new option warn-volatile-ignore=[yes|no] controls whether Astrée issues a warning whenever the C volatile keyword is ignored. The new option is disabled by default to avoid too many warnings.
  • The new option quick-widening=[yes|no] controls whether the analyzer may enter the quick widening mode.

Server

  • The user space and system space server modes have been integrated into a single server executable.
  • Server data directories are now locked. The locking prevents inconsistencies that could arise when running more than one server on the same data.
  • Server access can be restricted to a set of registered users.
  • Servers now announce their existence on the local network and can be found automatically by the Astrée GUI.

Interface

  • It is now possible to detach open editor views into separate windows.
  • Added launcher for managing multiple installed client and server versions.
  • All unanalyzed code is now listed in the Summary/F view. It is possible to step through that list to traverse all unanalyzed code fragments.
  • The current project name is now displayed in the title bar of the GUI.
  • Code that has been discarded by the frontend based on the settings in the Parser view is now marked light gray in the editor.

Frontend/parser

  • Functions with code that uses non-standard syntax extensions or inline assembly can be completely ignored by the frontend.
  • The parser can now guess the types of unknown functions, thus simplifying the analysis of incomplete software projects.

Reports

  • Added two new XML reports in which alarms and errors are ordered by category or source file, respectively.
  • All XML reports list the analysis options and semantic hypotheses.

Other

  • Optimized the raw analyzer output to reduce disc space and network bandwidth requirements.
  • Improved precision of the analyzer when checking for division by zero.

Bug fixes (already delivered with patches for release 11.04)

  • Fixed the handling of temporary data in the Astrée client (client reports “Unable to write to the temporary directory”).
  • Fixed inadvertent removal of required integer cast operators.
  • Fixed cases where the analyzer stopped unexpectedly when evaluating a condition.
  • Fixed missing updates of the Summary/C window in the output area of the GUI.
  • Corrected strcpy implementation in the example C stub library.