All network connections between the ALM server and its clients are now TLS-encrypted, and the ALM web interface is now served via HTTPS in addition to HTTP.
Upgrading your client to this release requires upgrading your ALM as well. Old client versions will continue to work with the new ALM using the non-encrypted legacy protocol, unless you block the corresponding port in your firewall. The default port for the legacy protocol is 42424, while for the new TLS connection it’s 42426.
A new environment variable AI_LICENSE_TLS
is used to configure
the license, while old versions use AI_LICENSE
. This enables you
to set up old and new versions to run in parallel, for example:
AI_LICENSE = alm-server@42424 AI_LICENSE_TLS = alm-server@42426
The default port for the ALM web interface is 42425 for HTTP and 42427 for HTTPS.
--dir <path>
a3*
directories. This enables you to unpack the product ZIP files in a directory
and use the launcher of any of them to access all of them. For example, if you
have a directory with
a3_c_123
,
a3_c_456
, and
a3_ppc_789
,
you can now use the launcher in a3_c_456/bin
to access all three tools.<strip-path/>
and <replacements/>
.
They are no longer needed and can be removed from DAX files.use-relative-paths
.Analysis precision has been improved for:
(un)signed x
-bit integer
where x
is the number of bits used to represent the type.unroll-loops-in-functions
and separate-function
now match entire function signatures instead of a prefix of function signatures.__ASTREE_modify
, __ASTREE_volatile_input
,
__ASTREE_known_range
, __ASTREE_global_assert
).Introducing a new diff-based comment mechanism which, in case of code changes,
identifies commented code locations by comparing the currently analyzed code
with a reference from a previous analysis run. The new comment mechanism
is available in all analysis modes
(astree
, astree-cxx
, rulechecker
).
--convert-to-diff-comments
.--export-diff-comments <dax-file>
allows exporting diff-based comments into a DAX file.x + y
Astrée now also shows
a tooltip for the +
operator, reporting the result of the addition.x = in >> 15; out = (in << 1) - (x << 16); // 'out' is now known to be positive for positive 'in'
((a - b - c) / d) < 8;
unaligned_dereference
by two new
Astrée semantics options:
warn-on-misaligned-dereference
(default: yes
)
warns about misaligned dereferencescut-misaligned-dereference
(default: yes
)
cuts traces with misaligned dereferences from the analysisunaligned_dereference=error
.__ASTREE_global_assert
can now express
that a pointer may only point to certain offsets in a variable.
For example, if the pointer p
may point to the fields
a
or b
of variable v
,
that can be expressed as
__ASTREE_global_assert((p; {&v.a, &v.b}));
__ASTREE_check_separate_targets
for the case that more than two arguments are given.__ASTREE_octagon_pack
with variables of pointer type
and the Boolean domain enabled.generate-undeclared-absolute-addresses
was enabled.combine="merge"
attribute.
This allows specifying additional includes and defines for the generated
preprocessor configuration via an additional DAX file, as configured
in the toolbox preferences.coverage_ignore
attributes.invalid_directive
now also warns about
__ASTREE_partition_calls
directives that have no function call
in scope.endasm
instead of end_asm
.pragma-usage
(A.5.2,
AUTOSAR.16.0.1A, AUTOSAR.16.7.1A,
M.3.4, M2008.16.6.1,
M202x-DRAFT.000213) by restricting it
to code sections included by the preprocessor.#include
.max-number-of-recursive-paths
.
It now reports which functions are involved in the recursion.unary-assign-separation
(AUTOSAR.5.2.10M,
M.12.13, M2008.5.2.10)
no longer warns about subscript operator uses in operands of increment/decrement
operations. For C++, the check treats overloaded operator calls like
built-in operators, in accordance with the latest interpretation of the
associated rules, to remove undesired alarms.unused-suppress-directive
now additionally reports the end location of the affected code area.unused-suppressed-directive
(B.1.2)
can now be configured to exclude source directives that are never reached by the preprocessor.clangstaticanalyzer
.
This removes irrelevant alarms for all checks that run in that phase.non-standard-escape-sequence-pp
into the check non-standard-escape-sequence
(A.2.11, M.1.1,
M2012.1.2, X.E.5.2.5.5).cast-integer-implicit
(M.10.1)
and cast-float-implicit
(M.10.2, X.F.27)
with initializers for bit-fields and at function returnstatic-object-zero-initialization
(AUTOSAR.3.3.2A).
It no longer warns about out-of-class definitions of static data
members without initializer if their in-class declaration features
an initializer.global-object-scope
(CERT.DCL.15, CERT.DCL.19,
M.8.10, M2012.8.7,
X.B.5.5, X.F.31).
Tentative definitions (without initializer) are now considered a use of the variable as well.implicit-designation
(M2012.9.2).
In addition to the excluded values {0}
and {0U}
,
arbitrary integer constants of zero value are now excluded as well
({0UL}
, {0x0}
, etc.).global-object-scope
(CERT.DCL.15, CERT.DCL.19,
M.8.10, M2012.8.7,
X.B.5.5, X.F.31),
which did not report tentative definitions (without initializer) without further use.min-comment-density-his
).
sline-comment
(M2012.3.1, M2023-C.3.1, CERT.MSC.4)
is no longer reported in code that is excluded by the preprocessor.
object-pointer-diff-cast
and object-pointer-diff-cast-implicit
(M2023-C.11.3, M2012.11.3, M.11.4)
now report when a pointer to an atomic qualified object type
is converted to a pointer of type char, signed char or unsigned char.pointer-qualifier-cast-atomic
and pointer-qualifier-cast-atomic-implicit
(M2023-C.11.8).sline-comment
by providing
a regular expression option to its associated rules
(CERT.MSC.4, M2012.3.1, M2023-C.3.1).bad-function
no longer fails on the use of non-function declarations.
This removes false positives for AUTOSAR.15.5.2A,
AUTOSAR.18.9.1A, AUTOSAR.26.5.1A,
M202x-DRAFT.000202, M202x-DRAFT.000355,
M202x-DRAFT.000226, M202x-DRAFT.000223,
M202x-DRAFT.000329, CERT-CPP.CON.37C,
CERT-CPP.MSC.30C, and CERT-CPP.MSC.50.assignment-operator-return-type
(AUTOSAR.13.2.1A) has been split into the checks
assignment-operator-return-type
(which allows void as return type) and
assignment-operator-return-type-void
.mmline-comment
(AUTOSAR.2.7.1M, M2008.2.7.1, M202x-DRAFT.000025).pragma-usage
(A.5.2, AUTOSAR.16.0.1A, AUTOSAR.16.7.1A,
M202x-DRAFT.000213, M2008.16.6.1)
which did not report the use of _Pragma("...")
.clean-global-namespace
(M2008.7.3.1, AUTOSAR.7.3.1M)
regarding template parametersoriginal-source-annotation-insertion-failed
(A.CPP.5.1) when the annotation insertion targets a location that might be
excluded by the preprocessor in only some translation units,
e.g. due to an include guardmixed-virtual-base
(AUTOSAR.10.1.3M, M2008.10.1.3,
M202x-DRAFT.000165),
which sometimes failed to consider all inheritance edgespotentially-throwing-static-initialization
(AUTOSAR.15.2.1A, CERT-CPP.ERR.58).
It now also reports violations within variable template (partial) specializations.bitop-type
(M2008.5.0.21, AUTOSAR.5.0.21M)
regarding the left-hand side of bitwise shift assignment operators <<=
or >>=
shift-width-constant
(M2008.5.8.1, AUTOSAR.5.8.1M)
regarding the right-hand side of bitwise shift assignment operators <<=
or >>=
underlying-cvalue-conversion
(AUTOSAR.5.0.3M, M2008.5.0.3)
with respect to reference types and elaborated typesunderlying-narrowing-conversion
(AUTOSAR.5.0.6M, M2008.5.0.6)
with respect to elaborated typesunderlying-signedness-conversion
(AUTOSAR.5.0.4M, M2008.5.0.4)
with respect to elaborated typesnon-diamond-virtual-base
(AUTOSAR.10.1.2M, M2008.10.1.2),
which sometimes failed to consider all inheritance edgesusing-directive-header
(AUTOSAR.7.3.4M, AUTOSAR.7.3.6M,
M2008.7.3.4, M2008.7.3.6)using-directive-non-header
(AUTOSAR.7.3.4M, M2008.7.3.4)using-declaration-header
(AUTOSAR.7.3.6M, M2008.7.3.6)inaccessible-external-function
(AUTOSAR.3.3.1A, M2008.3.3.1)inaccessible-external-object
(AUTOSAR.3.3.1A, M2008.3.3.1)unused-internal-function
(AUTOSAR.0.1.10M, AUTOSAR.0.1.3A,
M2008.0.1.10)unused-internal-variable
(AUTOSAR.0.1.3M, M2008.0.1.3)unnamed-namespace-header
(AUTOSAR.7.3.3M, CERT-CPP.DCL.59,
M2008.7.3.3)allow-signed-constant-with-unsigned
now only affects non-negative signed constants. This removes
false negatives of the checks underlying-signedness-conversion
(M2008.5.0.4, AUTOSAR.5.0.4M) and
bitop-type
(M2008.5.0.21, AUTOSAR.5.0.21M)
when the option is enabled.potentially-throwing-static-initialization
(AUTOSAR.15.2.1A, CERT-CPP.ERR.58).
In addition to checking for the existence of a noexcept
exception specification,
it now also checks the condition and thus also catches noexcept(false)
.parameter-name-match
(M2008.8.4.2, AUTOSAR.8.4.2M)
no longer warns about mismatched parameter names between an explicit
function template specialization declaration and the template declaration
that is specialized.function-return-unused
(M2008.0.1.7, AUTOSAR.0.1.2A)
now also warns when the overloaded call operator()
is used with function call syntax, i.e. with ()
.cast-integer-to-pointer
(M2008.5.2.8, AUTOSAR.5.2.8M)
no longer warns about conversion from integer type to function pointer.
This aspect of the associated rules is now covered by the new check
cast-integer-to-function-pointer
.inconsistent-default-argument
(M2008.8.3.1, AUTOSAR.8.3.1M)
now treats non-constant expression as having different values.
The associated rules are thereby decidable and now fully covered.ambiguous-identifiers
(AUTOSAR.2.10.1M, M2008.2.10.1)
for identifiers introduced by friend declarations.--concurrent-analyses-limit <int>
--set-concurrent-analyses-limit <int>
--report-only
can now also be used
for generating reports from AAF files./* Semantic hypotheses */
and /* Further directives */
sections of the output view and text report.__ASTREE_attributes(())
can now also be used
in files that do not require preprocessing, such as the 'Wrapper and Stubs File'.annotation-insertion-failed
).var@fun@"file.c"
) is no longer restricted
to Astrée directives only. The syntax can now be used
everywhere in that file.std::vector
and std::string
to the C++ STL stubs for Astrée.
The abstract version of std::vector
does not allow the use of low-level pointer arithmetic on the underlying representation,
e.g. using the pointer returned by data()
.
The abstract version of std::string
supports efficient analysis
of strings up to a total capacity of 100 bytes. API calls
that exceed this limit raise an alarm and their effects are ignored.enum_preferred_sign
from signed to unsigned. This change also corrects the following target ABIs
with respect to the preferred sign for enums:
enum_preferred_size=best
to match the actual platform behavior.The test case qk_abi_unaligned_derefence
has been removed
from the Astrée QSK.
The test case qk_abi_unaligned_derefence
has been removed
from the RuleChecker QSK.