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 action “Edit attributes…” 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 ASTREE_attributes(coverage_ignore) 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 <coverage-ignore>
  • 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 <files> 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

<coverage-ignore>
   <file>preprocessed/some/path/to/file.c</file>
</coverage-ignore>

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 Astrée 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 on 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 combine="(overwrite|merge)" to the <config/> tag. Overwriting or modifying configurations must always happen at the top level, even when affecting sub-configurations.
  • The original keyword 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);

Fixes

  • 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:

  • __ALIGNOF__
  • __forceinline
  • __global_reg(...)
  • __int64
  • __INTADDR__(X)
  • __irq
  • __packed
  • __pure
  • __smc(...)
  • __softfp
  • __svc(...)
  • __svc_indirect(...)
  • __svc_indirect_r7(...)
  • __value_in_regs
  • __weak
  • __writeonly
  • __declspec(...)

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, and fixes

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 <function>@"<file>".

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.5.2.2.10). 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.

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, CERT-CPP.CON.37C, CERT-CPP.MSC.30C, CERT-CPP.MSC.50).
  • 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.

Client GUI, batch mode, and report files

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 source-kind=preprocessed|original|all.
  • 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 source-kind=preprocessed|original|all.
  • 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 --export-skip-tu-data.

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:
    • __ASTREE_states_track
    • __ASTREE_states_merge
    • __ASTREE_wrapper_call
    • __ASTREE_trash
    • __ASTREE_access
    • __ASTREE_taint
  • 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 §3.2.2.2, C99/C11/C18 §6.3.2.2), 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

  • qk_aal_comment_pattern_basic
  • qk_aal_file_insert_comment
  • qk_check_ignored_states_track
  • qk_check_ignored_partitioning
  • qk_directive_attributes_source
  • qk_option_component_pairs_under_observation
  • qk_option_dump_volatiles
  • qk_option_taint_components
  • qk_rule_b_1_5

The test case qk_aal_insert_at_file_scope_into_original has been removed.

New test cases in the RuleChecker QSK

  • qk_aal_comment_pattern_basic
  • qk_check_floating_type_name
  • qk_check_function_like_macro_expansion
  • qk_check_imprecise_memcpy
  • qk_check_inappropriate_switch_case
  • qk_check_incomplete_base_construction_strict
  • qk_metric_locvar
  • qk_rule_b_1_6

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

  • qk_check_loop_counter_modification
  • qk_check_multiple_loop_counters

RuleChecker QSK test cases extended to C++

  • qk_check_case_clause
  • qk_check_cast_pointer_void
  • qk_check_define_in_block
  • qk_check_floating_point_loop_counter
  • qk_check_integer_suffix
  • qk_check_integral_type_name
  • qk_check_loop_termination
  • qk_check_null_statement
  • qk_check_octal_constant
  • qk_check_pointer_depth
  • qk_check_stdlib_use_system
  • qk_check_type_compatibility
  • qk_check_unclosed_ifgroup
  • qk_check_undef