Astrée Release 16.10
--------------------
General
-------
▲ The Windows version now makes use of certain libraries
it did not rely on before. Should you get a message about
missing libraries on first startup, simply install
the Visual C++ redistributable from Microsoft:
https://www.microsoft.com/en-US/download/details.aspx?id=48145
▲ A free plugin is now available for automatic integration
of Astrée in Jenkins, the leading open-source automation server:
https://wiki.jenkins-ci.org/display/JENKINS/AbsInt+Astree+Plugin
▲ The alauncher executable is now used for automation of Astrée and a³
(running analyses in batch mode, e.g. within continuous-integration systems).
It provides a verbose --help.
▲ The Safety Manual now also covers regulations for medical devices,
in particular the FDA Principles of Software Validation.
▲ The Safety Manual now describes qualified tool workflows for Astrée and a³.
▲ This stable release incorporates the changes
previously released as intermediate patches for release 16.04.
The corresponding release notes are available at
https://www.absint.com/releasenotes/astree/16.04/#patches
Performance
-----------
▲ The analysis precision has been improved in several ways:
△ Modified the widening strategy for higher precision.
△ Improved precision of casts from integer to floats
when the integer is known not to be 0.
△ More precise reachability information for expressions with side effects.
Expressions and statements that contain a sub-expression
that is non-returning -- e.g. a call to exit() or a compound
expression containing jump statements -- are not marked
unreachable anymore.
△ Higher precision for dynamically allocated memory when using
Astrée's function substitution feature.
△ Malloc call sites can now be distinguished using loop unrolling
directives. This leads to a more precise analysis of the values
stored in the dynamically allocated memory, and a finer tracking
of freed memory.
▲ Analyses no longer stop upon encountering undeclared absolute addresses.
Instead, all values written to any undeclared absolute addresses are
collected and used for any read to an undeclared absolute address.
In addition, when undeclared absolute addresses are encountered,
a list of suggested directives that would cover such accesses is provided.
▲ Modified the iteration scheme for parallel processes
to improve efficiency when analyzing asynchronous code.
▲ Fixed a widening issue that could cause very long analysis times
when iterating over asynchronous processes or context-insensitively
analyzed functions.
▲ Fixed analysis of expressions of the form
sizeof(&*a)
where "a" is of type "array".
Stub libraries
--------------
The OS stubs for OSEK now provide more efficient implementations
of the functions:
▲ EnableAllInterrupts
▲ DisableAllInterrupts
▲ SuspendAllInterrupts
▲ ResumeAllInterrupts
▲ SuspendOSInterrupts
▲ ResumeOSInterrupts
In addition, the effect of these functions is now more precisely
captured by the analyzer when the new Process priority domain is enabled
(precise-priorities=yes).
Server
------
▲ The server can now be locked in the server controller, such that
no further analyses can be queued or started. This is useful
e.g. when preparing for planned server shutdowns or upgrades.
▲ The server now also reports the license features that are enabled
by the configured license file. This information is written to stdout
as well as to the server log file.
C frontend
----------
▲ Reduced memory consumption when analyzing code that contains
many unused static or inline function definitions.
▲ Added support for linking incomplete and complete enum tags
to allow the forward declaration of enums.
▲ Type compatibility rules have been modified as follows:
△ arithmetic types of same size and signedness are no longer compatible
if they are not equal
△ the plain char type is no longer compatible with signed or unsigned char
△ function types without prototype are now compatible to function types
with prototype according to the conditions given in ISO/IEC 9899:1999
This modification affects incompatible type warnings of the C frontend,
as well as checks of MISRA-C:2004 rule 8.4 (type-compatibility) and
MISRA-C:2012 Appendix 1 rule 21.15 (memory-function-compatible).
Original source frontend
------------------------
▲ Added support for command-line macros with a replacement
starting with =, e.g. -DEQ===.
▲ Fixed argument substitution for operands of # and ##. The frontend now
takes the original tokens of the argument instead of the expanded ones
if the parameter instance is operand to one of the respective operators.
▲ The original source frontend now supports preprocessor macros like
#define B(X) X
#define A B
A(X)
where a macro name A expands to another macro name B
with the macro argument list for B lying outside
of the expansion result of A.
▲ The list of patterns to ignore (which is part of the parser configuration)
is now also applied to preprocessor directives in original source files.
Matching patterns are removed before checking coding rules.
Known issues
------------
▲ In order to update already existing preprocessed files on the server
after preprocessing, at least one of the following options must be set:
△ "Synchronize preprocessed files" under Project → Preferences
△ "Remove analysis files before importing preprocessed files"
under Configuration → Preprocessor
▲ In batch mode, the coverage information is missing from the XML result file
unless it is needed to generate some reports.
▲ When using the ABI option "rounding_mode=to_nearest", the analysis
might stop in some contexts when evaluating a guard expression
that involves a binary operation on floats.
▲ When using the option "exclude-signed-in-unsigned-overflows"
("Do not raise overflow alarms on unsigned computations with signed values"),
the analyzer might crash in certain scenarios.
The last two issues are fixed in Release 16.10 Patch 1 (build 271444).
GUI
---
▲ The new Data Flow view in the Results area displays all data flow
information collected by the analyzer. All accesses to global/static
variables are shown, with information about whether they are shared
or involved in a data race, what kind of access it is, and from which
function or process it originates.
The context menu in this view gives access to the corresponding
code locations.
You can interactively query the data flow information based on
a selection of relevant variables, functions, and processes.
These queries are applied as filters to the Data Flow view.
This is particularly helpful for identifying all processes
and accesses contributing to a data race.
▲ The Call Graph view can now show all possible call paths for accesses
to global variables. This feature is activated in the Data Flow view
via the context menu entries "Display in graph" and "Display variable
in graph". It is particularly useful when investigating shared variables
and data race alarms.
▲ An overview of analysis time broken down by different project parts
is now available under Tools → Analysis time. It can be
accessed as soon as the analysis has started and is updated on-the-fly.
▲ Improved Editor views.
△ Analyzed code lines without errors or alarms of type A, B, or C are
now marked in green. These lines are proven to be free of runtime
errors and data races under the assumptions made by the analyzer.
△ Exclamation marks denote code lines for which there are alarms
of type A, B, C, D, R, or other notifications. Clicking
on an exclamation mark takes you to the corresponding findings
in the Findings view.
△ The availability of invariants for display in the Watch view
is now denoted by blue line numbers rather than a blue bar.
▲ Improved filtering.
△ The files list in the Results → Overview → Filter
view can now be filtered for text strings or regular expressions.
△ The list of analysis projects in the "Open project" dialog
can now be filtered by pressing Ctrl+F.
△ Improved filtering in the Findings view now requires fewer clicks
for displaying the list of findings without comment.
△ The type filter in the Findings view is no longer reset to default
when starting an analysis.
▲ Improved wrapper generator.
△ You can now generate a wrapper with initialization functions only,
but without tasks.
△ For asynchronous execution models, the wrapper generator now
generates entry code that uses the analyzer intrinsic functions
__astree_create_process() and __astree_start_process()
instead of the no longer supported __ASTREE_asynchronous_loop directive.
Consequently, the wrapper generator takes an optional priority argument
for tasks and task entry functions can no longer take parameters.
△ The wrapper generator now warns before overwriting an existing
wrapper-and-stubs file. It then also offers the option of appending
the new code to the existing wrapper-and-stubs file, rather than
overwriting its contents.
▲ The Report view has been redesigned. Directories and file names
for report files can now be freely chosen, like in the DAX <report>
specification. Moreover, it is now possible to define and generate
customized HTML reports. For further details, see the Results section
of these release notes.
▲ Simplified the configuration of rule checks. It is now easier
to activate rules within deactivated sections and to enable
or disable categories of MISRA rules (Required, Advisory, etc.).
▲ Removed the extra stop button from the Preprocessing view.
The preprocessing can now be stopped by the stop button
in the toolbar that is also used for stopping the analysis.
▲ Improved value tooltips: for expressions of the form a->b
the GUI now displays not only a tooltip for the whole expression
a->b but also for the sub-expression a. Moreover, it now also shows
the values of indices in array accesses (e.g. a[i]) even if such
expressions appear on the left-hand side of assignments.
▲ The memory usage graph in the resource monitor now covers the entire
duration of the analysis.
▲ Improved the ordering of revisions in the result difference charts
of the Differences viewer. They are now ordered by analysis start time.
▲ Fixed loading original source files with file names containing
special characters (like é or ì).
▲ Improved responsiveness and reduced memory consumption
of the client GUI for analysis projects with millions of functions.
▲ Improved the import of AAL annotations. It now ignores all
annotation file contents that do not appear inside of an
__ASTREE_annotation block.
▲ If the DAX export option "ExportAll" is selected, the GUI now also
exports rules with parameters displayed as <empty>.
▲ When a location is highlighted in the editor, e.g. by clicking
on an alarm in the Findings view, the location is now centered
in the editor.
▲ Improved performance when commenting alarms in analysis projects
containing large files with many declarations.
▲ Improved error reporting in case of an expired license file.
▲ Removed the "Generate annotations" button from the Findings view.
Generating the annotations is now part of the Project → Save
action which is also accessible from the toolbar or via the global
Ctrl+S keyboard shortcut.
▲ The collapsed or expanded state of elements in the annotations view
is no longer reset by delete or insert operations.
▲ The "Copy part" mode for copying parts of an analyzer message
from the Output view can now also be entered by double-clicking on a line.
▲ The differences viewer for comparing revisions of analysis projects
now differentiates between the different kinds of findings:
runtime errors, data races, rule violations, etc.
▲ Fixed the global counter for memory locations involved in data races,
which is displayed in the Summary area. (In certain rare cases,
this number was too small.)
Improved and extended reports
-----------------------------
▲ New customizable HTML reports that can be configured in both the GUI
and in DAX. The configuration options provide all reporting features
of the XML summary reports and additional options that correspond
to the different operating modes of the Overview view in the GUI.
▲ The result summary in the analyzer log now also displays the number
of proven statements:
/* Result summary */
...
Reached code: 98 % (51/52 statements reached,
45/51 (88 %) statements proven)
...
A statement is proven if it is reached by the analysis
and does not cause an error or an alarm of type A, B or C.
▲ Error messages about incompatible types are now added
to the error summary counter of the analyzer, which is printed
in the text report and the Output view in the GUI.
▲ The analyzer now also outputs the patterns to ignore
and external declarations of the parser configuration:
/* Filter patterns */
function: asm void
identifier: __compiler_extension__
regexp: asm([^)]+);
identifier: asm
/* External declarations */
type: my_type;
declaration: my_type my_function(my_type, int);
▲ Improved reporting of potentially shared variables. The analyzer
now prints a detailed list of all variables that may be accessed
from more than one process. The corresponding option report-shared-variables
is now active by default.
/* Possibly shared variables */
'Process' at osek_stub.c:890.20-27
| read/written in Process 0: Task1 |
| read/written in Process 1: Task2 |
| read in Process 2: Alarm1 |
| read in Process 3: Alarm2 |
▲ Added new output of deadlock cycles and alarms about deadlocks.
ALARM (D): lock operation can cause a deadlock
(deadlock-cycle #1: process 0 locks 0, process 1 locks 1) at ...
ALARM (D): lock operation can cause a deadlock
(deadlock-cycle #1: process 0 locks 0, process 1 locks 1) at ...
The deadlock cycles that these alarms belong to are displayed
in the Output view of the GUI and in the text report:
----- deadlock-cycle #1: ----------
[ at ...
participant: [process 0, locked: {1} ] lock 0]
[ at ...
participant: [process 1, locked: {0} ] lock 1]
A deadlock cycle is a list of processes in a given state
trying to acquire a lock which is taken by another element of the list.
Each element of the list is printed with relevant context information
(call stack and position in the code where the lock is taken).
The new alarms and output are disabled by default and can be activated
by the new option warn-on-deadlocks=yes.
▲ Alarm messages about data races now indicate whether the access path
is volatile and atomic.
ALARM (B): write-write data-race on atomic access
in assignment 2 byte(s) at ...
Alarm messages with the additional information "on atomic access"
are exactly those data races that are not reported if the new
option warn-on-atomic-volatile-data-race is disabled.
▲ The parsing phase of the analyzer now ends with the line
Parsed X physical lines of preprocessed code
where X is the number of preprocessed source lines containing at least
one non-whitespace C token, excluding line directives and filtered code.
This line is also contained in the text report file.
▲ Alarms about "Wrong range of second shift argument" have been moved
from the category "Invalid ranges and overflows" to the new category
"Invalid shift argument". This modification affects the GUI and
the XML report file.
▲ Added a new category of alarms named "Overflow in conversion
(with unpredictable results)" for collecting float-to-integer conversions
that overflow the range of the target integer. The type of such overflow
alarms has been changed to A. After the overflow, the analyzer continues
with the full range of the target integer type.
▲ Astrée now raises additional alarms when comparing or copying
dangling pointers. The result of copying a dangling pointer is
an invalid pointer. For example, analyzing the following code
char* ptr = (char*)malloc(42);
free(ptr);
if (ptr != NULL) {
results in the alarm message
ALARM (A): use of dangling pointer { DANGLING: <memory-block> }
at <location>
where <memory-block> is the internal name of the memory block
that the pointer points to and <location> specifies the file,
line and column number where the pointer is used.
▲ The analyzer now distinguishes consistently between an expression
of the form &*e and its sub-expression e. If both expressions
raise alarms, these alarms will no longer be coalesced to the same
code location for the purpose of counting alarms per code location.
▲ Improved the display of invariants for bitfields in tooltips and
__ASTREE_log_vars to use proper names. That is, for code of the form
struct { char a:4; char b:4;} x;
x.b = 2;
the information for x.b is now displayed as x.b in {2}.
▲ The Astrée XML Result File format now has an XML schema definition file,
to be found at absint.com/dtd/astree-dax-report-configuration-16.10.xsd.
▲ Invalid AAL paths for alarm comments are no longer reported as errors,
but as notifications. The change was made because comments have no effect
on the program semantics assumed by the analyzer. Invalid AAL paths
used for inserting other directives are still reported as errors.
▲ The analyzer’s progress message for global iterations no longer
distinguishes between parallel and separate analysis modes. Here is
the new output for such iterations as displayed in the Output view
and text report:
global iter #5
global iter #5 (widened)
▲ The XML report now also contains the parser configuration,
i.e. the list of external declarations and patterns to ignore.
<parser_ignore>
<pattern type="function">foobar</pattern>
<pattern type="identifier">foo</pattern>
<pattern type="regexp">bar.*</pattern>
<pattern type="pragma-asm">yes</pattern>
</parser_ignore>
<external_declarations>
<external_declaration type="type">T;</external_declaration>
<external_declaration type="declaration">T x;</external_declaration>
</external_declarations>
▲ The XML report may now contain alarm messages without location information.
Currently the only alarms of this kind are violations of MISRA-C:2004 rule 21.1
and MISRA-C:2012 rule D.4.1 in cases where the rule check analysis-run fails.
▲ The message
NOTE: translate_warning(type): conversion from floating-point to integer:
from <TYPE> to <TYPE> at <LOCATION>
has been removed. Instead we recommend activating the MISRA-C:2012 rule 10.3
or the MISRA-C:2004 rule 10.2.
▲ If the right-hand side of a logical expression is reached by the analyzer,
it is now always properly marked as reached.
▲ Fixed the global counter for memory locations involved in data races
in the XML report file., i.e. the number given in the data_races attribute
of the <summary> tag. (In certain rare cases, this number was too small.)
Code metrics
------------
▲ Statement expressions (GCC compiler extension) are now taken into account
when computing metrics. In the computation of the metric "Language scope"
they are considered to be operators.
▲ The code metric LSCOPE (language scope) now also takes into account
the semicolon of null statements and statements in implicit control blocks
(like branches of an if statement that are not enclosed in brackets).
Standalone Rule Checker
-----------------------
Most of the supported MISRA rules can now be checked for
without running the runtime error analysis (skip-analysis=yes):
▲ The check for recursion now has two implementations with varying precision
that are chosen depending on the value of skip-analysis.
▲ The new check controlling-invariant-expression, associated with
MISRA-C:2004 rule 4.1 and MISRA-C:2012 rule 2.1, provides a partial
coverage for those rules without runtime error analysis.
▲ Likewise, the check uninitialized-variable-use (rule 9.1 of both
MISRA-C:2004 and MISRA-C:2012) checks for missing initializers
if the runtime error analysis is disabled.
▲ The following checks have been split in two
to gain a partial check that does not rely on the analysis:
error-information-unused error-information-unused
error-information-unused-computed
shift-width shift-width
shift-width-constant
essential-shift-width essential-shift-width
essential-shift-width-constant
parameter-match parameter-match
parameter-match-computed
boolean-invariant boolean-invariant
boolean-invariant-expression
controlling-invariant controlling-invariant
controlling-invariant-expression
MISRA-C:2004
------------
▲ Added support for rule 18.2.
▲ The following rule checks have been added to cover the aspect of
"implementational limits" (as defined in ISO/IEC 9899:1990 p2.2.4.1)
of rule 1.1:
△ max-arguments-macro
△ max-case-labels
△ max-condition-nesting
△ max-declarator-depth
△ max-declarator-nesting
△ max-enums
△ max-expression-nesting
△ max-externals
△ max-include-nesting
△ max-locals
△ max-logical-line-length
△ max-macros-defined
△ max-members
△ max-parameters
△ max-parameters-macro
△ max-statement-nesting
△ max-string-length
△ max-struct-nesting
△ parameters
▲ New checks for rule 15.0:
△ switch-skipped-code
warns about statements or declarations
preceding the first switch clause
△ switch-clause-empty-compound
warns about switch clauses consisting of only
an empty compound statement, e.g. default: {}
▲ Fixed checks for rule 8.4.
See the section on the C frontend for further details.
▲ The check function-return-type has been moved from rule 8.1 to rule 8.2.
▲ The checks for rule 8.1 now also warn about implicit
function declarations and function definitions without a preceding
declaration of that function.
▲ The check evaluation-order for rule 12.2
is now also performed in initializer expressions.
▲ The check for rule 11.3 has been improved
to also cover implicit conversions.
MISRA-C:2012
------------
▲ Amendment 1 is now supported, which adds new rules
and modifies rule 21.8. The new rules use the prefix M2012A1
followed by the MISRA rule number.
▲ Added support for rule 19.1.
▲ New checks for rule 16.1:
△ switch-skipped-code
warns about statements or declarations
preceding the first switch clause
△ switch-clause-empty-compound
warns about switch clauses consisting of only
an empty compound statement, e.g. default: {}
▲ Read accesses are now only treated as persistent side effects if they
are syntactically volatile. This affects rules 13.1, 13.2, 13.5, and 14.2.
▲ Fixed check for-loop-condition-sideeffect for the case when
the third expression of a for-loop is missing. This affects rule 14.2.
▲ Fixed check side-effect-in-initializer-list for initializer lists
with a single element. This affects rule 13.1.
▲ The check evaluation-order for rule 13.2
is now also performed in initializer expressions.
▲ The check function-return-type has been moved from rule 8.2 to rule 8.1.
▲ Fixed false alarm about violation of rule 6.2 when using the _Bool type.
▲ Fixed false alarms about violation of rule 13.3 when performing
the check unary-assign-detachment in combination with volatile variables.
▲ The checks for rules 11.1 and 11.4 have been improved
to also cover implicit conversions.
Both rule sets
--------------
The checks for the MISRA-C:2004 rules 11.4 and 11.5
and for the MISRA-C:2012 rules 11.3, 11.6, 11.7, and 11.8
have been extended to cover implicit conversions.
▲ Added the checks
△ pointer-qualifier-cast-implicit
△ inappropriate-pointer-cast-implicit
△ object-pointer-diff-cast-implicit
△ object-pointer-diff-cast-strict-implicit
▲ Split the check
cast-pointer-void-arithmetic cast-pointer-void-arithmetic
cast-pointer-void-arithmetic-implicit
▲ Added pointer-qualifier-cast-implicit to rule 1.1.
Customer-specific rules
-----------------------
▲ Fixed false alarm in rule X.A.4.8 for comment sequences of the form
/* comment1 *//* comment2
* comment2 continued */
▲ Corrected documentation of rule X.A.3.9.
▲ The rule X.A.4.3 can now be modified by a regular expression parameter.
Extensions of the DAX format
----------------------------
▲ New DAX version 1.3.
▲ External declarations are now specified in DAX rather than in an .edf file.
Here is an example that shows the new DAX tags:
<external-declarations>
<type>typeA</type>
<type>typeB</type>
<declaration>typeA f(int)</declaration>
<declaration>typeB g(typeA, int)</declaration>
</external-declarations>
▲ The DAX export from the GUI has been adapted accordingly.
Old DAX and .edf files can still be imported.
▲ The ABI settings have been extended for specifying pointers
of different size. Here is an example that shows all new DAX tags:
<abi>
<sizeof_attributed_pointer_1>2</sizeof_attributed_pointer_1>
<alignof_attributed_pointer_1>2</alignof_attributed_pointer_1>
<atomic_attributed_pointer_1>no</atomic_attributed_pointer_1>
<pointer_attributes_1>_near,_xnear</pointer_attributes_1>
</abi>
▲ The ABI settings have been extended to include information
about whether aligned accesses to the different basic data types are atomic:
ABI key DAX tag
atomic_bool <atomic_bool>yes|no</atomic_bool>
atomic_char <atomic_char>yes|no</atomic_char>
atomic_short <atomic_short>yes|no</atomic_short>
atomic_int <atomic_int>yes|no</atomic_int>
atomic_long <atomic_long>yes|no</atomic_long>
atomic_long_long <atomic_long_long>yes|no</atomic_long_long>
atomic_float <atomic_float>yes|no</atomic_float>
atomic_double <atomic_double>yes|no</atomic_double>
atomic_long_double <atomic_long_double>yes|no</atomic_long_double>
atomic_pointer <atomic_pointer>yes|no</atomic_pointer>
atomic_function_pointer
<atomic_function_pointer>yes|no</atomic_function_pointer>
Information about atomically accessible data types has been added
to the pre-defined ABIs where appropriate.
▲ For asynchronous execution models, the parameters attribute
of the <task> tag in the <wrapper> section has been replaced
by a new priority attribute:
<wrapper>
<task priority="50">Task0</task>
<task priority="100">Task1</task>
<execution-model>asynchronous</execution-model>
</wrapper>
▲ The DAX format has been extended by a <report-configuration> section
that allows the definition of customized reports. The extension is defined
in a separate XML schema that is included by the XML schema for DAX.
The schema can be found at
absint.com/dtd/astree-dax-report-configuration-16.10.xsd.
Updates to the TargetLink coupling
----------------------------------
▲ The TargetLink importer settings are now shared between all clients.
For analysis projects created with older versions of Astrée,
the settings are taken from the first user that opens the old project
and then saves it.
▲ "Import Result from XTC File" now puts the result into a new
AbsIntAnalysisResults element of the function instead of writing
to the function’s properties directly.
▲ Missing source files are no longer added to the analysis configuration.
Instead the toolbox prints a warning message.
▲ The Astrée Server Settings dialog now also lists Astrée
versions that were not installed in the default location.
▲ The Data Dictionary file in the TargetLink Data Dictionary Importer file
can now be specified using a relative path. Relative paths are extended
with the global base directory specified in the Preprocessor view.
Jenkins and Eclipse plugins
---------------------------
▲ Initial release of the Jenkins plugin for Astrée.
See absint.com/astree/jenkins.htm
▲ First public announcement of the Eclipse plugin for Astrée.
See absint.com/astree/kerci.htm
Batch mode
----------
▲ Progress information is now printed to stdout:
Progress: [13:45:13]: Processing DAX...
Progress: [13:45:13]: Importing...
[...]
Progress: [13:45:14]: Analyzing...
Progress: [13:45:30]: Analysis done...
▲ For any error that occurs during preprocessing, the text report file
now includes the preprocessor command line that caused it.
General configuration
---------------------
Modified the interpretation of preprocessing configurations
w.r.t. the use of relative paths as their base directory.
Such paths are now extended by prepending the base directories
of all parent configurations up to the global base directory.
This path extension terminates at the first base directory
that is specified as an absolute path. Example:
<base>C:/tmp/my_code/</base>
<config name="libs">
<base>lib</base>
<config name="extra files">
<base>extra</base>
<files>
<file>file.c</file>
</files>
</config>
</config>
This DAX configuration specifies the following file for preprocessing:
C:/tmp/my_code/lib/extra/file.c
The same path extension is also applied to include paths and is also
performed when configuring the preprocessor in the GUI.
Options
-------
▲ New options:
△ precise-priorities (default "no")
Only applies to analyses of concurrent software.
Activates a new domain for more precise handling of process priorities
including dynamic priorities (e.g. according to the Priority Ceiling
Protocol). Generally this leads to higher analysis times, but yields
significantly more precise results.
△ warn-on-deadlocks (default "no")
Activates detection of deadlocks in asynchronous software.
See the Results section of these release notes for further details.
△ warn-on-atomic-volatile-data-race (default "yes")
When this option is set to no, no data race will be reported for accesses
to memory through lvalues that are qualified as volatile and have a type
declared as atomic in the ABI specifications. This is particularly useful
for analyzing lock-free implementations of concurrent behavior.
△ at-location (enabled by default)
Controls whether Astrée supports @<address> declarations
(compiler extension) for data placement at an absolute location.
If enabled, the analyzer considers the following declaration
int i @0x1234;
to be equivalent to
int i;
__ASTREE_absolute_address((i, 0x1234));
That is, the declared variable is known to be allocated
to the given absolute address. The address can also be specified
as a constant expression.
▲ It is now possible to specify how bitfields should be treated
with respect to data races. By default, concurrent bitfield accesses
within the same byte are reported as data races. When using the new
option bitfield-data-race-enclosing-bytes-only=no, bitfield accesses
are considered to interact with all bitfields contained within
the boundaries of the type used in their definition.
▲ Removed options:
△ automatic-shared-variables
Shared variables are now always automatically detected.
△ constant-propagation
Constant propagation is now always used when evaluating constant
expressions. In addition, it is used for source code simplification
if the simplify option is enabled. That is, simplify=yes now behaves
like simplify=yes constant-propagation=yes in earlier releases.
▲ The option partition-pt1 now takes an integer value as argument
instead of the previous yes/no. The integer value specifies into how many
partitions the values of PT1 filters are divided by the analyzer.
The default value is 3, which was the value used with partition-pt1=yes
in earlier Astrée releases. Values less than 2 disable partitioning
of PT1 filters. Values greater than 3 increase precision up to a certain
limit. When converting old analysis projects or importing them via AAF
or DAX, the old value yes is automatically converted into 3, while no
is converted into 0.
▲ The default value of stop-parse-error-immediate has been changed to "no",
i.e. the option is now disabled by default.
▲ With the option stop-parse-error-immediate=no, parse errors no longer stop
the rule checking on preprocessed files completely. Instead it is performed
on all successfully parsed files.
Directives
----------
▲ The directives __ASTREE_asynchronous_loop and __ASTREE_shared_variable
are not supported anymore. Asynchronous tasks should be declared using
__astree_create_process and __astree_start_process.
▲ The directive __ASTREE_known_range again accepts parenthesized expressions:
__ASTREE_known_range(( (*p)[], [0;100] ));
This was temporarily unsupported in release 16.04.
▲ The directive __ASTREE_absolute_address now accepts not only constants
but also constant expressions as absolute addresses.
▲ When encountering an invalid __ASTREE_absolute_address directive,
the analyzer no longer stops. Instead it reports the error and carries on
with the analysis. The invalid directive is ignored.
▲ In release 16.04 the directive __ASTREE_absolute_address was unintentionally
accepted in function scope (and ignored for function local variables).
It is now strictly rejected in function scope and only allowed
at the global level as documented.
ABI
---
▲ The analyzer now supports pointers of different sizes which are provided
by many compilers for accessing objects placed in different memory regions.
A typical example are 'near' and 'far' pointers. To this end, the ABI
settings allow the configuration of up to three additional 'attributed'
pointer types. Each 'attributed' pointer has its own size, alignment,
and atomicity settings. An additional list of attributes specifies
the keywords that are used to declare a pointer of this kind. The given
size information is used by the analyzer to calculate the correct layout
of other types. The new ABI keys and DAX tags are:
△ sizeof_attributed_pointer_1
△ alignof_attributed_pointer_1
△ atomic_attributed_pointer_1
△ pointer_attributes_1
▲ Updated the ABI for c166 to respect the __near, __xnear, __far, __huge,
and __shuge attributes for pointers.
▲ Added ABI for IAR on RL78 with data model "Near".
▲ The ABI settings have been extended by information about whether
aligned accesses to the different basic data types are atomic.
The new ABI keys are constructed by adding the prefix atomic_
to a basic data type, e.g. atomic_bool, atomic_char, atomic_short.
Information about atomically accessible data types has been added
to the pre-defined ABIs where appropriate.
▲ Corrected the values for the long double type in the pre-defined
ppc32diab ABI.
Patch 1 (build 271444)
----------------------
Fixed the following known issues:
▲ When using the ABI option "rounding_mode=to_nearest", older builds
of the analyzer might stop in some contexts when evaluating
a guard expression that involves a binary operation on floats.
▲ When using the option "exclude-signed-in-unsigned-overflows"
("Do not raise overflow alarms on unsigned computations with signed values"),
older builds of the analyzer might crash in certain scenarios.
==============================================================================
Last updated on 24 November 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.10