Astrée Release 15.04
--------------------
General
-------
* The C stub library now supports 16-bit and 32-bit architectures.
The correct configuration is inferred from the size of a pointer
in the ABI settings.
* When opening for the first time an analysis created with an older release,
verify your local settings (Preprocessing, Reports, Code generators).
In rare cases, the automatic conversion may produce invalid entries.
Precision
---------
* The analyzer now computes significantly more precise intervals
for expressions using the bitwise operators AND (&), OR (|),
and XOR (^).
* The new option "partition-pt1" partitions first order lag (PT1) elements
of the form "x + (i - x) * c" to allow for a more precise analysis.
This option is enabled by default.
* The new non-relational domain of congruence intervals adds precision
when dealing with deeply nested structures and arrays. It is activated
via the new option "congruence-intervals=yes".
* The new option "exclude-signed-in-unsigned-overflows=yes" keeps precise
information for signed values that are explicitly cast to unsigned.
When casting the unsigned result back to signed, the analysis can then
yield a more precise result. The analyzer reports overflows of signed
values in unsigned computations only if the overflow also occurs
in the signed representation. This feature is particularly useful
for analyzing TargetLink-generated code.
In addition, the new option "exclude-signed-negation-overflows-in-cto=yes"
will exclude alarms raised by signed negations (when negating the smallest
representable integer of a given type) when that negation occurs after
casting an unsigned with CTO semantics.
C language features
-------------------
* Added support for compound literals like "&((struct s){0})".
* Astrée now accepts non-standard empty initializer lists
(e.g. "int arr[] = {};") which are supported by many C compilers.
* Added support for the keyword "typeof" (GCC extension).
Astrée can now analyze code such as
int x = 3; typeof(x) y = 900 / x;
* The new option "anonymous-global-structs-and-unions=yes" enables support
for global anonymous structs and unions. This is a C language extension
supported by some compilers. Astrée implements the behavior
of the IAR compiler and names such objects after their first field
with the prefix "_A_".
* The analyzer now accepts functions with variable argument lists.
Directives
----------
* New:
* "__ASTREE_trash" for use in stub functions (e.g. the C library stubs).
It models a random modification of a given number of bytes of memory
starting from a given address.
* "__ASTREE_access((v, s));" models a read access on the first s bytes
of the variable v.
* "__ASTREE_huge_valf()" and "__ASTREE_huge_val()" return
positive infinity as a floating constant of type float
or double, respectively. They are used to implement
the standard macros "HUGE_VAL", "HUGE_VALF", and "INFINITY"
in the C stub library.
* "__ASTREE_va_start((param));" allows implementing the "va_start"
macro of the C standard library for initializing a "va_list" object
to handle variable argument lists. An implementation of the macro
(together with corresponding declarations of the "va_arg", "va_copy",
and "va_end" macros) can be found in the standard C library stubs
that are installed with Astrée.
* "__ASTREE_malloc" can be used to implement "malloc", "realloc",
and "free". Stubs for these functions have been added to the Astrée
C library to illustrate the usage of the new directive.
* Improved and extended:
* The "__ASTREE_comment" directive now accepts new types of comments
for alarms. In addition to "false", "true" or "undecided", an alarm
message can now also be classified as "true_high", "true_low"
or "true_no_defect".
* The directive "__ASTREE_absolute_address" has been extended
to also work for static variables.
* The analyzer now accepts "__ASTREE_partition_control" directives
before for-loops with declarations, e.g.
__ASTREE_partition_control((12)) for (int i = 0; i < 12; i++)
* It is now possible to keep the partitions created during a function call
after the return point. To that end, the function call should be preceded
by the directive "__ASTREE_partition_control", e.g.
__ASTREE_partition_control f(4);
* Generalized the "__ASTREE_modify" directive to allow modifying
lists of values and specifying new ranges for modified values.
For example, the annotation
__ASTREE_modify(( x, y[0-3], z->p; [11,42] ));
sets the value range of x, y[0], y[1], y[2], y[3], and z->p
to the interval [11,42].
Note that this extended directive can raise a new kind of alarm
if the specified interval is invalid.
Options
-------
* The new option "ais-export=yes" enables the collection of information
about calls via function pointers. The collected information can be
exported into an AIS file for use by a³ binary-level static analyzers
(e.g. StackAnalyzer).
* Removed the option "show-hints".
* Removed the option "stop-parse-error-delayed" which allowed starting
the analysis even if there were parse errors in the preprocessed files.
All preprocessed files in the project must now either be accepted
by the analyzer or removed.
* Added a new option "list-entry-functions=n" for collecting all functions
with the maximum call depth of n. The collected information is used
to display a list of potential entry functions for the analysis.
* The option "separate-function" is now fully compatible
with the data flow options "dump-dataflow" and "report-shared-variables".
* There are two new ABI settings, "rounding_mode"
and "rounding_mode_for_constants". The latter is used for the parsing
of constants and the former is used for all other floating-point operations.
Both optons can be set to "to_nearest" or to "all". The latter means
that no assumption is made by the analyzer concerning the rounding mode.
The default rounding mode for constants is "to_nearest" (as required
by the C standard), while for the other operations it is "all".
For architectures using internal representations with more than
64 bits for doubles, "rounding_mode" should always be set to "all"
since the double rounding is not equivalent to rounding to nearest.
* Replaced the option "warn-on-initializer-ranges=yes"
by the new option "exclude-overflows-in-initializers=no".
* Removed the option "honor-cto-comments" for suppressing alarms
in expressions marked with TargetLink's CTO comments. It is
no longer needed since the analyzer can now automatically exclude
the undesired alarms by semantics-based reasoning activated via
the new option "exclude-signed-in-unsigned-overflows".
Fixes
-----
* Fixed the clock domain which could cause very high analysis times
in release 14.10 and release 14.10i with build numbers below 234645.
* Fixed analyzer crashes when dealing with variables
allocated to the absolute address 0.
Rule Checker
------------
* Added support for the Misra-C:2012 rule set.
* MISRA-C:2004:
* Added support for rules 3.4, 5.7, 12.1, 12.6,
16.7, 19.3, 19.7, 19.9, and 21.1.
* Extended support for rule 16.8.
* Fixed check missing-else for rule 14.10 of MISRA 2004.
The rule checker no longer warns about single "if"
statements without "else". MISRA requires a final
"else" clause only for "if ... else if ..." cascades.
* The checks rule 5.4 have been refined and now also take enum tags
into account.
* Fixed check for rule 8.12. The respective rule check is
no longer restricted to header files.
* Improved the precision of MISRA-C rule checking to remove
false alarms for the checks include-syntax, plain-char-usage,
and statement-sideeffect.
* Fixed false alarms concerning violations of rule M.8.8 and M.10.1.
* Extended the checks for rule 20.2 to declared identifiers.
* Added a second comment density code metric that follows the HIS definition.
* The Rule Checker can now also check naming conventions for variables,
functions, macros, and user-defined types. Valid names can be specified
via regular expressions. The feature is found in the new "Style rules"
category in the options.
* The Qualification Support Kit package that validates the Rule Checker
is no longer an add-on to the basic Astrée QSK that validates
the run-time error analysis. The two QSKs are now separate and
require separate qualification test runs.
GUI
---
* All-new Result Viewer for exploring all findings of the analyzer.
It displays a list of alarms and errors which can be easily browsed,
sorted, and filtered. A single click on a finding loads all relevant
information, such as the source code with tooltips and the list
of all relevant contexts. Each finding can be classified and
commented by the reviewer. Available classifications are:
* true error
* true error with high priority
* true error with low priority
* true error that is not considered a defect in the software under analysis
* false alarm
* undecided
The results of the review appear in the XML reports and summaries.
It is not necessary to re-run the analysis.
* It is now possible to generate AAL annotations automatically
by simply right-clicking into the code displayed in the editor
and selecting "Generate Annotation" from the context menu.
After specifying a directive to insert, Astrée automatically
generates the AAL specification that places the directive
at the selected position in the code. The analyzed code is not modified.
* Added a new display of potential entry functions (periodic
tasks and initialization functions) based on a pre-analysis
of the source code. The list is available via the Tools menu,
and is also displayed automatically if no analysis entry point
was specified. Relevant tasks and initialization functions can
then be selected to configure the analysis. Collecting information
about potential entry functions can be disabled via the new
option "list-entry-functions".
* The new editor view mode preference (accessible via Project ->
Preferences -> Editor) allows to change the default view
for preprocessed code. Available choices are "Original source",
"Preprocessed source", and "Split view" which displays the original
and preprocessed sources side by side.
* Improved editor layout and performance when adding a large number
of annotations to the exact same program point.
* In the Output view of the GUI, it is now possible to copy
not only whole lines but also line parts.
* The extraction of AAL annotations from the source files can
now be canceled using either the stop button in the menu bar or
the "Stop extraction" button in the "Advanced" tab of the Annotations view.
* Importing an Astrée options file (via Project -> Import ->
Options) now only affects options that are listed in the imported file.
Other options are no longer reset to their default value.
* The "new project" wizard can now be skipped (added finish button).
* It is now possible to jump directly back to the last displayed
editor view by clicking on the "Files" entry in the project side bar
or pressing Alt+E.
* Modified the default behavior when loading a DAX specification
that references a wrapper file and at the same time contains further tags
in the "<wrapper>" section. In this case, Astrée no longer
re-generates the wrapper automatically but uses the referenced ".cfg"
file. Running a batch mode analysis with such a file behaves likewise.
* Fixed the actions "Select category", "Unselect category", "Select all",
"Unselect all" in the context menu of the Rules options.
This fixes a known issue from release 14.10.
* The Preferences dialog has been extended by a field for specifying
a user name for authentication with the Astrée server.
Toolbox and Data Dictionary import
----------------------------------
* Astrée now imports value range annotations from the Data Dictionary
also for calibration variables of vector and matrix types,
and for variables with the flag "volatile=off".
* Fixed an issue that prevented the usage of the AbsInt Toolbox
with MATLAB versions older than 2013a (removed the usage of "strsplit").
* Improved the detection of available subsystems in the Toolbox.
This fixes issues with missing stub functions for lookup and
interpolation routines.
* Optimized annotations generated for TargetLink’s
linear search interpolations.
* Added an option to the AbsInt Toolbox for running a user-defined
MATLAB script, e.g. for generating additional AAL annotations,
before starting the Astrée analysis.
* The DD import now also annotates ranges for array parameters.
* The DD import now also generates assertions for vector outputs.
* Bounds for scaled fixed point values are now always rounded
to integer numbers. Rounding is downwards for lower bounds
and upwards for upper bounds.
* Added a new option for adding the source files of the DSFxp library
to an analysis.
* Improved generated directives for RTE-Frame variables.
Server
------
* The server data directory name may now contain special characters
(like é).
* The server now closes all open client connections
when the data directory is changed via the server controller.
Documentation
-------------
The Astrée documentation has been extended by a new manual
containing detailed compliance matrices for Astrée
regarding undefined/unspecified/implementation-defined behaviors
according to the C99 standard.
==============================================================================
Last modified on 4 May 2015 by alex@absint.com.
Copyright 2015 AbsInt. http://www.absint.com/
==============================================================================
An HTML version of these release notes is available at
http://www.absint.com/releasenotes/astree/15.04/