Astrée Release 15.10
--------------------
Detection of data races and inconsistent locking
------------------------------------------------
Astrée has been extended to perform a precise and sound analysis
of asynchronous programs. All possible interactions between parallel tasks
are now considered. All potential data races and lock/unlock problems
are detected. ARINC 653 and OSEK applications can be analyzed fully
automatically taking the OS behavior into account.
* New categories of alarms:
* Data races
(read/write or write/write concurrent accesses by two threads
to the same memory location without proper mutex locking)
* Inconsistent locking
(lock/unlock problems)
* Invalid calls to operating system services
(e.g. OSEK calls to TerminateTask() on a task with unreleased resources)
* New OS stub libraries, fully integrated with the built-in preprocessor:
* OSEK
* ARINC 653
* New analyzer-intrinsic functions for modeling OS actions:
* __astree_create_process
* __astree_start_process
* __astree_lock_mutex
* __astree_unlock_mutex
* and many more
* New analyzer options:
* warn-on-data-race=[yes|no]
warns about potential data races (enabled by default)
* log-parallel-iter=[yes|no]
prints extra progress information
when iterating over asynchronous processes
* dump-data-dictionary=[yes|no]
prints the final ranges of global variables
and statistics about shared memory usage
* dump-process-dataflow=[yes|no] collects reads and writes
of global variables and aggregates them per process
* Collection of data flow information per parallel process/task.
The collected information is displayed in the GUI and can be
written to a report file.
New analyzer-intrinsic functions
--------------------------------
Several directives have been replaced by analyzer-intrinsic functions.
Semantically, they still correspond to directives, but are no longer listed
as such in the analyzer log.
This modification affects all built-in operations of the analyzer
that are used solely for implementing stub functions.
Existing source files for stubbing can still be used
when including the astree.h header file and defining
__ASTREE__ and __ASTREE_LEGACY_DIRECTIVES__ when preprocessing.
Here is the list of the affected directives and the new
analyzer-intrinsic functions they have been replaced with:
* __ASTREE_bzero -> __astree_bzero
* __ASTREE_double_exp_2 -> __astree_double_exp_2
* __ASTREE_double_extract_exponent -> __astree_double_extract_exponent
* __ASTREE_double_sqrt -> __astree_double_sqrt
* __ASTREE_exit -> __astree_exit
* __ASTREE_huge_val -> __astree_huge_val
* __ASTREE_huge_valf -> __astree_huge_valf
* __ASTREE_huge_vall -> __astree_huge_vall
* __ASTREE_malloc -> __astree_malloc
* __ASTREE_memcpy -> __astree_memcpy
* __ASTREE_va_start -> __astree_va_start
The GUI offers automatic conversion of old directives via the Tools menu.
Rule checks
-----------
* For easier configuration and better understanding,
all rules and checks have been merged into a single view.
For each rule, you can now see all the checks used by it.
When enabling or disabling some aspect of a rule by toggling
a check, you immediately see which other rules are affected.
* The list of pre-defined filters in the Configuration view
has been extended by the rule categories of MISRA C and
MISRA AC AGC (Mandatory, Advisory, Obligatory, Readability,..).
* Header files are now only checked in contexts in which
they are actually included while preprocessing. This fixes
unjustified warnings about preprocessing problems in rule checking.
MISRA-C:2004
------------
* Added support for rule 16.10.
* Improved precision for rule 13.6 to eliminate false alarms.
* For violations of 19.15, the analyzer now reports the exact line
where a file is included twice.
* The check for rule 13.3 has been refined and now also takes several
patterns of indirect equality tests into account.
* Improved precision to eliminate false alarms about violations of rule 8.9.
* Fixed rare false alarms for rule 19.15.
* Improved coverage of rule 18.4 by adding a check
that warns about union objects.
MISRA-C:2012
------------
* Added partial support for rule 8.13.
* Corrected check for rule 2.5. Macros defined in the preprocessor settings
are no longer subject to the rule check "unused-macro".
* For violations of Dir. 4.10., the analyzer now reports
the exact line where a file is included twice.
* Improved coverage of rule 19.2 by adding a check
that warns about union objects.
Extensions of the DAX format
----------------------------
* Incremented the version number to 1.1.
* The elements "options", "abi", and "parser-ignore" now support
importing settings from other DAX files. This is done using
the optional "import=<file>" attribute.
* Model link settings for code generated via TargetLink
or EmbeddedCoder can now be specified in DAX files.
* It is now possible to refer to environment variables in text nodes
and attribute values of DAX files. Here is an example which evaluates
two environment variables YES and VAR:
<dax version="1.1">
<files use-relative-paths="${YES}">
<file>${VAR}.c</file>
</files>
</dax>
* Improved the rule checker configuration in DAX files.
Instead of using the now-deprecated "rules" and "checks" options,
they can now be specified in a new <rulechecks> section
as shown in the example below:
<dax version="1.1">
<options>
<rulechecks>yes</rulechecks>
</options>
<rulechecks>
<checks enable="all">
<array-index>no</array-index>
</checks>
<rules enable="none">
<M04>yes</M04>
<M04.12.1>no</M04.12>
</rules>
</rulechecks>
</dax>
Additional values can be passed where needed using the following syntax:
<dax version="1.1">
<rulechecks>
<rules enable="none">
<M2012.6.1 value="char;int">yes</M2012.6.1>
</rules>
</rulechecks>
</dax>
* The ABI section now supports loading one of the predefined ABIs.
Individual settings from this ABI can still be overwritten. Here is
an example which loads the ABI for 32-bit Intel x86 but overrides
the setting for sign of bitfield:
<dax version="1.1">
<abi target="ia32">
<bitfield_sign>signed</bitfield_sign>
</abi>
</dax>
If the target option is omitted, Astrée uses the analyzer
default ABI settings that are specified in the user manual.
* The server-side reference file for inserting AAL annotations
can now be exported via Annotations → Advanced and referenced
in DAX files via the "reference" option of the <annotations>
tag. Example:
<annotations file="annotations.aal"
reference="reference.aalref"/>
Note that the reference file is specific to the version
of the Astrée server and the operating system it is running under.
It may need to be re-generated when uploading it to a server
with a different version number or running under a different OS.
Integration with dSPACE TargetLink
----------------------------------
* Added support for TargetLink 4.0.
* The Toolbox for TargetLink now also considers
the IncludeFileSearchPath and SourceFileSearchPath properties
of the data dictionary. Paths listed in IncludeFileSearchPath
are added to the list of include paths for preprocessing,
and C source files from paths listed in SourceFileSearchPath
are added to the files to analyze.
* It is now possible to specify an additional script or executable
for post-processing files generated by the "Import Data Dictionary".
Post-processing is applied to the generated "Wrapper and stubs"
as well as to the "Annotations" file. The script can be specified
either in the Toolbox or in the "Code generators" view.
* The DD import now also generates directives for ranges
of calibrateable struct components.
* Improved handling of interpolation routines.
* Added new configuration elements to specify top-level subsystems
for which calls are generated in the analysis wrapper. This is useful
if a subsystem’s code is called by a top-level subsystem (e.g.
when using model referencing). The new configuration elements are
"data_dictionary_toplevel_subsystems" in XTC, "<toplevel_subsystems>"
in DAX, and "Code Generators" -> "Import Data Dictionary" in the GUI.
* The "MATLAB script" field in the Astrée preferences
now also accepts MATLAB script code (e.g. a function call)
instead of just the name of a MATLAB script file.
Options and ABI
---------------
* New options:
* keep-float-specials
configures the treatment of infinities and NaN. If disabled (default),
the analyzer behaves like in previous releases, i.e. it warns about
such values and discards them before continuing with the analysis.
If the option is enabled, the analyzer omits such warnings and instead
keeps the special values. This mode of operation is useful for modeling
targets on which floating point special values do not raise exceptions,
e.g. quiet instead of signaling NaN.
* dynamic-smash-variables-threshold=n
allows to specify a maximum number of variables to which a pointer
may refer before those variables are smashed, i.e. represented
by a single abstract object.
* automatic-partition=[yes|no]
controls all automatic partitioning heuristics. This option
has no influence on user-defined partitioning directives,
in contrast to the option "partition=[yes|no]".
* warn-read-of-never-written-variables
enables warnings about read accesses of global or static variables
which have neither an explicit initializer nor a previous assignment.
Such reads are reported as class D alarms.
* --export <archive>
batch mode option for exporting the analysis configuration and results
as an .aaf archive at the end of the analysis run.
* The alignment of char arrays can now be configured via the new ABI
setting ">alignof_char_array". The default value is 1.
* The option "warn-on-uninitialized" has been deprecated.
Warnings about accessing uninitialized variables with automatic storage
duration (local variables) are now always enabled. Such accesses are
reported as class A alarms.
Uninitialized local variables have sometimes been used for generating
full-range intervals in user-defined stub function, typically following
this pattern:
/* stub function: returns a random character */
char random (void) { char c; return c; }
This pattern will now always lead to a class A alarm.
Stub functions of this kind should be rewritten as follows:
char random (void)
{ char c; __ASTREE_modify((c; [-128, 127])); return c }
The modify directive acts like an assignment that initializes
the variable with the specified range. The C stub library that
is shipped with the tool has been corrected in this manner.
* Fixed import of a partial list of rule checks from an options file
so that already configured rules are no longer overwritten.
* The different kinds of analysis settings (options, ABI, etc.)
can now be imported from and exported to the DAX format. Files
with analysis settings in old formats (.opt, .abi, etc) can still
be imported but are no longer exported by the GUI. For options
and rules, the new DAX export allows either a full export of all
options and rules or alternatively the export of only those options
and rules that have been explicitly modified, i.e. that deviate
from the tool's default settings.
Configuration
-------------
* The views for the analyzer options, rule-checker options and ABI
have been restructured and unified. The new view is available via
"Analysis configuration" -> "Settings" in the project toolbar.
It now provides the same look and feel for all configuration items
and a filtering mechanism for faster lookup of specific options,
rules, or ABI settings.
* The ABI configuration view now displays the target that has been
selected from the list of predefined targets. Only explicit deviations
from the selected target are highlighted.
Code browsing
-------------
* Functions defined in a preprocessed file can now be listed directly
in the Files list in the main navigation panel. This enables
easier and faster navigation of large files.
* The editor view now highlights matching parentheses and braces
when positioning the cursor in front or behind such characters.
* The preprocessing view now distinguishes two modes of operation.
By default, the view allows to configure and start the built-in
preprocessor. When using an external preprocessor instead, the view
can be switched into a new mode by unchecking the new option
"Use the built-in preprocessor". In this mode you can enter
the include paths and defines that were used by the external
preprocessor. This information is then used for locating
the original source files and for configuring the rule checking
on those files.
Result Viewer
-------------
* More fine-grained filtering of the alarms to be displayed.
The number of currently visible alarms is shown.
* The Viewer now lists unused comments, i.e. comments that no longer
refer to alarms. Such comments typically come about when the code
under analysis was modified before re-running the analysis. You can
now move them to the corresponding alarms in the new analysis run,
or delete them outright.
* It is now possible to comment alarms which are raised
by directives (e.g. __ASTREE_assert) that have
been inserted via AAL annotations.
* Comments imported via DAX in batch mode are now visible
in the Result Viewer after a batch analysis.
Output
------
* The output and report files no longer list all analyzer settings,
but rather either:
1. only the settings that deviate from the default,
i.e. have been modified by the user in the GUI,
or
2. only the settings that are listed in a .dax or .opt
file when running the analysis in batch mode.
* When preprocessing files with the built-in preprocessor,
the invocations of the preprocessor and its outputs are now part
of the analysis log. They can be found in the "Output" tab of the GUI
and the text report file.
* In the editor, the currently displayed tooltip can now be copied
to the clipboard with Ctrl+T.
* The code metrics view and report have been extended by a Location column
which holds the locations of functions for which the metrics are given.
Precision
---------
* The new domain of distance to zero for floats allows for a more precise
analysis when dividing by a float that can be positive or negative.
It detects if the absolute value of such a variable is far enough
from zero so that overflows can be excluded. This prevents some
false alarms about floating-point divisions which were raised
by previous versions of Astrée.
* Added a new interpolation domain for a more precise analysis of typical
interpolation routines (e.g. as generated by the TargetLink code generator),
resulting in fewer false alarms about potential run-time errors.
The new domain can be enabled by the option "interpolation=yes".
* Improved the precision when logical expressions appear inside comparisons,
such as in
if((a < 0) == 0)
* Improved the precision of the analysis for possible ambiguities
due to side effects in expressions.
Directives
----------
* It is now possible to assign absolute addresses to variables
with incomplete type as in the following example:
unsigned char* rom[];
unsigned char* rom_end[];
__ASTREE_absolute_address((rom, 0x1000));
__ASTREE_absolute_address((rom_end, 0x2000));
size_t rom_size = rom_end - rom;
* New directive __ASTREE_alarm for raising alarms in stub functions.
The directive can be used to raise any kind of alarm with a freely
configurable message text. Moreover, the alarm can be optionally
reported at the location where the stub function is called,
rather than at the location where the directive is inserted.
Here is an example from the new OSEK stub library:
__ASTREE_alarm((raise_at_caller;
invalid_usage_of_os_service;
"invalid call to ReleaseResource
(resource has not been acquired)"));
C frontend
----------
* The analyzer now allows the linking of functions that are declared
with incompatible types in different compilation units.
Hence, the following AUTOSAR-compliant code can now be analyzed:
/* file1.c */
typedef int T;
void f(T* p) { }
/* file2.c */
typedef int T[8];
void f(T*);
void main (void)
{
int a;
int* pa = &a;
f(pa);
}
* Flexible array members are now supported,
i.e. types of the following kind are accepted:
struct S {
int a;
int b[];
};
* The analyzer now accepts empty struct declarations as extension,
i.e. declarations of the following form are accepted:
struct S {
int a;
; /* empty struct declaration */
int b;
};
* Old GCC-style designated initializers are now accepted,
e.g. { x: 42 }, which behaves the same as { .x = 42 }.
* The analyzer now handles more variants of GCC-style
inline assembler automatically.
Libraries and stubbing
----------------------
* The C stub library for Astrée now supports all
ABI configurations that are supported by the analyzer.
The built-in preprocessor automatically configures
the library according to the specified ABI settings.
* Automatically generated stub functions are no longer considered
for reached-code statistics as they are not actually part
of the analyzed code.
Report files
------------
* The types of alarm comments are now printed in a separate column
in summary report files.
* XML summary report files can now link each alarm to the model link
HTML file containing the source code for which the alarm was raised.
This requires a proper configuration of the display of model link files
via "Code generators" -> "Model link".
* Missing directories for report files are now created automatically
if possible.
Other modifications and improvements
------------------------------------
* Fixed a known issue from release 15.04 where importing projects
created with release 14.04i, 14.10, or 14.10i would in rare cases
crash the server.
* Fixed the printing of string constants when using the option
"dump-source" or the scenario builder. This fixes another
known issue from release 15.04.
* The analyzer now also warns about potential ambiguities due to
side effects on function-local static variables.
* Fixed cases of missing and misclassified declarations when searching
for identifiers in the Search tab of the GUI.
==============================================================================
Last modified on 9 October 2015 by alex@absint.com.
Copyright 2015 AbsInt. www.absint.com
==============================================================================
An HTML version of these release notes is available at
www.absint.com/releasenotes/astree/15.10