Astrée Release 12.10
--------------------
New features
------------
* 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.
* 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.
==============================================================================
Last modified on 1 October 2012 by alex@absint.com.
Copyright 2012 AbsInt. http://www.absint.com/
==============================================================================
An HTML version of these release notes is available at
http://www.absint.com/releasenotes/astree/12.10/