Astrée and RuleChecker Release 22.10

Backwards compatibility
Analysis results created with earlier releases cannot be displayed. 
When opening analyses from previous versions on the server or when 
importing them from AAF files, the results are discarded.
Note that configuration data is preserved, so that analyses can be 
repeated with the new version. To preserve old analysis results, 
export analysis projects to AAF before upgrading the server 
and use the previous version for reviewing the results.

Source-component tracking
Introducing new features for specifying source components 
and tracking interactions between them:

* Source components can be marked using the directive ASTREE_attributes 
  with the new attribute component("X"), where "X" is the component's name. 
  These attributes can also be set via the new "Edit attributes..." action 
  in the context menu of the original source files list.
* Component information is then displayed in the data-flow view, 
  the control-flow view, and in the corresponding sections of report files.
* The new option component-pairs-under-observation allows highlighting 
  the interactions between two components in the data-flow and control-flow views 
  and reports.
* The new option taint-components enables activation of taint semantics 
  to expose component dependencies.

Improved and extended octagon domain
* The octagon relational domain is now available for analyses of C++ 
  and mixed C/C++ code. This includes all options related to octagons 
  and octagon packing (octagon, automatic-octagon-packing, interproc-oct-packs, 
  max-oct-pack-size, fields-in-octagon-packs, octagon-epsilon, print-packs), 
  as well as the directive __ASTREE_octagon_pack.
* The octagon packing heuristics newly introduced with release 22.04 
  have been updated to improve precision on Boolean operations 
  and to treat *&var as var.
* It is now possible to refer to function parameters in __ASTREE_octagon_pack 
  directives, using the extended identifier syntax param_name@fun_name.
* The option fields-in-octagon-packs is now enabled by default.
* Fixed an issue that could cause the analysis to abort with exception 
  when the octagon domain was enabled.

New annotation mechanism for C++ analyses
* In Astrée's C++ mode, the context menu of the original-source editor view 
  now allows inserting annotations (Astrée directives or code snippets) 
  into arbitrary program locations before starting the analyzer. 
  In contrast to AAL annotations, such program locations are identified by 
  code patterns rather than control-flow based descriptions.
* The new view "Original Source Annotations" shows original source code 
  annotations and allows editing them.
* The DAX syntax has been extended to express the new annotations.

Reworked mechanism for coverage-ignore
The coverage-ignore feature now only uses the directive 
and produces consistent output in all views and report files.

To this end, the following aspects are no longer supported and have been removed:
* the DAX tag 
* the attribute coverage-ignore in the files lists in the Preprocessor view
* the context menu entry “Exclude from project coverage” 
  in the preprocessed files list
* the ignored attributes of the  tags in the XML report

Please note that previous configurations cannot be converted automatically.
DAX configurations can be converted manually by replacing DAX entries such as


by an AAL annotation

  "file.c" insert comment: ASTREE_attributes(coverage_ignore);

which is equivalent to writing the comment /* ASTREE_attributes(coverage_ignore) */ 
into file.c. Note that file names in AAL are resolved by unique suffix. 
Therefore, the path to the file can often be omitted.

AbsInt License Manager
The ALM now allows specifying a log file and log size. 
All connections to the server are then logged to the file in the JSON line format. 
After the specified log size is exceeded, the log file is rotated.

* --log-file <file> creates the log file, otherwise no log file is created
* --max-log-file-size <size> specifies the maximum log size in MB

Further changes
* Added support for the C language version ISO/IEC 9899:2018
 (configured by setting the option c-version to C18).
* Astr´e now also reports all directives that are inserted 
  by automatic partitioning, loop unrolling, and further heuristics.
* The consequence and alternative of the conditional operator ?: 
  are now marked as unreachable when the analyzer detects them 
  to be unreachable. This also affects the rule check unreachable-code 
  associated with the rules CERT.MSC.12, CWE.561, M.14.1, M2012.2.1, 
  and X.A.5.22.
* Improved precision on code that uses the builtin functions 
  __builtin_isfinite, __builtin_isinf, and __builtin_isnan.
* __ASTREE_alarm((raise_at_caller; ...)); directives now produce 
  the exact same output as __ASTREE_alarm((raise_here; ...)); 
  directives that appear in a function with the attribute raise_at_caller.
* The new option dump-volatiles prints all variables and fields 
  that are treated as truly volatile by Astrée.
* Astrée can now prove the absence of out-of-bound array accesses 
  of the form a[i-j] or a[i+j] when i-j or i+j, respectively, is known 
  to be in range.
* The analyzer now tracks pointer arithmetic in integer types for pointers 
  that are cast to integer types and back again.
* The limit for the size argument of __astree_memcpy, __astree_bzero, 
  and __ASTREE_access changed to 2^61-2.
* When Astrée can prove that the size argument for memcpy or 
  __astree_memcpy definitely exceeds the size of the target memory block, 
  it now signals the issue as definitely occurring and stops the analysis 
  for the affected context.
* Pressing the analysis stop button during an analysis no longer terminates 
  the analyzer immediately. Rather, the abstract interpreter performs a 
 "soft stop" during which it collects partial results up to the point 
  at which it was stopped. The collected data can give valuable insights 
  for fine-tuning the analysis, in particular while setting up long-running 
  analyses on large code.
* Improved the interpolation domain to remove false alarms about 
  division by zero in interpolation functions, in particular 
  for TargetLink code.
* Improved the performance of the state machine domain 
  when used in conjunction with separate functions.
* Astrée now discards partitioning directives when 
  the partitioned expression or variable:
  - is volatile,
  - or smashed,
  - or may point to more than one target,
  - or may be asynchronously written by another process 
    at the start of partitioning.
  It is possible to make the analyzer report ignored directives 
  by enabling the new diagnostic rule B.1.5.
* Astrée now shows scheduling contexts and state machine contexts 
  in alarm messages.
* Improved the __ASTREE_partition_ranges directive to generate 
  more appropriate partitions for small floating point intervals.
* Improved the precision of ratio expressions a * b / c 
  when the analyzer can infer that 0 <= b <= c.
* DAX files may now contain multiple occurrences of the tags 
  annotations, files, options, parser-ignore, preprocess, and reports.
* The names of preprocessor configurations are now required to be unique. 
  This requirement holds globally, i.e. reusing the name 
  of a sub-configuration in a different root configuration 
  is also forbidden. The name of a configuration may only 
  be re-used to explicitly overwrite or modify that configuration. 
  This intent must be indicated by adding the new attribute 
  to the <config/> tag. Overwriting or modifying configurations 
  must always happen at the top level, even when affecting 
* The keyword "original" for AAL annotations to insert 
  __ASTREE_attribute directives is now deprecated. 
  The old syntax

    original "file.c" insert: __ASTREE_attributes((coverage_ignore));

  should be replaced with the following new syntax:

    "file.c" insert comment: ASTREE_attributes(coverage_ignore);

* Fixed an issue that in rare cases could cause the analyzer 
  to abort with an exception when the Boolean domain and the option 
  exclude-signed-in-unsigned-overflows were both activated.
* Fixed an issue that in rare cases could cause the analyzer 
  to abort with an exception when the interpolation domain was enabled.
* Fixed an issue that prevented the option analysis-entry 
  from having an effect in astree-cxx mode for C++ analysis.

Integration with KEIL μVision
Updated the keil_intrinsics.h file that is shipped with the AbsInt toolbox 
for μVision, to filter/rewrite more keywords. Users that use this header 
may need to remove the following parser filters and macro definitions 
from their project configurations:


Rule sets and checks for C
The new rule check function-like-macro-expansion (CERT.PRE.0, M.19.7, 
M2012.D.4.9) allows for reporting the expansion of function-like macros.

Rule sets and checks for C++
* Added new rule set M202x-DRAFT to support the public review process 
  of the draft rules for the next release of MISRA C++. 
  Please note that this rule set is still under development. 
  Rule numbers and the set name are preliminary and will change 
  with the release of the final document.
* Added support for the following CERT rules:
  * CERT-CPP.INT.50 (check cast_integer_to_enum)
  * CERT-CPP.MEM.55 (check operator-new-requirements)
  * CERT-CPP.MEM.57 (check default-new-overaligned-type)
  * CERT-CPP.STR.50 (check check_stream_input_char_array)
* Added support for AUTOSAR rule AUTOSAR.18.5.9A
* The new diagnostic rule A.CPP.4.1 warns if the result of the evaluation 
  of an expression depends on the order of evaluation of sub-expressions 
  in C++ code.
* The new check floating-type-name (M.6.3, M2008.3.9.2, M2012.D.4.6, X.A.5.6) 
  reports the use of unnamed floating-point types.
* The rules M2008.16.1.1 and AUTOSAR.16.1.1M are now fully checked.
* The rules M2008.16.2.3 and AUTOSAR.16.2.3M can now configure the check 
  include-guard-missing to allow comments at all positions in and around 
  include guards.

Rule sets and checks specific to Astrée
* New informational diagnostic rule B.1.5 that warns when thresholds 
  of __ASTREE_partition_begin and __ASTREE_states_track are exceeded 
  during the analysis, causing the analyzer to ignore them in the 
  affected contexts. Note that this rule is not enabled by default.
* New diagnostic rule B.1.6 that warns when the analyzer loses precision 
  on memcpy and may lose track of copied pointer values.

Enhancements, clarifications, refinements for both C and C++
* Improved the behavior of the checks identifier-unique and static-identifier-reuse 
  to avoid double reporting and remove false negatives for rule M.5.5 and M2012.5.9:
  * The check static-identifier-reuse no longer reports non-static declarations, 
    but only the identifier of a static declaration (including a reference 
    to the conflicting declaration). It now reports conflicts in all namespaces, 
    including types, tags etc.
  * The check identifier-unique no longer reports declarations of internal linkage 
   (which are already covered by the check static-identifier-reuse).
* The option allow-boolean-constants has been extended to also transitively apply 
  to operations that do not change the (essential) type of their operands, such as in 
  _Bool b = condition ? 1 : 0;
* Fixed an issue which could cause rule violations to be reported for configurations 
  that did not enable the respective checks when using more than a single 
  rules configuration.
* The metrics CALLING and RPATH now consider cross-language function calls 
  between C and C++ code.
* Fixed corner cases leading to incomplete file metrics (CDFILE, FUN, LINE, PLINE) 
  and inaccurate metrics (CALLING, RPATH, CDFILE, CDFUN), eliminating false 
  positives and false negatives for the respective threshold checks 
 (min-comment-density, min-comment-density-his, min-number-of-calling-functions, 
  max-number-of-calling-functions, max-number-of-recursive-paths).
* Improved the check include_syntax (M2012.20.3, M2008.16.2.6, M.19.3) 
  to warn about extra tokens in include directives. This removes false negatives 
  for the associated rules.
* The function metrics table now distinguishes internal linkage functions 
  by the translation units in which they are defined, using the scheme 

Enhancements, clarifications, refinements for C code
* Rule M2012.21.12 is now configurable with respect to the macro 
  identifiers to be reported. Such identifiers are now reported 
  by the check bad-macro-expansion instead of stdlib-use-fenv.
* The following checks are no longer applied to code excluded 
  by the preprocessor:
  * define-in-block (M.19.5)
  * min-comment-density-his (T.14.1)
  * null-statement (M.14.3, X.A.4.11)
  * null-statement-strict (X.A.4.11)
  * pragma (X.A.3.10)
  * pragma-usage (A.5.2, M.3.4)
* Removed false positives for the check definition-duplicate 
 (M.8.9, M2012.8.6). It no longer reports tentative definitions 
  for which another definition exists solely in the same translation unit.
* Removed false negatives for the check array-initialization (M2012.9.3) 
  which did not warn about code like 
  char arr[10] = {0U}; 
  Only {0} without sign suffix is allowed in such context 
  by exception 1 of rule M2012.9.3.
* Corrected the essential type (cf. MISRA C:2012) computed for 
  integer constants (including constant expressions) of type 
 (un)signed long or long long, for which the type of lowest rank rule 
  does not apply. This resolves false negatives and false positives 
  for all rules concerned with the essential type of expressions, 
  such as M2012.10.x.
* Removed false negatives for the checks:
  * object-pointer-diff-cast, object-pointer-diff-cast-implicit 
   (M.11.4, M2012.11.3), object-pointer-diff-cast-strict, and 
    object-pointer-diff-cast-strict-implicit (M.11.4), which now 
    also warn about conversions for which the unqualified object type 
   (cf. M2012.11.3) differs only in const or volatile qualification.
  * sizeof (CERT.EXP.44, M.12.3, M2012.1.3, M2012.13.6), 
    which did not warn about side effects nested in variable-length 
    arrays and about volatile accesses that are not covered 
    by the exception of M2012.13.6.
  * reserved-declaration (CERT.DCL.37, ISO17961.resident, 
    M.20.2, M2012.21.2), which did not warn about the declaration 
    of an identifier starting with an underscore.
  * identifier-unique-extern-relaxed (X.C.NAM.5), which did not 
    warn about non-compliant variables if a local non-extern 
    variable with same name existed in the same project.
  * cast-pointer-void (M2012.11.5) on C code, which did not warn 
    about conversions from type pointer to T when T was typedef'ed 
    to void, e.g. typedef void T; 
* The checks language-override, language-undefine, and 
  reserved-declaration now take the configured c-version into account. 
  Removed the now obsolete checks language-override-c99, 
  language-undefine-c99, and reserved-declaration-c99. 
  This affects the rules CERT.DCL.37, ISO17961.resident, 
  M.20.1, M.20.2, M2012.21.1, M2012.21.2, and X.A.6.2.
* Removed false positives for the checks:
  * redeclaration (A.1.9, CERT.MSC.40, M.1.1, M2012.D.2.1, 
    M2012.1.1, M2012.8.5, X.E. If the c-version option 
    is set to C11 or C18, repeated typedefs that are compliant 
    with the standard are no longer reported.
  * unused-typedef (M2012.2.3) and unused-tag (M2012.2.4), 
    which no longer warns about types used solely within C++ code.
* A C function with internal linkage that is included in multiple 
  translation units is now considered a single function 
  unless its metrics differ between translation units. 
  This especially affects the metric CALLING and the rule checks 
  min-number-of-calling-functions and max-number-of-calling-functions.
* The rule check distinct-identifiers-macros (M.2012.5.5) 
  no longer warns about identifiers in macro definitions 
  skipped by the preprocessor.
* Improved coverage for rule M2012.14.2 thanks to the new checks 
  loop-counter-modification and multiple-loop-counters.
* The check inappropriate-bool (M2012.10.1) no longer warns 
  if the first operand of the conditional operator ?: 
  is of pointer type (see MISRA C:2012 TC 2.16).
* The checks essential-type-assign (M2012.10.3), composite-cast, 
  and composite-cast-width (M2012.10.8) no longer warn about 
  expressions of pointer type (see MISRA C:2012 TC 2.16).
* The check inappropriate-char-usage (M2012.10.2) now warns 
  when the integer operand has a type of rank greater than 
  that of int (see MISRA C:2012 TC 2.19).
* The new check inappropriate-switch-case (M2012.10.3) 
  warns about case statements with inappropriate essential type. 
  This removes false negatives for rule M2012.10.3.
* The check controlling-invariant-expression (M.14.1, M2012.2.1, 
  M2012.14.3) now also warns about do .. while(<E>); loops, 
  if the controlling expression <E> is known to always evaluate 
  to false, but is not an integer constant expression of 
  essentially Boolean type (see MISRA C:2012 TC 2.27). 
  This removes false negatives for rule M2012.14.3.
* The check return-implicit (CERT.MSC.37, M.16.8, M2012.17.4) 
  now exempts the main function, as it is defined to return 0 
 (see MISRA C:2012 TC 2.30). This removes false positives 
  for rule CERT.MSC.37.

Enhancements, clarifications, refinements for C++ code
* The following rule checks for C have been extended to also consider
  identifiers from C++ code as potential naming conflicts:
  * distinct-extern (CERT.DCL.40, ISO17961.funcdecl, M2012.5.1)
  * distinct-identifiers-macros (M2012.5.5)
  * identifier-unique-extern (M.5.7, M2012.5.8, X.C.NAM.5)
  * identifier-unique-extern-relaxed (X.C.NAM.5)
  * identifier-unique-macro (M.5.7)
  * identifier-unique (M.5.7)
  * identifier-unique-relaxed (X.C.NAM.5)
  * static-identifier-reuse (M.5.5, M.5.7, M2012.5.9)
* The rule check ambiguous-identifiers (AUTOSAR.2.10.1M, M2008.2.10.1)
  has been extended to also consider identifiers from C code
  as potential naming conflicts. It also no longer warns about
  identifiers in files excluded from rule checks.
* Removed false negatives and false positives for the check
  bad_function (AUTOSAR.15.5.2A, AUTOSAR.18.9.1A, AUTOSAR.26.5.1A,
* Removed false negatives for:
  * integral-type-name (AUTOSAR.3.9.1A, M2008.3.9.2) which failed
    to report type (signed/unsigned) long long in C++ code;
  * alignas, atomic-qualifier, atomic-specifier, floating-type-name,
    integral-type-name, integral-type-name-extended, long-double,
    pointer-attribute, restrict, wchar-t, which were not applied
    to the operand of sizeof.
* Removed false positives for the checks:
  * multiple-output-values (AUTOSAR.8.4.4A),
    c-style-cast (AUTOSAR.5.2.2A, M2008.5.2.4),
    implicit-non-void-lambda-return-type (AUTOSAR.5.1.6A), and
    function-return-unused (M2008.0.1.7, AUTOSAR.0.1.2A)
    in dependent contexts
  * member-function-missing-const and member-function-missing-static
   (M2008.9.3.3, AUTOSAR.9.3.3M) to no longer report violations
    in classes with dependent bases
  * conditional-as-sub-expression (AUTOSAR.5.16.1A) with non-trivial
    data types
  * clean-global-namespace (M2008.7.3.1, AUTOSAR.7.3.1M) reported
    for parameters within function types
  * incomplete-data-member-construction (AUTOSAR.12.1.1A)
    for potentially delegating constructors, to no longer report
    violations for constructors with a single member initializer
    that names a dependent type
  * scattered-data-member-initialization (AUTOSAR.12.1.3A)
    in the context of templates
  * uninitialized-member-modification-in-constructor
   (AUTOSAR.12.6.1A) for constructors in which members are initialized
    by a delegating constructor, to no longer report violations
    for constructors with a single member initializer that names
    a dependent type
* The check integral-type-name (AUTOSAR.3.9.1A, M.6.3, M2008.3.9.2,
  M2012.D.4.6, X.A.5.6) no longer reports floating-point types.
  This removes false positives for AUTOSAR.3.9.1A,
  which is not concerned with floating-point types.
* The check exception-specification-mismatch-link (AUTOSAR.15.4.3A,
  M2008.15.4.1) now treats throw() as a non-throwing exception
  specification. This removes false positives and false negatives.
* The checks bitop-type (M2008.5.0.21, AUTOSAR.5.0.21M) and
  bitop-recast (AUTOSAR.5.0.10M, M2008.5.0.10) no longer report
  violations in type-dependent contexts where the operation in question
  cannot be determined to be a bit operation vs. a call to an overloaded
  operator. This removes false positives for the aforementioned rules.
* The following checks no longer warn in dependent contexts
  if it is unclear whether a dependent type is bool or can be
  converted to bool by a bool() operator. This removes false positives.
  * non-boolean-loop-control (M2008.6.5.6, AUTOSAR.6.5.6M)
  * non-boolean-if-condition (M2008.5.0.13, AUTOSAR.5.0.2A)
  * non-boolean-loop-condition (M2008.5.0.13, AUTOSAR.5.0.2M)
  * non-boolean-logop (M2008.5.3.1, AUTOSAR.5.3.1M)
  * non-boolean-conditional (M2008.5.0.14, AUTOSAR.5.0.14M)
  * relational-operator-return-type (AUTOSAR.13.2.3A)
  * continue-in-bad-loop (M2008.6.6.3, AUTOSAR.6.6.3M)
* The check comma-operator (M2008.5.18.1, AUTOSAR.5.18.1M) no longer
  warns about uses of the comma operator in C++ fold expressions.
* The PATH metric now takes throw and catch statements in C++ code
  into account. This can yield additional violations of the associated
  check max-number-of-paths (T.9.1).
* The check reinterpret-cast (AUTOSAR.5.2.4A) has been split into
  reinterpret-cast and reinterpret-cast-extended.
* The check incomplete-base-construction (AUTOSAR.12.1.1A,
  M2008.12.1.2) has been split into incomplete-base-construction
  and incomplete-base-construction-strict.
* Fixed an issue that caused /* ASTREE_comment(...) */ and
  /* ASTREE_suppress(...) */ source directives with a set of check keys
  to only apply to the last key in the list.
* Improved the reporting of C++ rule violations inside of macros
  by printing the relevant macro expansion stack.
* The check goto-nesting (M2008.6.6.1, AUTOSAR.6.6.1M) now treats
  switch clauses (see M2008.6.4.3) as blocks and thus warns
  more strictly about gotos into switch clauses.
* The check clean-global-namespace (M2008.7.3.1, AUTOSAR.7.3.1M)
  now treats namespace aliases as namespace declarations.
  Thus they are no longer reported as violations.
* The check direct-recursion (AUTOSAR.7.5.2A, M2008.7.5.4)
  no longer warns about recursion that occurs in constexpr functions
  if all callers are core constant expressions. In this case,
  there is no recursion at runtime.
* The checks bitop-type (M2008.5.0.21, AUTOSAR.5.0.21M) and
  underlying-signedness-conversion (M2008.5.0.4, AUTOSAR.5.0.4M)
  now honor the option allow-signed-constant-with-unsigned.
* Revised the check initializer-list-constructor-rival
 (AUTOSAR.8.5.4A) to improve the quality of the rule implementation:
  * Constructors with an std::initializer_list& parameter
    are also treated as initializer-list-constructors.
  * Constructors are treated as initializer-list-constructor
    only if the initializer list is the first parameter.
  * The violation is now reported for all constructors
    of the violating class.
* The default rule argument for AUTOSAR.5.1.1A now also specifies
  std::operator<< as a logging mechanism.

Server and server controller
The server controller now also shows incompatible servers that run 
on previous releases. Incompatible servers are grayed out in the list 
of available servers.

Unused comments
* The unused comments table in the Findings view can now be sorted 
  by clicking on the column headings.
* The unused comments table in the Findings view can now be filtered
  by pressing Ctrl+F while the table is in focus.
* Unused comments can now also be drag-and-dropped to a finding 
  in the Findings view from the corresponding editor overlay.
* Added copy/cut operations to the context menu for editor overlays 
  for alarm comments.
* Used comments can be copied to other findings in the Findings view 
  by dragging and dropping them from the corresponding editor overlay.

Taint analysis
* Added new view Locations -> Taints to the output area 
  that lists all code locations with taints.
* When taint analysis is enabled, variables that are tainted with a given hue 
  can now be highlighted in the editor views by selecting a hue to display 
  in the Locations -> Taints view of the output area.

Other improvements
* The control-flow and call graph views now show which functions 
  have been analyzed separately.
* The new context menu entry "Export annotations" in the preprocessed 
  files list allows to export the annotations for selected files 
  if a mapping to the insertion location exists (as indicated by 
  annotation overlays in the editor view or the @ symbol 
  in the Annotations view).
* The new "Edit attributes..." action in the context menu 
  of the original source files list allows to generate and edit 
  annotations for file attributes. An orange dot at the file icon 
  indicates the existence of attributes.
* The new "Show/hide missing files" action in the context menu 
  of the original source files list toggles the display
  of original source files that have been referenced 
 (e.g. from line directives in preprocessed files) but could not 
  be found and uploaded. Missing files are shown grayed-out.
* In the Findings view, the previous location information 
  for unused comments is now more often available. 
  The "Display in Editor" in the context menu allows 
  to navigate to that location.
* The Classes view and the class graph for C++ no longer display 
  C-like structs and unions.
* Rearranged some entries of the Preprocess view to improve usability.
* Invalid and duplicated tags in DAX files are now more consequently 
  reported as errors instead of being silently discarded.
* The AUTOSAR configuration dialog now displays the information 
  from ARXML file(s) used for the latest analysis run, if these 
  files are not already available on the local machine 
 (e.g. when inspecting an analysis project that ran 
  on a different machine).
* In custom report configurations, it is no longer necessary 
  to specify files by their absolute paths. Instead, it's now 
  possible to refer to them by plain file name, or unique suffix 
  in case the plain name is not unique. This is particularly useful 
  for specifying custom report configurations in DAX files. 
  To this end, the <file/> tag in custom report configurations 
  now also accepts a new attribute 
* Improved the XML report format for representing the optional 
  CAUSE lines of ALARM messages and fixed a regression which could 
  cause such lines to be missing from the XML report in recent releases.
* In the analysis results filter, files and directories 
  no longer need to be specified by their absolute paths. 
  Rather, they can alternatively be specified by plain file name 
  or unique suffix (in case that the plain name is not unique). 
  This is particularly useful for specifying the result filter 
  in DAX files. To this end, the <path/> tag now accepts 
  the new attribute 
* Improved performance of searching in the Output view.
* The "type" attribute of the "result" tag in the XML result file 
  is now set to "n/a" if the client fails to connect to a project, 
  e.g. due to parse errors in the DAX file.
* The AAF export now allows omitting large optional data 
  from the exported files. When exporting AAF files in batch mode, 
  the optional data can be omitted by adding the new option 

GUI fixes
* Fixed an issue that could cause newly added alarm comments to get lost 
  when using the optional comment mode "Patterns" and not explicitly saving 
  the new comments via Ctrl+S or Project -> Save before performing 
  further actions in the GUI.
* Fixed sorting in the Reads and Writes columns of the data flow view.
* Fixed the generation of AAL annotations for definitions of static functions 
  without storage class specifier. The AAL path used to be missing a file name, 
  which is required to match a static function.
* Fixed an issue that could cause the call graph view to show incorrect numbers 
  of alarms and errors per function.
* Fixed an issue that could cause the hint "results are intermediate" 
  to not be removed when opening a finished analysis after closing 
  an analysis that's still running.
* Fixed the display of file paths in the rules configuration when opening 
  a project on Windows that was created on Linux or vice versa.
* Fixed an issue that in rare cases caused the client to fail 
  reading analysis results correctly or crash in the process.

Frontends and preprocessor
* Updated the LLVM/clang toolchain to version 14.
* Improved error handling to avoid or clarify frontend_clang errors 
  stating "No analyzed file could be found for...".
* The C frontend now rejects code like 

    union tag x; 

  when "tag" refers to a struct and vice versa.
* The C frontend now supports the builtin functions 
  __builtin_isnanf and __builtin_isnanl.
* The new source directive /* ASTREE_attributes(...) */ can be used 
  to associate attributes with original source files, analogously to 
  using the __ASTREE_attributes((..)); directive at file scope.
* Improved the handling of Astrée directives in AAL insertion. 
  The following directives are no longer counted as statement 
  during the evaluation of an AAL position specification:


* Parser filters are no longer applied in preprocessing directives 
  such as #if, #ifdef, and #ifndef.
* The C frontend now supports GCC's __int128 type specifier.
* The C frontend now more thoroughly reports array declarations 
  with non-constant or non-integer size expressions.
* In accordance with the C standard (C90, C99/C11/C18, 
  the C frontend no longer rejects the dereference of void* as long as 
  the result is not used. Instead, the analyzer will stop with an error 
  when reaching such an expression.

Stub libraries, ABIs, OS and compiler configurations
* The assert macro, which maps "assert" to "__ASTREE_assert", 
  can now also be used in expressions, rather than only in statements. 
  The macro can now also be used in a C++ constexpr context 
  from language version C++14 onwards.
* Improved the extraction of OS information from ARXML files 
  when the core specification is missing.
* Removed option to restrict the analysis of an AUTOSAR project 
  to a given core or application.
* Extended the use of the attribute "hide_directives" 
  to the OS stub libraries.
* Optimized the implementation of the SetEvent, ClearEvent, and 
  WaitEvent functions in the OSEK stub library.
* Improved the STL container abstractions in Astrée's 
  standard C++ library to fix frontend issues with types 
  that are not copy-constructible.

New test cases in the Astrée QSK

The test case qk_aal_insert_at_file_scope_into_original has been removed.

New test cases in the RuleChecker QSK

The test cases qk_check_language_override_c99, qk_check_language_undefine_c99, 
and qk_check_reserved_declaration_c99 have been removed from the RuleChecker QSK.

RuleChecker QSK test cases extended to C

RuleChecker QSK test cases extended to C++

Last updated on 9 March 2023 by Copyright 2022-2023 AbsInt.
An HTML version of these release notes is available at