% used in conditionsoffsetof for the code pattern
&((S*) NULL)->field
NaN,
∞, or −∞.__ASTREE_global_assert
now retain their globally asserted bounds, even when affected by data races.cut-write-to-const is enabled, then
write_to_constant_memory alarms are used to sharpen the analysis information
such that affected pointers cannot point to definitely const memory afterwards.[0,16] U {255}
can be represented precisely in many cases.__ASTREE_absolute_address directives.To grade alarms according to their significance, findings are now extended by a new attribute “weight”.
The weight can be displayed in an extra column in the Findings view. It is hidden by default and can be enabled from the context menu by right-clicking on the table header.
The findings can also be filtered according to their weight from Overview → Filter.
The corresponding DAX tag is <threshold kind="weight">.
The weight can be exported to the XML report and custom report files
using the DAX element <include-weight threshold="value">.
__ASTREE_partition_calls(())
that partitions function calls in any declaration or the statement
that directly follows it. For if, switch,
for, while, and do-while statements,
it only partitions function calls in the condition expression.__ASTREE_partition_control
now also works when placed in front of a switch statement
whose body starts with declarations.__ASTREE_modify((x; full_range)) no longer stops
the analysis of the current context if x is const.__ASTREE_attributes now accepts
a new attribute hide_directives which omits Astrée
directives in scope from the lists of semantic hypotheses
and further directives. The new attribute is intended for
use in stub libraries.__ASTREE_alarm and __ASTREE_print
now support printing of pointers and strings. For example, the code
const char* mystr = "hello";
const char* myptr = mystr + 3;
__ASTREE_print(("%s0, %1", mystr, myptr));
results in the following output in both the analyzer log
and the text report file:
{hello}, {__ASTREEstring.hello.0} + {3} at <program-location>__ASTREE_partition_ranges
now accepts a slice of integer values:
__ASTREE_partition_ranges((var; {0 : 5}));
which is equivalent to:
__ASTREE_partition_ranges((var; 0, 1, 2, 3, 4, 5));
__ASTREE_boolean_pack
can now be used with bit-fields. For example:
struct T {int a; unsigned b:1;} v;
__ASTREE_boolean_pack((v.a; v.b));__ASTREE_attribute now accepts the new argument
forbid_separate that prevents affected functions from being
analyzed separately. It has the same effect as listing them
as forbid=<function> in the separate-function option.
The separate-function option takes precedence over
forbid_separate attributes.__ASTREE_modify
if the first argument is a large unsmashed array.main.__astree_memcpy().Definite Alarm (A) Group 1 ... ALARM (A) invalid_pointer_dereference:...
Definite Alarm (A) Group 1 ... ALARM (A) overflow_upon_dereference:...
separate-with-caller-stack-pointers has been removed.
The analyzer now behaves as if the option was enabled.__ASTREE_global_assert and
__ASTREE_volatile_input
when applied to large arrays.__astree_stop_process(process_id),
Astrée now emits an alarm message and ignores the intrinsic.generate-absolute-addresses.
It now generates distinct directives for separate contiguous
memory blocks up to a size limit. The new heuristic reduces
the impact of the generated directives on the performance
of the analysis.Dynamic folding no longer folds parts of variables with different value ranges.
Note that the directive
__ASTREE_global_assert modifies the range of a variable.
In other words, if a[i] is affected by an __ASTREE_global_assert,
but a[j] is not, then a is no longer dynamically folded.
warn-on-float-to-unsigned-conversion-trap
enables alarms on conversions from float to unsigned integer,
if values are in the interval (-1, 0). The option is disabled
by default. If enabled, the new alarm float_to_unsigned_conversion_trap
warns about such conversions that may trigger trap events
on some architectures.var@"file.c"),
as long as a preceding __ASTREE_import(()); directive is present.__ASTREE_import(()); directive is present. The syntax
var@fun addresses a variable named var in a function named fun.
The new syntax can also be combined with the syntax for
addressing static functions, as in var@fun@"file".exclude-signed-in-unsigned-overflows=yes
and symb=yes.boolean-domain was activated
in combination with exclude-signed-in-unsigned-overflows
caused the analysis to stop for a given context
with an “ERROR analysis_stopped_unexpectedly”.config-function-unknown (rule A.5.4)
warns about function names that are used in the Astrée option
separate-function but do not name a function in the analyzed code.autosar-inclusion-order)
warns about illegal header inclusion order in Astrée analysis projects
that use Astrée’s AUTOSAR OS stubs. It warns about #include
directives that attempt to include the real Os.h or osek.h
header files before the corresponding header file stubs for Astrée.constant-out-of-range
(rule M2012.1.1, M.1.1)
warns about constants that do not fit into the range of their type.The new checks are associated with rule M2012.1.3 and M.1.2, and correspond to the following Astrée alarms:
This new analysis phase runs checks provided by the Clang Static Analyzer.
It is deactivated by default and can be enabled by setting the new option
skip-clang-static-analyzer-phase to no.
The following new checks are available:
These new checks are associated with the following rules for C++:
Added support for the following AUTOSAR rules:
Added support for the following SEI CERT C++ rules:
Added a new C++-specific category of diagnostics rules (A.CPP), available for both RuleChecker and Astrée.
Improved reported source location for rule violations that refer to implicit conversions applied to the right-hand side of assignments or to the expression of a return statement.
unused-suppress-directive,
which no longer reports comment/suppress directives that apply to a violation
of check unused-suppress-directive.allow-signed-constant-with-unsigned=yes.
The fix affects rules based on MISRA’s essential type system
in case that the option is set. The option is disabled by default.bits_per_byte to 16.stdlib-limits without Astrée analysis
now covers the long double variants of mathematical functions.
This affects rule M2012.D.4.11,
M.20.3, and CERT.FLP.32.__ASTREE_import directives.
Erroneous uses are reported as violations of diagnostic rule
A.5.1 instead of causing fatal tool errors or crashes.max-language-scope (T.13.1).extern-object-declaration
(rule M2012.8.4) which failed to report
tentative definitions that are not followed by another definition. Example:
// ... no declaration of x int x; // tentative definition of x -> non-compliant, now reported // ... no definition of x
field-overflow-upon-dereference,
float-division-by-zero,
incompatible-argument-type,
int-division-by-zero,
int-modulo-by-zero,
null-dereferencing,
overflow-upon-dereference,
pointer-comparison,
pointer-subtraction,
read-data-race,
uninitialized-variable-use,
write-data-race,
write-to-constant-memory.undefined-extern. Array declarators
are no longer part of the reported source extent.unused-tag and identifier-unique-tag,
which in rare cases misclassified the use of a struct tag as a definitionbitfield-typing, which in release 21.04i (build 9394592 and 9410978)
reported bitfields using a typedef of explicitly signed short, long, and long longexternal-file-spreading
(M.8.8, M2012.8.5)
when operating on case-insensitive file systems in analysis projects
that use files with names that only differ in capitalization.type-compatibility-link
(A.1.1, CERT.DCL.40,
CERT.MSC.40, ISO17961.funcdecl,
M.1.1, M.8.4,
M2012.1.1, M2012.D.2.1),
which did not warn about tentative definitions of objects
without preceding declaration in the same translation unitcontrolling-invariant
at the first operand of ? :include_position
(M2008.16.0.1,
AUTOSAR.16.0.1M)
has been split into two checks to allow for a more fine-grained configuration:
include_position_language_linkage
warns about #include directives preceded by language linkage specifications (i.e. extern "C").
include_position
no longer warns about #include directives preceded by language linkage specifications
main-function-catch-all
(AUTOSAR.15.3.3A,
CERT-CPP.ERR.51,
M2008.15.3.2,
M2008.15.5.3),
which warned about non-defining declarations of the main function.
underlying-cvalue-conversion
(AUTOSAR.5.0.3M,
M2008.5.0.3) warning about compliant pointer arithmetic in C++.
external-file-spreading
(AUTOSAR.3.2.3M,
CERT-CPP.DCL.60,
M2008.3.2.3)
when operating on case-insensitive file systems in analysis projects
that use files with names that only differ in capitalization.output-parameter and multiple_output_values
(AUTOSAR.8.4.8A,
AUTOSAR.8.4.4A).
Parameters of lvalue-reference or pointer type
are only considered output parameters if they are
modified but never read in the function body.
Rule AUTOSAR.8.4.8A
and AUTOSAR.8.4.4A
are classified as partially checked.definition-duplicate for user-defined new and delete operators.
They replace the default definitions from the standard library without conflict.file” attribute in the tags <options>
and <abi> is no longer supported.<item/> list syntax is now mandatory.
For example, the old specification
<substitute-functions>aa=bb,cc=dd</substitute-functions>must now be written as:
<substitute-functions> <item key="aa">bb</item> <item key="cc">dd</item> </substitute-functions>
<item/> list syntax,
the tags for rules now use "enabled" attributes to express
(de-)activation of rules. For example, the old specification
<RULENAME value="AA, BB">yes</RULENAME>must now be written as:
<RULENAME enabled="yes">
<value>
<item>AA</item>
<item>BB</item>
</value>
</RULENAME>enabled”. For example, the old specification
<CHECKNAME>yes</CHECKNAME>must now be written as
<CHECKNAME enabled="yes"/>
<result-filter/> allows
the automatic configuration of the "Overview → Filter"
settings of the client. The filter settings are stored
persistently with the analysis project.__ASTREE_comment,
__RULECHECKER_comment,
__ASTREE_suppress,
__RULECHECKER_suppress,
as well as their source-directive counterparts
ASTREE_comment,
RULECHECKER_comment,
ASTREE_suppress,
RULECHECKER_suppress
now support a set of finding keys instead of only a single finding key.
Here is an example of the old syntax using a single finding key:
__ASTREE_suppress(1, 1, check_assignment);And here is an example of the new syntax using a set of finding keys:
__ASTREE_suppress(1, 1, {check_assignment, check_bitfield});ASTREE_comment and ASTREE_suppress).
The previous implementation inadvertently matched multiple files
if they shared the same suffix (e.g. file.cpp
also matched other_file.cpp) causing an error.__ASTREE_import.From this release on, Astrée and RuleChecker require at least Windows 10.
__ASTREE_wrapper_call directives are no longer generated by the TargetLink integration.Removed erroneous quotation marks in defines passed to the preprocessor configuration.
astree.cfg)
can now be opened in an editor via the context menu.int arr[0] = {23};
the initializer is ignored, as it violates the diagnostics A.1.2 and A.1.8.__ASTREE_global_assert.#pragma directives containing type specifiers.#pragma directives containing invalid tokens.__ASTREE_octagon_pack and
__ASTREE_boolean_pack.0x1.00000000000008p0,
which lies exactly between the two double numbers 0x1.FFFFFFFFFFFFFp0
and 0x2.p0.__ASTREE_global_assert,
to assert the variables and functions that a pointer may point to.The source directive /* ASTREE_comment */
now also accepts keys of alarm category groups, such as
rules_category.
Schedule()
in the OSEK stub library shipped with Astrée.
It now determines the ID of the process in which
it is invoked instead of always assuming an invalid ID.bits_of_byte=16 and bits_of_char=16.tmpnam and snprintf
in the C stub library.nested-isrs=yes|no
<priorities> <priority isr="fun_name" value="1001"/> </priorities>
<declaration-mode/>.The test cases
qk_directive_comment_source_external,
qk_filter_pragma_asm,
and
qk_option_separate_with_caller_stack_pointers
have been removed from the Astrée QSK.
The test case
qk_directive_comment_source_external
has been removed from the RuleChecker QSK.
