Astrée Release 16.04
--------------------
General
-------
* Red Hat Enterprise 5 is no longer supported. The minimum requirement
is now Red Hat Enterprise 6 (CentOS 6) or compatible distributions.
* In addition to the installer that requires administrator rights,
Astrée is now also available as a simple ZIP archive
that can be unpacked and used without installation.
* Improved support for displays with high dpi values.
* It is now possible to export a project with all its revisions
into a single .aaf file.
* The Safety Manual now also addresses Astrée's relation
to the safety standards IEC-61508 and Cenelec EN-50128.
* Automatic conversion of analysis projects from previous Astrée versions
to release 16.04 does not preserve the preprocessing configuration.
To circumvent this restriction, export the preprocessing configuration
to DAX using your old version and import the DAX file into your analysis
project after converting it to release 16.04.
Performance
-----------
* The analysis server can now handle a large number of analysis projects
and revisions more efficiently.
* Computing potentially shared variables is much faster now,
particularly for larger analysis projects.
* Faster loading of projects with many AAL annotations.
* Faster loading of comments for alarms.
* Faster generation of large report files.
* Optimized performance and memory consumption
when the option separate-function
is used in an analysis with multiple asynchronous tasks.
Analysis
--------
* The new Gauge domain infers linear relations between the program
variables and the loop counters and thus improves analysis precision
inside of loops. It is activated via the new option gauges=yes.
Additionally, it provides notifications about loops for which no upper
loop bound can be derived.
* More precise handling of NaN and infinities when the option
keep-float-specials is set.
* Fixed an exceptional abort of the analyzer that occurred in rare cases
when evaluating complex logical expressions.
* Generalized the built-in offsetof to accept member designators
that contain array designators, e.g. offsetof(struct S, arr[5][4].b).
* Improved precision on loops with side-effects in the test.
* Improved the precision of the pre-analysis for possible ambiguities
due to side effects in expressions involving assignments
of the form x = f().
* The analyzer now supports the use of enumeration constants as pointers
to absolute addresses. This allows the analysis of code like
__ASTREE_absolute_address((int, 0x1000));
enum { ADDR = 0x1000, };
...
*(int*)ADDR = 42;
C frontend
----------
* The C99 type _Bool is now supported.
* All kinds of K&R style function definitions are now accepted,
e.g. void f(i) int i; { ... }.
* Astrée now supports statement expressions (GCC extension), e.g.:
int f(void) { return 19 + ({ int x = 23; x; }); }
* Fixed interpretation of bitfields whose base type is specified using
typedef with the underlying type having an explicitly specified signedness.
* Added support for compound literals in global initializers.
* Astrée now accepts casts involving unnamed struct types
in expressions of the form ((T*)s)->f where T is an unnamed struct type.
* Astrée now accepts initializers for empty structs, e.g.
struct S {} s = {};
* Removed restrictions about the use of function pointers as parameters
(some cases used to be rejected by the C frontend).
Stub libraries
--------------
Added a new entry function OSEK_sequential_main to the OSEK stub library.
This entry provides an automatic sequentialized setup for OSEK projects
using an OIL configuration. It can be used to detect run-time errors
that already occur without interaction between the tasks.
Server
------
* Under Linux, all files in the server working directory are now
created with the default settings for file permissions of the user
who started the server.
* Improved registration of the server as a Windows service to ensure
a more reliable automatic startup of the server after restarting Windows.
GUI: side bar
-------------
The project side bar has been re-arranged to improve usability.
* The sections Local Settings and Server Settings have been
replaced by a Configuration section, with the subsections
Preprocessor, Parser, Analyzer, and Annotations.
* The new Results section contains the new Findings view
that replaces the old Result Viewer.
* The preprocessed file list now automatically shows the list
of functions in the currently displayed file for faster navigation.
* The wrapper-and-stubs file and the analysis entry point are now
configured by the new analyzer options config-file=filename
and analysis-entry=function-name, respectively.
The configured wrapper-and-stubs file appears at the beginning
of the preprocessed files list.
* The Wrapper Generator and Model Link settings have moved
to the Tools menu.
* The new Project Summary area provides more information
than before, listing the totals for errors, run-time errors,
data-flow anomalies, rule violations, data races, reached code,
and analysis duration.
* The traffic lights are now displayed horizontally
to better accomodate the more detailed Summary.
GUI: analysis results
---------------------
* Improved interactive tabular and graphical overviews for Findings
per category, Findings per file/function, Rule violations, Reachability,
Code metrics, and Data and control flow information.
* For faster access of individual results, the single button "Show results"
has been replaced by five buttons: Output, Findings, Not reached, Watch,
and Search.
* A new Findings view replaces the former Result Viewer.
All run-time errors and MISRA-C violations are listed here,
and can be classified or commented on.
The view can be filtered by various criteria, such as the type
of findings or a certain code line selected from the editor view.
Thus, this view also replaces the former Line Summary view.
* A new Not Reached view displays all code locations that have not been
reached by the analyzer.
* The lists in the Findings and Not Reached views can be filtered
in the Results overview and exported as CSV files to create custom reports.
Other GUI changes
-----------------
* New, highly efficient and scalable display of value ranges as tooltips
for variables in the editor view. The tooltips are now available
even if the export of invariants is disabled and include more information
than before, such as the return values of function calls. The tooltips
are enabled by default and can be disabled using the new option tooltips=no.
* The editor views for preprocessed and original source code
now offer back and forward buttons for fast navigation.
* In the Open Project dialog, analyses that have been marked
private by the current user are now indicated by an icon and
a remark in the Remark column.
* The verbosity of the output view can now be configured
right above the view rather than in the Preferences dialog.
* Improved identifier search now lists all variable definitions
(including tentative ones), any intrinsic function calls, and all
variables used in Astrée directives and intrinsic function calls.
* Generalized commenting on findings. In the new Findings view,
it is now possible to comment on findings for which annotations
containing type names are required.
* Comments for findings do not allow newline characters, backslashes,
or double quotes.
* In configuration views (ABI, Options, Rules), new context menu entries
allow to reset settings to their default values.
* The Annotations view now supports drag&drop for multiple annotations.
Alarms
------
* An alarm of type D is now raised for each detected definite infinite loop.
In older releases this would only issue a notification.
For intentionally infinite loops in stub libraries and generated
wrapper functions, the alarms can be suppressed using an annotation.
* Messages about failed assertion and check directives are now more verbose.
For example, an assertion of the form __ASTREE_assert((Y < 27));
will raise the following message if the analyzer cannot prove
that the specified condition always holds:
ALARM (A): assert failure __ASTREE_assert((Y < 27)) at ...
* Reports of erroneous constant expressions now include an exact description
of the error. For example, a declaration such as enum { A = 1/0 }
now raises the message
ALARM (A): division by zero
* New alarms now warn about integer and floating point constants
that are too large:
ALARM (C): signed long long integer constant '9999999999999999999'
not included in [-9223372036854775808, 9223372036854775807]
ALARM (C): floating-point constant '1.79769313488e+308'
not included in 64-bit floating-point range
* Data races are now reported as alarms of type B and counted
per memory location (i.e., per variable) rather than per code location.
Report files
------------
* The new summary report "Rule checks" documents the Rule Checker configuration
(active rules and checks) together with all violations. It can be generated
in batch mode with the option --report-rulechecks <filename>
or specified in DAX by the element <xml-rulechecks>.
* The XML report has changed in the following ways:
* the report is no longer generated on-the-fly,
only once the analysis has finished
* the report contains the list of all functions in the analyzed code
* the <coverage> section now also contains reachability information
per function
* alarm messages about potential data races also list the involved
memory locations (variables)
* Data flow and code metrics report files are now also available in batch mode.
They can be configured by the following command-line options:
* --report-dataFlowFunctions <filename>
* --report-dataFlowVariables <filename>
* --report-dataFlowProcesses <filename>
* --report-metricsLocation <filename>
* --report-metricsType <filename>
* The following information has been added to the Coverage summary:
* how many percent of each function have been analyzed
* the list of the program locations that have not been analyzed
* The differences viewer now provides an "Export to XML…" button
for writing a report file that lists the number of alarms sorted
by category for all compared projects or revisions. The result is
a table of the following form:
Name Description Revision Alarms Division by zero ...
my_analysis first 1 2 1 ...
my_analysis second 2 49 12 ...
Location information
--------------------
* Corrected the location information for write-after-write alarms.
It now refers to the left-hand-side of the assignment.
* Improved parser error location when encountering unrecognized
compiler-specific keywords in declarations.
* Improved location information for alarm messages, in particular
for rule violations. It is now more precise, reducing possible overlap
between code locations with alarms.
Misc
----
* Astrée now only displays the number of program locations
for which alarm and error messages are reported. It no longer
displays the number of messages themselves, which can differ
from the number of locations (e.g. if analyzing a program location
in different call contexts always leads to the same runtime error).
The information about the number of messages has been removed
from the Project Summary in the GUI, the XML report, and the XTC
result file. This simplification makes the results easier to understand.
The omitted information is typically irrelevant in practice.
* Files that could not be found when uploading original source files
to the server are now listed in the output view and text report file
before starting the analysis.
* The output view and report file now contain separate version information
and time stamps for the preprocessing and analysis stages.
* Detailed reachable code statistics per file are now also included
in the text report and output view of the analyzer. Example:
/* Reached functions */
| --------------------------------------------------------------------- |
| | Number of statements | |
| Reached functions (5/9) | total | reached | not reached | percent |
| --------------------------------------------------------------------- |
| strcpy_x | 5 | 5 | 0 | 100 % | at strcpy_x.c:66.0-72.1
| strcmp_x | 7 | 6 | 1 | 85 % | at strcmp_x.c:66.0-72.1
| malloc_x | 3 | 3 | 0 | 100 % | at malloc_x.c:66.0-72.1
| main | 4 | 4 | 0 | 100 % | at main.c:85.0-91.1
| Proc8 | 14 | 14 | 0 | 100 % | at Proc8.c:66.0-82.1
| --------------------------------------------------------------------- |
/* Not reached functions */
| --------------------------------------------------------------------- |
| | Number of statements | |
| Not reached functions (3/9) | total | reached | not reached | percent |
| --------------------------------------------------------------------- |
| memcpy_x | 3 | 0 | 3 | 0 % | at memcpy_x.c:67.0-72.1
| Proc3 | 6 | 0 | 6 | 0 % | at Proc3.c:66.0-77.1
| Proc1 | 13 | 0 | 13 | 0 % | at Proc1.c:66.0-88.1
| --------------------------------------------------------------------- |
/* Stubbed functions */
| --------------------------------------------------------------------- |
| | Number of statements | |
| Stubbed functions (1/9) | total | reached | not reached | percent |
| --------------------------------------------------------------------- |
| Func1 | 4 | 4 | 0 | 100 % | at strcpy_x.c:51.12-17
| --------------------------------------------------------------------- |
* Notifications and errors are now consistently printed with
a "NOTE" or "ERROR" prefix, respectively.
* The different rule checking phases now have dedicated
section headers in the analyzer output and text report.
Rule checks
-----------
* The New Project wizard now also supports configuring the Rule Checker.
* Simplified configuration of rule checks. The explicit option "rulechecks"
has been removed. Instead the Rule Checker is automatically enabled
if the set of rules to check for is not empty. The computation
of code metrics can now be enabled independently from rule checking
using the new option metrics=yes.
* The new summary report "Rule checks" documents the Rule Checker
configuration (active rules and checks) together with all violations.
It can be generated in batch mode with the option
--report-rulechecks <filename>
or specified in DAX by the element <xml-rulechecks>.
* New and better frontend for parsing original (non-preprocessed)
source files for rule checking. It is more robust and no longer
restricts the use of preprocessor directives.
* Descriptive texts for checks and rules, including the official
MISRA-C rule descriptions, are now displayed under "Settings" -> "Rules"
as well as under "Findings" -> "Details".
* With the new option allow-boolean-constants=yes, the Rule Checker
allows 0 and 1 constants to be used in boolean contexts.
Code like bool_t b = 1; then passes without violation
of the MISRA-C:2004 rule 10.1 or the MISRA-C:2012 rule 10.3.
* Boolean constants introduced as enumerators are now handled
as effectively/essentially boolean (MISRA-C:2004/2012)
if they are part of a typedef defining the boolean type.
* Fixed an issue that could cause the Rule Checker to not find the header
files of the C stub library and therefore stop with a parse error.
* Fixed check for violations of customer-specific coding rule X.A.5.19.
MISRA-C:2004
------------
* Added support for rule 20.3.
* The underlying type of the ! operator is now always Boolean.
* Fixed the reporting of MISRA-C:2004 violations in initializers
which caused violations of rule 10.1 to be reported as violations
of rule 10.2 and vice versa.
* Fixed false alarms about rule 10.1 and 11.3 in conjunction
with null pointer constants and array accesses.
* Fixed false alarms for check external-file-spreading
for rule 8.8 related to tentative definitions.
MISRA-C:2012
------------
* Added support for rule D.4.11.
* Added partial support for Directive 4.9.
* Rule 17.3 is now fully supported.
* New option allow-signed-constant-with-signed=[yes|no] controls whether
the essential type model is relaxed, such that constant expressions
of essentially signed type and non-negative value that are subject to
the usual arithmetic conversions (see ISO/IEC 9899:1999 §6.3.1.8)
are considered unsigned, if the other operand is essentially unsigned.
* Fixed false alarms about rule 10.3 in conjunction with explicit casts
using predefined types and explicit sign information (signed/unsigned
char/short/int etc.).
* Fixed false alarms for check external-file-spreading for rule 8.5
related to tentative definitions.
* Fixed false alarms about rule 10.4 and 11.4 in conjunction
with null pointer constants and array accesses.
Extensions of the DAX format
----------------------------
* Incremented the version number to 1.2.
* The ABI specification has been restructured. A sample DAX specification is:
<abi import="@ia32.dax" target="my custom abi">
<char_sign>signed</char_sign>
</abi>
The base ABI is imported from the file specified in the "import" attribute.
Any modifications, such as the different value for "char_sign" above,
are listed explicitly. In addition, the "target" attribute can be used
to specify a name for the ABI.
The base ABI can be imported from any DAX file, not only the predefined
ABIs shipped with the tool. A predefined ABI can be referenced either
by its absolute path or by its file name prefixed with an @, as above,
to make the specification installation-independent.
The file referenced by the "import" attribute must not itself reference
another ABI.
* The <original-sources> section has been removed.
Original source files that shall not be preprocessed by Astrée
must now be listed in a <preprocess> section that includes
<use-internal-preprocessor>no</use-internal-preprocessor>.
Included header files are then retrieved automatically and don't need
to be listed. The tags <replacements> and <strip-compilation-path>
from the <original-sources> section of previous DAX versions are now
available within the <preprocess> section. The <strip-compilation-path>
tag has been renamed to <strip-path>.
* New tag <private>yes</private> for marking analysis projects as private.
When importing a DAX file that uses this tag, the resulting analysis
project is marked as private for the user who imported the analysis.
Note that this tag must be removed before loading a DAX specification
as user "anonymous".
* When exporting parser settings, the Astrée client now adds the setting
<pragma-asm>yes</pragma-asm> to the DAX file if filtering of code blocks
enclosed between "#pragma asm" and "#pragma endasm" was enabled.
* The former top-level tag <entry> has been replaced by
<options>
<analysis-entry>function_name</analysis-entry>
</options>
* The wrapper and stubs file is now specified as follows:
<options>
<config-file>filename</config-file>
</options>
The specified file must also be added to the <files> list.
Updates to the TargetLink coupling
----------------------------------
* Added support for TargetLink 4.1.
* Improved the configuration of the Toolbox for TargetLink
by separating the preferred server connection settings
from other preferences. The server settings are now part
of the global configuration and don't have to be re-entered
when using the Toolbox with different models. All other preferences
can still be configured on the model level. Additionally, it is now
possible to specify a global set of preferences that act as a default
in case that no model specific settings are found.
* The new Astrée server settings dialog of the Toolbox provides
a dropdown that lists all installed versions of the Astrée client.
For each client version, a different server connection can be configured
and stored, pointing to an Astrée server that is compatible with
the selected client.
* In case of an incorrect server configuration, the generated XTC request
can be reloaded to correct the server settings and retry to start
the analysis, without having to go back to the Toolbox.
* Semantic support for TargetLink CTO arithmetic is now enabled
by default when the analysis is automatically launched from the Toolbox
(exclude-signed-in-unsigned-overflows=yes,
exclude-signed-negation-overflows-in-cto=yes).
* Bounds for floating point values are no longer rounded
to integer numbers by the DD converter.
* The C library stubs are now automatically excluded from the global
coverage statistics for analysis projects created by the Toolbox.
* The Toolbox now allows specifying a DAX file for automatic import
of analysis configurations.
* Improved API for automating Astrée analyses via M-script.
Configuration
-------------
* The internal preprocessor now supports automatic includes
which can be added to each preprocessing configuration.
Files listed as automatic includes are processed as if
they were included at the beginning of each primary source
file in this configuration. In DAX 1.2 automatic includes
can be specified as
<automatic-includes>
<automatic-include>string</automatic-include>
...
</automatic-includes>
* Preprocessing settings are now shared between clients.
Each configuration provides a base path which can be modified
in order to quickly adapted the settings to another client.
* Removed options:
* warn-on-fullrange
* dump-process-dataflow
The per-process data flow information is now automatically collected
if the option dataflow=yes is enabled.
* chrono
For debugging suspected analysis-time issues in analysis projects,
contact support@absint.com.
* export-disambiguate
The export of invariants is now always context-sensitive.
Context-insensitive invariants are still available in the new
tooltips, which are enabled by default.
* -u and --files
Automated batch mode analyses can be fully configured by DAX files.
* Options now enabled by default:
* dataflow
* auto-generate-stubs
* case-insensitive
* __ASTREE_initialize((v)) now has an effect when v is an array or
a structure. It initializes the whole array (or structure), and
in addition removes NaN and infinities from floating point values
when using the option keep-float-specials=no.
* __ASTREE_modify((v; full_range)) now also sets v to be initialized
when it is an array or a structure. In such cases, it doesn't add
NaN and infinities anymore when using the option keep-float-specials=no.
* OIL files for OSEK configuration specified in the preprocessing view
are now uploaded to the analysis server where they appear in the list
of original source files.
* Fixed an issue in the ABI settings view of the GUI that prevented
the modification of pointer sizes.
* Nested preprocessing configurations now correctly inherit include paths
and macro definitions from their parents.
* Fixed an issue that prevented the commenting of alarms
from the Wrapper and Stubs view if the wrapper contained
an __ASTREE_import(()) directive.
* Added a GUI preference that controls whether report files
are automatically updated after an analysis run.
* The synchronous execution model of Astrée supports
an upper bound for the effectively maximal iteration count
of infinite loops, to be used for the cyclic executive loop.
The bound becomes effective when using the directive
__ASTREE_wait_for_clock(()).
In previous releases, the analysis entry functions generated
by the wrapper generator and the TargetLink importer made use
of "__ASTREE_wait_for_clock(())" to bound the maximum execution
steps of the generated main loop. For the sake of clarity this
default has been changed so that no upper bound for the maximum
number of execution steps is implicitly assumed.
Both the wrapper generator and the TargetLink importer provide
a new option so that users can explicitly activate a maximum
loop bound with a user-specified value. The bounds can also be
specified via DAX by the new tag <max-clock> inside
the <wrapper> or <data-dictionary> tag.
* The syntax of suppress-source directives has been extended
to allow to cover the remainder of a file by omitting
the length argument. For example, the following directive
suppresses all rule checks for a source file when inserted
in the first line of said file:
/* ASTREE_suppress(0, , rules-category) */
* The intrinsic __astree_create_process accepts a name
as an (optional) last argument. That name is printed
in the output window and in the call graph and data flow view
when referring to that process.
Authentication
--------------
* Users can now change their passwords from within the client GUI
via "Project" -> "Change password...".
* Optionally, the client can now remember the user and password
for a server connection. In this configuration it is possible to run
the qualification support kit (QSK) even if the user "anonymous"
has been disabled by the server administrator.
* Authentication information provided via the option
--user username@password option can now be stored by using
the new option --remember-password. Subsequent connections,
whether in batch mode or via the GUI, then automatically re-use
the stored authentication information unless different information
is explicitly provided.
Analysis history
----------------
* Multiple revisions of a project can now also be compared
by selecting them in the Open dialog, right-clicking and
invoking Compare from the context menu. It is no longer necessary
to first open the analysis history graph.
* The analysis history can now be accessed via the Project menu.
The entry "Project" -> "History" -> "Show revisions…"
opens the history graph to display the currently existing revisions.
The entry "Project" -> "History" -> "Create new revision"
creates a new revision based on the currently opened revision.
The new revision is automatically opened.
Patch 1 (build 264466)
----------------------
* Fixed rule checking to prevent rule violations for source files
contained in the "List of source files to exclude from rule checks"
(option ignored-source-files).
* Fixed unfinished AAL conversion of comments and possible server crash
when the client disconnected during the conversion.
* Fixed error reporting of the original-sources parser so that it points
straight to the corresponding line in the source code if possible.
* Fixed the interpretation of macros that are passed on the command line
(e.g. -DFOO=bar) in the original-sources parser used for rule checking.
* Fixed a regression where settings imported via DAX reset existing settings.
* Fixed the parallel analysis mode to consider
the __ASTREE_max_clock directive.
* Fixed wrong highlighting of messages and not analyzed code
in the editors for original source.
* Fixed a file handling issue that could cause certain files
to be reported as unknown or not found during parsing.
* Improved fallback for generating AAL paths to prevent losing alarm comments.
* Optimized the partition-array-access heuristic to reduce
the memory consumption and analysis time on certain code.
* __ASTREE_comment directives that specify the type of alarm to comment
on now only affect alarm messages for exactly the specified code range.
__ASTREE_comment directives without an alarm type behave as before,
affecting all alarm messages anywhere within the specified code range.
This modification enables precise commenting on nested alarms
of the same type in the Findings view.
* The wrapper file is no longer subject to MISRA rule checks.
Patch 2 (build 265481)
----------------------
* Fixed the XML report generation in batch mode to output the correct
comment_kind attribute for commented alarm messages rather than "undecided".
* Optimized loading the Findings view for findings with a large number
of contexts.
* Previous versions of the analyzer might stop with the message
"NOTE: Direct flow changed to ⊥ during test in this context"
after encountering a comparison that involves a variable with a range
strictly right or strictly left of zero:
if (...)
x = 1.;
else
x = -1.;
y = x == 0.;
This issue has now been fixed. In older versions of release 16.04,
it can be worked around by using the option float-distance-to-zero=no.
* Fixed AAL generation for program locations after labels.
E.g., when generating paths like "case A: + N statements",
the value of N in the generated annotation was off by one.
* New command line option --preprocess-report-file <file>
for writing a plain text file that contains the preprocessor output
as displayed in the Preprocess view. The option is particularly useful
for observing the progress of the preprocessing phase in batch mode.
* The indentation-level rule check is now run before parser filters
on original code. This fixes the customer-specific rule X.A.4.8
in the presence of parser filters applied to line beginnings.
* Fixed rule check cast-implicit to not warn about implicit casts
on pointers that only concern type qualifiers. The check is used
in customer-specific rule X.A.5.44.
Patch 3 (build 265552)
----------------------
Fixed false alarm about customer-specific rule X.A.4.8 that was raised
for a multi-line comment when the last non-newline character before
the comment was a slash.
==============================================================================
Last updated on 20 June 2016 by alex@absint.com.
Copyright 2016 AbsInt. www.absint.com
==============================================================================
An HTML version of these release notes is available at
www.absint.com/releasenotes/astree/16.04