Astrée Release 17.04
--------------------
Standalone RuleChecker
----------------------
RuleChecker and Astrée can now be used separately.
This is implemented as follows.
▲ The product "Astrée for C" is replaced by the framework "a³ for C",
which contains the two analyzers Astrée and RuleChecker.
This renaming affects:
△ the installation packages
△ the names of the client, server, and server-controller executables
△ the names of Qualification Support Kits
△ the report files
▲ Analysis projects can now be created in one of two modes:
1. Astrée mode
for finding runtime errors, with the usual powerful user interface,
optionally invoking RuleChecker if you wish
2. RuleChecker mode
for finding violations of coding rules and compiling code metrics,
with a simplified GUI, without running Astrée
Note that invoking RuleChecker in the Astrée mode
maximizes precision on semantical rules.
▲ License files for previous Astrée releases are incompatible
with this release. All customers with active support have been emailed
new license files. Contact support@absint.com with any questions.
▲ The release notes for RuleChecker are now published separately as well.
See www.absint.com/releasenotes/rulechecker_release_1704.html.
Improved performance
--------------------
▲ Reduced analysis time for do-while loops.
▲ Reduced memory consumption when analyzing code with many function calls.
▲ Optimized GUI performance on huge analysis projects.
▲ Improved performance when loading very large projects on Windows.
▲ Reduced memory consumption during preprocessing, in both GUI and batch mode.
Improved precision
------------------
Improved precision for:
▲ strict comparisons on floating point variables in the octagon domain
▲ analyses with the option warn-on-field-overflows enabled
▲ evaluating comparisons between overflowing pointer expressions and NULL
▲ the Gauge domain for loops, enabled by the option gauges=yes.
For example, given the loop
for (unsigned K=30, N=15; INPUT < K/2; K-=2)
N--;
it can now prove that the loop terminates and thus N and K cannot overflow
if the float variable INPUT is known to be larger than or equal to 1.0.
General improvements
--------------------
▲ When subtracting two pointers to different memory blocks and one of them
is the NULL pointer, the analyzer now warns about both issues in a single,
unified alarm message. Here is an example for subtracting a pointer pointing
to a variable x from the NULL pointer:
ALARM (A): subtracting pointers on different
memory blocks { NULL } and { x }
▲ The analyzer now also detects misaligned memory accesses on variables which
are known to be intentionally allocated to misaligned absolute addresses.
Assuming that the char array a is allocated to the address 1001, Astrée
will detect that *(unsigned short*)(a + 3) accesses an aligned address
but *(unsigned short*)(a + 2) does not. For the latter, it now produces
the following alarm message:
ALARM (A): invalid dereference: misaligned memory access at 1001 + 2
may not be a multiple of 2
▲ Accesses to address 0 no longer stop the analyzer with an error if 0
is explicitly declared as a valid absolute address:
__ASTREE_absolute_address((int, 0));
▲ Optimized the analyzer to more precisely determine floating point bounds
close to 1e50.
▲ Improved the notifications about ambiguities due to side effects
in expressions. They are now more precise for assignments of the form
lhs = f(..) where lhs has no read accesses and f(..) is a function call.
▲ Invalid array size expressions (with a constant value ≤ zero)
no longer cause the analyzer to stop with an error message. Instead
all such arrays are assumed to be of size zero. The diagnostic rule A.1.2
detects and reports such invalid array definitions.
▲ When ignoring the return value of a function by (incorrectly) assuming
a void return type, the analyzer no longer stops with a definite
runtime error. Instead, the error is reported and the analysis continues
with the assumption that the return value of the function is ignored.
▲ The analyzer no longer stops with a definite runtime error
in function calls that assume a non-pointer return value although
the called function has return type void. Instead, the error is reported
and the analysis continues with the assumption that the return value
is not initialized and contains arbitrary values.
▲ Fixed false alarms about "Reinterpreting incompatible parameter type
in a function call" in function calls using a plain char type but expecting
an explicitly (un)signed char type, and vice versa.
▲ The octagon abstract domain is now used to:
△ show the absence of division by zero over floats
△ the absence of overflows in memcpy, bzero,
and array accesses through pointers (as in p[i] where p is a pointer)
▲ Fixed the interpretation of character constants with values > 127
in case of using the ABI settings char_sign=yes and bits_of_char=16.
▲ Astrée now supports the explicit allocation of variables into existing
memory blocks using absolute address directives. In such cases, it also
supports expressions that access several adjacent variables:
unsigned char a, b;
/* allocate memory for a and b */
__ASTREE_absolute_address((char[2], 0x150));
/* allocate a into existing memory block */
__ASTREE_absolute_address((a, 0x150));
/* allocate b into existing memory block */
__ASTREE_absolute_address((b, 0x151));
unsigned short f(void) {
return *(unsigned short*)&a; /* Read both a and b */
}
▲ Multiple declared variables with incompatible types are now
initialized consistently, independent of the parsing order of files.
Note that such declarations constitute constraint violations
and violate the diagnostic rule A.1.1.
Qualification Support Kits
--------------------------
▲ 13 additional test cases for Astrée
and 26 additional test cases for RuleChecker.
▲ Consistency checks for XML result and XML report files.
C frontend
----------
▲ Fixed an issue that could cause the frontend to abort with error
when enabling the option anonymous-global-structs-and-unions.
▲ The C frontend no longer prints unjustified warnings about type
incompatibility for variably modified array types when mixed with
constant size array type.
int a[10];
int n = sizeof(a) / sizeof(*a);
int (*q)[n] = &a; /* this line no longer triggers a warning */
▲ Global __asm and __asm__ statements are now also handled automatically.
It is no longer necessary to define parser filters to remove such statements
from the code.
▲ The frontend now accepts differences of address constants with
the same base in integer constant expressions, e.g. &g[1] - &g[0].
Such expressions, which are supported by some compilers, are still reported
as violations of MISRA-C:2004 rule 1.1 and MISRA-C:2012 rule 1.2.
▲ The frontend now accepts parameters with variably modified type, e.g.
int f(unsigned x, int (*p)[x])
▲ Shortened error messages about incompatible types
if the types involve structures.
▲ Function filters now only match whole identifiers.
Thus the feature now behaves exactly as documented.
Original-source frontend
------------------------
▲ The analyzer no longer issues unjustified warnings
if the ## operator is followed by an empty macro parameter.
▲ Consistent handling of repeated expansions of a macro M defined as
#define M N
#define N() some_expansion
New project wizard
------------------
The wizard now simplifies the setup of analysis projects in all the different
modes: Astrée, RuleChecker, and Astrée + RuleChecker.
Preprocessor view
-----------------
▲ You can now preprocess a subset of the original source files
by selecting them and using the context menu.
▲ Likewise, you can select a source file and use the context menu
to exclude the corresponding preprocessed file from the project coverage.
Editor view
-----------
A line with more than one finding is now marked by a special icon.
The number of findings is shown when hovering over it.
Findings view
-------------
▲ Lines from this view can now be copied to the clipboard.
▲ The Home and End keys now let you jump to the first or last
entry in the findings table.
▲ Double-clicking on the Comment column for rule violations
lets you comment on them in the original source code.
Overview → Filter view
---------------------------
▲ Added a button for resetting the filter to its default settings.
▲ The layout of the widgets can now be changed between horizontal and vertical
via a button in the toolbar.
▲ New Findings/Classification tab that lists the number of reported alarms
for each file and function together with their classification (uncommented,
undecided, true or false).
Analyzer → ABI view
------------------------
Fixed the "Reset to analyzer defaults" action which in some cases would not correctly
reset the ABI settings.
Analyzer → Options view
----------------------------
Reorganized the options to clarify which ones affect both Astrée and RuleChecker,
and which affect only one of them.
Parser view
-----------
▲ Identifiers and regular expressions specified in the "Patterns
to ignore" tab now accept an optional replacement text. If specified,
matching patterns are replaced by this text instead of just being filtered.
▲ Entries in the list of "Patterns to ignore" can now be disabled
from the context menu.
Analysis history and differences viewer
---------------------------------------
▲ New dialog for providing a description when creating a new revision.
▲ Descriptions of leaf revisions can now be edited from the history tree.
▲ Fixed an issue that under Windows could lead to some revisions missing
in the Differences viewer.
DAX export/import
-----------------
▲ Improved the DAX export of nested preprocessor configurations
with relative base directories.
▲ The DAX export of the GUI no longer exports the output directories
of the Preprocessor view to increase the compatibility of DAX files
exported on other machines.
Search
------
The identifier search now allows searching for struct/union member declarations
and distinguishes between member reads, writes, taking the address of a member,
and using it in a directive.
Slicing
-------
The dialog for starting the program slicer now allows selecting a variable
that is written in the current expression.
Control Flow view
-----------------
This new view displays the function calls in each process.
Data Flow view
--------------
▲ When using the Data flow view in the output area to investigate
data races, the context-menu function "Display findings" now narrows down
the relevant findings not only to a certain variable but also to
a certain function in which the variable is accessed.
▲ The Data Flow view in the output area now also displays the location
of each access to each variable for all processes under which the access
may occur.
Overview → Data Flow view
-------------------------
For each variable, this view now also displays the number of distinct locations
at which it is read or written.
Overview → Filter view
-----------------------
This view affects the information displayed in Overview → Data Flow.
Call Graph view
---------------
The call graph view now also allows searching for arbitrary substrings
of function names.
Watch view
----------
Fixed cases of missing invariants for statements.
Annotations view
----------------
▲ Added a horizontal scrollbar when annotations exceed the available space.
▲ When Astrée reports alarms for a directive (e.g. an __ASTREE_assert)
that was introduced via an AAL annotation, it is now possible to invoke
the context menu on either the displayed directive in the code or
on the corresponding entry in the Annotations view, and select the new
action "Display findings", which then displays the list of alarms reported
for that directive.
▲ The Annotations view now also displays comments for annotations, e.g.:
main { +1 statement}
insert before : __ASTREE_print(("start"); /*This is a comment.*/
Diagnostics
-----------
Diagnostics messages formerly issued as errors or notifications (e.g.
C constraint violations) are now covered by the new rule set "A. Diagnostics".
Make sure to enable this rule set for all Astrée analysis projects.
For old analysis projects specified in DAX, the new diagnostics can be enabled
by adding the following section to the DAX file:
<rulechecks>
<rules enable="none">
<A>yes</A>
</rules>
</rulechecks>
Text report
-----------
▲ More compact tables for reached, not reached, and stubbed functions.
The suffix "[at location]" at the end of each line is now omitted.
(The lines are still linked to the corresponding source code locations
in the GUI’s Output view.)
▲ The wording of two lines in the summary section has changed to clarify
their meaning:
△ "Alarms on code locations" → "Code locations with alarms"
△ "Alarms on memory locations" → "Memory locations with alarms"
▲ Code metrics are now included in the text report file:
/* Project metrics */
|-----------------|
| Project metrics |
|-----------------|
| RPATH | 0 |
|-----------------|
/* File metrics */
|----------------------------------------------|
| File metrics | CDFILE | LINE | FUN | PLINE |
|----------------------------------------------|
| src/Func1.c | 0.00 | 19 | 1 | 16 |
| src/Func2.c | 0.00 | 34 | 1 | 31 |
| src/Func3.c | 0.00 | 13 | 1 | 8 |
|----------------------------------------------|
/* Function metrics */
|------------------------------------------------------------------------------------------------------------------|
| Function metrics | CYCL | RETURN | GOTO | STMT | PARAM | MLINE | LEVEL | PATH | CALLS | CALLING | LSCOPE | CDFUN |
|------------------------------------------------------------------------------------------------------------------|
| Func1 | 2 | 2 | 0 | 7 | 2 | 13 | 2 | 2 | 0 | 2 | 1.94 | 0.00 |
| Func2 | 6 | 3 | 0 | 16 | 2 | 28 | 3 | 18 | 2 | 1 | 2.31 | 0.00 |
| Func3 | 2 | 2 | 0 | 5 | 1 | 5 | 2 | 2 | 0 | 1 | 1.62 | 0.00 |
|------------------------------------------------------------------------------------------------------------------|
▲ The Compressed Report file is no longer available.
XML report
----------
The XML report file now also contains code metrics, if the option metrics=yes
was enabled for the analysis.
Custom reports
--------------
▲ In addition to HTML, the reports can now also be output as plain text
or CSV. The output format is specified in DAX via the new attribute
format=html|text|csv.
▲ The Metrics View and the Metrics section in the configurable report
no longer list functions for which no metrics are computed by the analyzer
(e.g. unused static functions).
▲ Modified default headers for some sections in the configurable reports
to clarify their meaning.
▲ The files filter for custom reports now also affects the information
listed in the Data Flow section.
▲ The Data Flow section now shows the location of each access to each variable
for all processes under which the access may occur.
▲ It is now possible to specify the column to sort
the Data Flow information by.
▲ Custom reports may now contain information about the function calls in each
process as displayed in the new Control Flow view of the GUI.
▲ The former Summary reports have been replaced by predefined custom reports.
Summary report files specified in DAX version 1.3 or earlier are
automatically converted into the corresponding new custom reports.
The Summary Overview report file is no longer available.
▲ New variables for use in report headers and file names:
△ %REPORT_TYPE%
△ %FILE_TYPE%
△ %PROJECT%
△ %REVISION%
△ %USER%
△ %VERSION%
△ %BUILD%
△ %MODE%
▲ Improved the reporting of data races in the custom reports.
▲ The file filter in the custom-report configuration now also affects
the data race section so that only data races in the selected files
are listed.
▲ The report configuration can be included in the report,
either by including the whole configuration or by referring
to the configuration name.
▲ Added optional number of reported alarms for each file/function
in the project together with their classification.
Extensions of the DAX format
----------------------------
▲ New DAX version 1.4.
▲ The new project modes can be specified inside the <dax/> tag:
<dax mode="rulechecker" version="1.4"> ... </dax>
<dax mode="astree" version="1.4"> ... </dax>
If not specified, the mode defaults to "astree".
▲ Modified attributes of the <parser-ignore/> tag:
△ the file attribute used to import .par files from older Astrée versions
is no longer available
△ it is now possible to specify a replacement
using the new attribute "replacement"
▲ In the custom report configuration, the tags that can appear
inside the <findings/> tag have been renamed as follows:
DAX 1.3 DAX 1.4
<alarms/> <include-alarms/>
<errors/> <include-errors/>
<notifications/> <include-notifications/>
▲ DAX files referenced by the import attribute of the <abi/> tag
are now allowed to import an ABI from yet another DAX file.
▲ An entry in the <patterns-ignore/> section is now ignored
if it contains the new attribute enabled="no".
▲ The attribute coverage-ignore="yes" for <file/> tags
in the <preprocess/> section allows to exclude the corresponding
preprocessed file from the project coverage.
▲ The new tag <include-configuration mode="contents"|"name"/>
controls the inclusion of the report configuration in custom reports.
▲ The new key <alarm-classification> in the custom report configuration
controls the output of the number of reported alarms for each file/function
in the project together with their classification.
Preset option profiles
----------------------
You can now pick from several option profiles to automatically set
the most appropriate options accordingly. The following profiles are available:
▲ Setup (fast)
▲ Setup (normal)
▲ Analysis (fast)
▲ Analysis (medium)
▲ Analysis (normal)
The Setup profiles are a good choice for initial analysis runs to help you
check and complete the setup. The Analysis profiles can then be used
for final analysis runs, with different levels of precision.
New options
-----------
▲ generate-undeclared-absolute-addresses
With this option enabled, accessing an undeclared absolute address will raise
an alarm but the analysis will continue assuming that the address is valid.
Once the analysis has finished, suggestions for __ASTREE_absolute_address
directives will be displayed in the Output view. This corresponds to
the analyzer’s behavior in release 16.10.
With the option disabled, the analysis stops for the current context
when accessing an undeclared absolute address. This corresponds to
the analyzer’s behavior in all releases before 16.10.
The suggested workflow is to set this option during analysis setup,
review the generated directives, copy them into the "wrapper and stubs" file,
and disable the option for subsequent analysis runs.
▲ separate-with-caller-stack-pointers
enables a context-insensitive analysis of functions that access pointers
to the caller stack.
▲ auto-unroll-size
controls the maximum number of statements of loops that can be subject to
heuristic loop unrolling (auto-unroll). The default value is 10.
▲ assume-unknown-pointers-are-valid
triggers the following effects when enabled:
△ The directive __ASTREE_initialize applied to a local pointer variable
changes an invalid pointer into a possibly valid pointer, so that
the analysis may proceed.
△ When a stub is generated for a function returning a pointer value,
then that pointer is assumed to be possibly valid (as with global pointers).
△ When no size is given for a global array, accessing the array
does not stop the analysis. The analyzer continues with the assumption
that the array may have any size.
△ If the option global-initialization is disabled and a global pointer
is read without being first written to, the analysis does not stop.
Instead, an alarm is emitted and the analysis continues with the assumption
that the pointer was either NULL or pointed to some unknown variable
not declared in the analyzed code.
Changes to existing options
---------------------------
▲ auto-generate-stubs
now also generates stubs for function pointer calls with unknown targets.
▲ partition-double-if
has been optimized to no longer partition double if-sequences
when the branches of the if are too big or when the conditions
don’t test the same variable.
▲ partition-array-access
now performs a less aggressive partitioning. In most cases this improves
the analysis performance with no noticeable loss of precision.
When desired, the old, more aggressive partitioning behavior can be
restored by using the new option aggressive-partition-array-access=yes.
▲ Optimized the heuristic for selecting functions to analyze
context-insensitively (separate-function=*). Analyses using
this heuristic can become faster and slightly less precise.
▲ The option global-initialization has two new sub-options
that offer better control over the zero initialization
of global objects without initializers:
△ tentative-initialization
controls the initialization of global objects with only tentative
definitions (i.e. only declarations without initializer)
△ extern-initialization
controls the initial value of global objects without initializer
and only 'extern' declarations
Disabling one of these options will cause the analyzer to assume
arbitrary initial values for such objects.
▲ The option ignored-source-files has been removed. Files to be checked
are now explicitly specified in the new RuleChecker configuration.
See also these release notes’ sections on DAX and rule checks.
Directives
----------
▲ The directive __ASTREE_suppress now also accepts "rules_category" as type,
causing all rule checks to be suppressed for the specified code region.
▲ The min_size parameter of the __ASTREE_partition_ranges directive
has been replaced by a new size parameter with slightly different semantics.
The analyzer now tries to adjust all partitions to exactly the specified size.
If the partitioned range cannot be exactly divided by size, remaining values
are collected in an additional partition with smaller size.
Please note that the size parameter can still be overridden by the
max_partitions parameter. That is, if the partitioned range divided by size
results in a number of partitions that is larger than max_partitions,
the analyzer will limit the number of partitions to max_partitions.
All of these partitions have approximately the same size, thus effectively
ignoring the size parameter. The new semantics of the size parameter
is particularly useful if a value needs to be partitioned in even intervals.
▲ The arguments of __ASTREE_alarm are now checked more strictly
during parsing to give immediate feedback about configuration issues.
Here are two examples of new error messages for invalid arguments:
Invalid directive (message argument missing or empty).
Directive is ignored at ...
Invalid directive (message argument not allowed with rule checker alarm).
Directive is ignored at ...
▲ The directive __ASTREE_partition_ranges((...)); now accepts
arbitrary constant expressions for its size and max_partition arguments.
▲ If an __ASTREE_assert assertion fails in multiple partitioning contexts,
only the contexts in which it failed are now reported.
▲ Removed restriction on the maximum number of created partitions
when explicitly specifying a maximum using the max_partition option
of __ASTREE_partition_ranges.
▲ __ASTREE_global_assert may now also be placed inside of function code
and thus can be applied to block-scope variables (like function-local
automatic or static variables).
Preprocessor
------------
▲ For the option "Use paths relative to destination directory…",
the default has changed from no to yes. This results in more compact
and stable file paths for modified destination directories.
▲ In nested preprocessor configurations, child configurations with an empty
base directory now inherit the base directory of their parent.
▲ Fixed the import of preprocessed files which could fail when the GUI
preference "Synchronize preprocessed files" was disabled.
▲ Preprocessing no longer issues warnings if the analyzed code redefines
standard C macros such as __STDC_VERSION__.
Stub libraries
--------------
▲ All defines in the OSEK stub library are now guarded and can be
overwritten by the user if needed. The OSEK main function can also
be disabled by a macro definition if it conflicts with a main function
in the analyzed code.
▲ For the C stub libraries wchar_t and wint_t, it is now possible
to override the types and related macros by defining the following macros
during preprocessing:
△ __ASTREE_WCHAR
△ __ASTREE_WINT
△ __ASTREE_WCHAR_MIN
△ __ASTREE_WCHAR_MAX
△ __ASTREE_WEOF
These macros are expected to expand to the desired definition
of the wchar/wint type or macro, respectively.
▲ The built-in preprocessor now also takes into account
ABI values inherited from a reference target when specializing
the C stub library.
Server
------
▲ The owner of an analysis project can now be changed
by the server administrator in the server controller.
▲ When deleting a user, projects that are marked private to that user
are also automatically deleted from the server.
▲ Fixed an issue that could lead to a reset of the current
analysis configuration when the client lost connection to the server
during a configuration transmit.
Integration with TargetLink
---------------------------
▲ The generation of Astrée report files can be disabled under Preferences
and via the M-script function SetStandardReports.
▲ For AUTOSAR projects, the initialization phase of the generated
analysis wrapper code now contains a call to Rte_Start.
▲ The Astrée Preference dialog allows to persistently store the setting
for the batch mode execution. The M-Script API function InvokeAstree()
optionally uses this stored setting if available.
▲ The AbsInt Toolbox allows to exclude TargetLink standard files
(simulation files and DSFxp library files) via the preferences dialog.
Bug fixes
---------
▲ Fixed the Windows installer for the Astrée client such that it installs
the OIL file converter for OSEK even if no server is installed.
▲ Fixed segmentation faults during startup on Linux installations
that use glibc versions < 2.5.16.
▲ Fixed an issue with the option exclude-signed-in-unsigned-overflows
which in rare cases caused the analyzer to crash.
▲ Fixed an imprecision that in release 16.10 caused unreachable return
statements containing function calls to not be reported as unreachable.
▲ Removed false alarms about out-of-bound array accesses when accessing
arrays of unspecified size.
▲ Fixed rare cases of missing value tooltips for (sub)expressions.
▲ Fixed an issue that caused comments of AAL annotations blocks
not to be loaded. Here is an example of such a block:
__ASTREE_annotation(( /* comment was not loaded and displayed */
...));
------------------------------------------------------------------------------
Last updated on 12 April 2017 by alex@absint.com.
Copyright 2017 AbsInt. www.absint.com
------------------------------------------------------------------------------
An HTML version of these release notes is available at
www.absint.com/releasenotes/astree/17.04