break
or return
statements__ASTREE_modify((*ptr; full_range))
when
ptr
is of type float*
and might point
to several different memory locations. The directive then no longer
adds ±Inf/NaN to *ptr
.global-iteration-limit
allows bounding the number of global
iterations of the analyzer. The option is off by default.global-iteration-limit-per-phase
allows bounding the number
of global iterations for each asynchronous phase of the analysis. The option is off by default.warn-on-memory-leaks
raises alarms when
NULL
.ais-export-source-location
switches
the export of AIS annotations for AbsInt's WCET and stack analysis tools
from the default "routine calls" annotations to more precise
source-code relative annotations.separate-function
now accepts new parameters
for fine-tuning separate functions for different analysis phases and processes.text-report-tables
to empty now removes all tables
from the text report instead of printing the default tables.separate-function
for context-insensitive analysis, the analyzer now covers separate contexts
with possibly recursive functions up to true recursions. The alarm message
ALARM (A) stopped separate context: context may be recursivethat warned about not fully covered separate contexts has been removed.
dev-geo=yes
) now stops if
the dependency graph grows very large.var@function
,
to help distinguish multiple occurrences of the same variable name.__ASTREE_global_assert
directive so that
it is now possible to assert the variables and functions a pointer may point to.
The associated syntax is described in the documentation.__ASTREE_global_assert
violation
on a smashed variable of union type, Astrée now computes more precisely
in which cases the violation cannot occur and continues the analysis with these cases.insert comment
to permit insertion of ASTREE_comment
and ASTREE_suppress
directives in comment blocks within original source files. For example:
__ASTREE_annotation(( "main.c" insert comment: ASTREE_comment(...) "main.c" insert comment: ASTREE_suppress(...)Ii ));
list-not-reached
and gray markings
in the GUI) has been improved for C++, in particular in the presence of templates.
A statement is completely grayed out in the code view only if it cannot be reached at all.
If parts of a statement are unreachable, e.g. the increment in a for-loop or the operands
of lazily evaluated operators (||
, &&
), only these parts are grayed out.cxx_invalid_this_pointer: this pointer may be null or invalidis raised when calling a member function with an object pointer that may be null or dangling.
__ASTREE_partition_control if (cond) ...
and __ASTREE_partition_expr((cond));
when cond
is an expression that uses the lazily evaluated logical operators
||
or &&
.state-machine
and by the directives __ASTREE_states_track
and __ASTREE_states_merge
.<abstract-cxx-stl-stubs>yes</abstract-cxx-stl-stubs>
to the <preprocess/>
section of DAX files.cxx_invalid_usage_of_iterator
. The alarm is reported
in the following situations:
cycl-simplify-switch
causes
the switch statement to be counted as a single decision when computing
the CYCL metric. The new option is disabled by default.unused-macro
.
It now also reports macros that are defined using the following scheme:
#ifndef M // this check is no longer considered a use of M #define M #endif
builtin-constant-p
and builtin-sel
in favor of the new check builtin-function
(rule A.2.20)
that warns about the use of all supported compiler builtin functions.Added support for the following MISRA rules:
compound-alignment
(X.B.6.2, X.D.7.6.d) now handles
if ... else if ...
constructs as one entity. This means that each
nested block in such an if else
cascade is checked for being aligned
with the first if
instead of the closest preceding if
.compound-alignment
(X.B.6.2, X.D.7.6.d) is now performed
on original source code to avoid the impact of the preprocessor on indentation.Added support for rule M2008.7.4.1.
Added support for the following AUTOSAR rules:
parameter-missing-const
(CERT.DCL.0, CERT.DCL.13,
M.16.7, M2012.8.13),
which warned about non-const pointer parameters even when passed to
a function pointer call and the callee required them to be non-const.assignment-to-non-modifiable-lvalue
(A.1.7, CERT.EXP.40,
CERT.MSC.40, M.1.1,
M2012.1.1, X.E.5.2.2.1),
which warned about assignments to struct types with flexible array members,
which does not constitute a constraint violation.uninitialized-local-read
(CERT.EXP.33, CWE.456,
CWE.457, CWE.665,
CWE.824, CWE.908,
ISO17961.uninitref, M.9.1,
M2012.9.1).__ASTREE_assert
, __ASTREE_known_fact
,
and __ASTREE_known_range
are now considered to be written by the directive statement.side-effect-in-logical-exp
(M2012.13.5),side-effect-in-initializer-list
(M2012.13.1),evaluation-order
(A.4.1,
CERT.EXP.10, CERT.EXP.30,
M.12.2, M2012.1.3,
M2012.13.2, X.A.5.34),evaluation-order-initializer
(A.4.2,
M2012.1.3, X.A.5.34),multiple-volatile-accesses
(CERT.EXP.10,
CERT.EXP.30, M.12.2,
M2012.1.3, M2012.13.2),side-effect-in-conditional
(X.E.5.2.1.2),logop-side-effect
(CERT.EXP.2,
M12.4), andfor-loop-condition-sideeffect
(M2012.14.2).
statement-sideeffect
(M.14.2, CERT.MSC.12),expression-statement-pure
(M2012.2.2, CWE.561), andexpression-statement-dead
(M2012.2.2, CWE.561).__ASTREE_volatile_input
directives as volatile, introduced in the last intermediate release 20.10i b8841650.essential-type-assign
(M2012.10.3)
which did use the wrong type for bit-fields of essentially Boolean type.__has_include_next
and #include_next
for uncommon mixtures of relative and absolute paths
in the preprocessor configuration that previously lead to spurious parse errors.cast-implicit
(X.A.5.44)
which did not report integer conversion at switch conditions nor implicit
conversions at case
statements.unsigned-bitfield-promotion
(X.E.5.2.1.1)
which did not report integer promotion for the switch condition expression.#include
directives using backslash as path separator.undefined-extern
on C++ (AUTOSAR.3.2.2M, AUTOSAR.3.2.4M,
CERT-CPP.DCL.60, M2008.3.2.2,
M2008.3.2.4)
which did not warn about undefined variables introduced by explicit
template instantiation, such as in
/* template even providing a function body */ template<class T> void f(T) {} /* explicit instantiation which does not create a definition */ extern template void f<>(int);
implicitly-virtual-method
(M2008.10.3.2), which did warn about out-of-line definitions of virtual methods.implicit-virtual
(AUTOSAR.10.3.1A),
which did warn about out-of-line definitions of virtual methods.scattered-data-member-initialization
(AUTOSAR.12.1.3A) that warned about constructor member initialization with non-constant
constructor call as being constant.scattered-data-member-initialization
(AUTOSAR.12.1.3A) that did not warn about constant non-numeric member initialization
in constructor, e.g. pointer initialization with nullptr.non-pod-struct
(AUTOSAR.11.0.1A) in templates.non-pod-struct
(AUTOSAR.11.0.1A).non-private-non-pod-field
(AUTOSAR.11.0.1M, M2008.11.0.1) in templates.underlying-bitop-width
(M2008.5.0.20, AUTOSAR.5.0.20M)bitfield-signed-size
(M2008.9.6.4, AUTOSAR.9.6.4M)underlying-cvalue-conversion
(M2008.5.0.3, AUTOSAR.5.0.3M)underlying-signedness-cast
(M2008.5.0.9, AUTOSAR.5.0.9M)cvalue-float-int-cast
(M2008.5.0.7, AUTOSAR.5.0.7M)cvalue-int-float-cast
(M2008.5.0.7, AUTOSAR.5.0.7M)underlying-widening-cast-float
(M2008.5.0.8, AUTOSAR.5.0.8M)underlying-widening-cast-int
(M2008.5.0.8, AUTOSAR.5.0.8M)digraph-token
(AUTOSAR.2.5.2A, M2008.2.5.1) for template parameters starting
with ::
(resulting in the character sequence <::
).definition-duplicate
(AUTOSAR.3.2.2M, AUTOSAR.3.2.4M,
M2008.3.2.2, M2008.3.2.4)
which warned about inline variables of external linkage.scattered-data-member-initialization
(rule AUTOSAR.12.1.3A).
The check did not warn when fields were initialized
to the same effective value using different initialization, e.g.
for bool field;
it did not report: field() // initialized with false
: field(false) // initialized with false
.<arxml-file>
has been replaced
by a <files/>
list to enable specification of multiple
ARXML files for AUTOSAR. For example:
<autosar> <files> <file>f1.arxml</file> <file>f2.arxml</file> </files> </autosar>
<separate-function/>
tag to enable expressing
separate functions for different analysis phases and processes.<dax><base>PATH</base></dax>
tag
to configure the project base directory.A3_PROJECT_BASE_DIR
,
A3_PREPROCESS_BASE_DIR
, and A3_CONFIG_BASE_DIR
for use in DAX files.A3_PREPROCESS_BASE_DIR
corresponds to the former
A3_GLOBAL_BASE_DIR
variable, which is considered deprecated
and will be removed in a future release.A3_CONFIG_BASE_DIR
corresponds to the former
A3_BASE_DIR
variable, which is considered deprecated
and will be removed in a future release.This is the last release to officially support Windows 7. Future releases will require at least Windows 10.
The new Compilation Database Importer tool allows to automatically
extract a preprocessor configuration from a compile_commands.json
file
as generated by modern build systems like e.g. cmake
. It is available
via the Tools menu and via a new batch mode option. The extracted configuration
can be exported into a .dax
file or imported directly
into the current analysis project.
Fixed a syntax error in the generated directive for multidimensional output variables.
--symbols %Y
to make the compiler symbols available in RuleChecker projects.arm_compat.h
header file is included automatically
if ARMCLANG is used. This can be disabled using the command-line option
--no-compat
.config-file
to the analysis project.astree-cxx
for C++ projects,
astree
for C projects).space-overhead=n
allows to configure
the space overhead of the garbage collection during analysis runs.<messages/>
, <alarm_types/>
,
<alarm_categories/>
, and their children.
The following (simplified) example illustrates the changes.
Here is the structure of these XML tags from previous releases:
<messages> <alarm_message type="a21581" key="array_out_of_bounds" /> <error_message type="a21541" key="error_analysis_stopped"/> </messages> <alarm_types> <alarm_type id="a21581" category_id="c2" class="A" key="array_out_of_bounds"/> <alarm_type id="a21541" category_id="c11" class="E" key="error_analysis_stopped"/> </alarm_types> <alarm_categories> <alarm_category id="c2">Invalid usage of pointers and arrays</alarm_category> <alarm_category id="c11">Errors</alarm_category> </alarm_categories>Here is the same example using the new structure:
<findings> <finding kind="alarm" class="A" key="array_out_of_bounds"/> <finding kind="error" key="analysis_stopped"/> </findings> <finding_categories> <finding_category category_group_id="c2" finding_key="array_out_of_bounds" finding_kind="alarm" class="A"/> <finding_category category_group_id="c11" finding_key="analysis_stopped" finding_kind="error"/> </finding_categories> <category_groups> <category_group id="c2">Invalid usage of pointers and arrays</category_group> <category_group id="c11">Errors</category_group> </category_groups>
<base>
DAX tag in global scope (see also the release notes about DAX changes).
--block-remote-connections
when starting the server,
or by setting "Block connections from remote hosts" in the server controller.--password-constraints
.__ASTREE_volatile_input
directives that refer to (parts of) variables that are already affected by a preceding
__ASTREE_volatile_input
directive.__astree_va_start
.__builtin_huge_val
__builtin_huge_valf
__builtin_huge_vall
__builtin_inf
__builtin_inff
__builtin_infl
__builtin_isfinite
__builtin_isinf
__builtin_isnan
__builtin_nan
__builtin_nanf
__builtin_nanl
__builtin_nans
__builtin_nansf
__builtin_nansl
__builtin_expect
typedef union { unsigned _v; struct { unsigned v1:1; }; } ut; unsigned u = ((ut){.v1 = 1}._v);
enum_preferred_size
has been extended to accept
a new value best
corresponding to the Diab compiler's
-Xenum-is-best
option. The effect of the value smallest
has been modified to correspond to the Diab compiler's -Xenum-is-small
and the GCC compiler's -fshort-enums
options. This modification may lead
to differently sized enums for analyses configured to enum_preferred_size=smallest
and enum_preferred_sign=unsigned
. The new choices are more compatible
with the majority of compilers. Users of the Diab compiler that use the -Xenum-is-best
option should switch to enum_preferred_size=best
.NDEBUG
is no longer implicitly defined.offsetof
(mapping it to the analyzer built-in offsetof
).__builtin_copysignf
built-in function of the CompCert compiler.pow
and powf
.tanh
, tanhf
,
imaxabs
, and llabs
to the C stub library.TRUSTED_FUNCTION_NAME
DEFINE_TRUSTED_FUNCTION
DEFINE_TRUSTED_FUNCTION_WRAPPER
The test case qk_option_stopped_separate_context
has been removed from the Astrée QSK.
The test cases qk_check_builtin_sel
and
qk_check_builtin_constant_p
have been removed
from the RuleChecker QSK.
qk_check_loose_asm