Astrée release 12.10

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 support@absint.com if you wish to enable this feature.

Options

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

Directives

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.

Analyzer

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

GUI

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

Server

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