Astrée Release 14.04
--------------------
New features
------------
* The XML reports of different analyses or different versions
of the same analysis can now be compared with respect to options,
directives, source files, and numbers of alarms and errors,
using the XML differences viewer which is available from the
tools menu. The differences viewer can also be accessed from
the analysis history dialog to inspect the differences between
different revisions of an analysis.
* The analyzer can now detect and warn about write accesses
to variables which are possibly not read between two write accesses
(write-after-write). This feature is controlled by the new option
"warn-on-write-after-write".
* The GUI can now save the project configuration in a DAX file.
This feature is available via "Project" -> "Export" -> "Project...".
* The new External Declarations view allows to specify types
and (function) declarations that are missing, e.g. because
they are part of compiler-specific extensions, or because
some include files are not available to the analyzer.
One use case for this feature is for generating stub functions
for compiler intrinsics. When providing the analyzer with a suitable
function declaration via the External Declarations view,
it can automatically generate a stub function if the option
"auto-generate-stubs" is used.
* The new directive "__ASTREE_partition_ranges((e:a1,...,an))"
allows partitioning an expression "e" according to a list
of intervals "a1,...,an". The alternative syntax
"__ASTREE_partition_ranges((e1;min_size=e2;max_partition=n))"
automatically generates partitions covering the range
of the expression "e1" using the minimal size specified by "e2"
and/or the maximum number of partitions "n".
Analyzer
--------
* The detection of shared variables has been improved
so that it is now possible to have two tasks using the same
entry function. This brings about a modification of the
__ASTREE_asynchronous loop directive, which now
requires all tasks to be listed explicitly. Hence, analysis
wrappers of the following form are no longer valid:
typedef void(*t)(void);
static t tasks[] = { t1, t2 };
unsigned int idx;
__ASTREE_known_fact(( idx < 2 ));
__ASTREE_asynchronous_loop(( tasks[idx]() ));
The correct way for re-writing the above analysis wrapper example is:
__ASTREE_asynchronous_loop(( t1, t2 ));
The wrapper generator in the GUI has been modified accordingly.
* Fixed the AAL processor so that it allows inserting
"__ASTREE_partition_control" statements before assignments.
* Fixed the calculation of coverage information and number of statements
for analyses that use the option "auto-generate-stubs=yes".
* Improved the precision of the analyzer on barycentric computations
of the following form:
in1 = [-1.1];
in2 = [-1,1];
while (1) {
b = [0,1];
out = b * in1 + (1 - b) * in2;
if (*) in1 = out;
if (*) in2 = out;
}
* Astrée now issues an alarm when an expression may write
to a string literal in which case the behavior is undefined
and the program may even crash. Here is an example:
char *s = "Sky";
s[0] = 's';
The result of Astrée:
ALARM (A): write to constant: writing to string literal "Sky".
Definite runtime error during assignment in this context.
Analysis stopped for this context.
* If an AAL annotation cannot be inserted, the analyzer no longer stops
but reports an error message and continues with the analysis.
* The precision of the domain of boolean relations has been improved.
In particular, the analysis of guards in tests is now more precise.
* The option "cut-invalid-pointer" has been removed.
* The new expert option "dump-hypotheses=[yes|no]" controls whether
the analyzer output contains additional sections that list all
semantic hypotheses and further directives. It is provided so that
the size of the analyzer output can be reduced when running analyses
with very large numbers of directives. However, it is recommended
to leave the option enabled so that the result documents the semantic
hypotheses on which the correctness of the analysis result relies.
* Improved the precision of the analyzer when analyzing conditional
expressions using the bitwise OR operator.
* Improved precision on pointers when casting them as integers.
* Initialization of global variables to 0 can now be activated independently
of the initialization option for static variables. That is, even with
"static-initialization=no" and "global-initialization=yes",
the non-static global variables will now be initialized to 0.
Client
------
* Modified the automatic wrapper generator for TargetLink so that
the root step functions of the model can be called in arbitrary order.
* The text search feature of the GUI can now also search the original
source files, not only the preprocessed files.
* Modified the filtering (Ctrl+F) in the Summary/C view so that filters
now consider the names of the categories, not the alarm messages.
* Modified the filtering (Ctrl+F) in the Summary/F view so that filters
now consider the names of the files, not the alarm messages.
* A new standard example demonstrates automatic detection
and sound analysis of shared variables in asynchronous tasks.
* Filtered expressions are now highlighted in the editor
also when the analysis was not successful.
* The original source files of an analysis project can now be downloaded
from the server from the context menu of the original files list.
* Re-designed the preprocessing dialog of the GUI to improve usability,
performance, and flexibility.
* Fixed sporadic crashes when deleting configurations
from the Preprocessing view.
* Improved warning message when some reports could not be generated.
* It is now possible to reorder the entries in the Parser view using
drag and drop.
* Improved performance and reduced memory consumption when loading
information about not analyzed code in the client.
* A tooltip in the Coverage column of the Summary/F view now displays
the number of statements that were not analyzed, together with
the total number of statements in the file.
* The Alarm density view can now be filtered such that it displays
only functions with more alarms than a given threshold.
Server
------
* Fixed the automatic upload of original source files to the server
after preprocessing. Instead of uploading only the C files from the list
of files to preprocess, it now also uploads all included header files.
* Locating the original source files for large analysis projects
is much faster now.
* Fixed a bug that could cause the upload of original source files
to overwrite some of the preprocessed files on the server.
* The uploading of source files to the server has been optimized
to reduce transfer times.
* Reduced server startup time on working directories with many large projects.
* Improved the error message for client/server connection failures
due to version mismatch.
==============================================================================
Last modified on 8 April 2014 by alex@absint.com.
Copyright 2014 AbsInt. http://www.absint.com/
==============================================================================
An HTML version of these release notes is available at
http://www.absint.com/releasenotes/astree/14.04/