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.