Astrée and RuleChecker release 25.04

Support for C++23

Added general support for C++23. Some features are not fully supported just yet, notably modules and coroutines. Further details can be found in the user manual.

Support for MISRA C:2025

The new C:2025 rule set announced by MISRA last month is supported by Astrée and RuleChecker from that very day.

Of the 223 rules in the MISRA C:2025 rule set, Astrée supports 222, and the standalone RuleChecker supports 219.

Further details can be found as usual under “Help” → “Compliance matrices”.

New features for IDE integration

  • Added support for the Language Server Protocol (LSP) to allow integration into any IDE or code editor that provides an LSP client.
  • Added a plugin for Visual Studio Code based on LSP.
  • The standalone Eclipse plugin is now deprecated, as it can be replaced by installing LSP4E in Eclipse and configuring it to use Astrée’s LSP server.

OAuth2 support

Added support for OAuth2-based authorization. The user group claim from an OAuth2 UserInfo endpoint can be mapped to user and admin roles on the Astrée analysis server.

Improved precision

  • Improved precision of dynamic octagon packs in loops and partitions.
  • To improve the precision of static folding for unions (triggered by options smash-threshold or smash-const-threshold), the folding now takes into account the memory layout of all fields of the union type.
  • After reporting a (potential) call using a NULL or invalid function pointer, the analysis now carries on for the subset of valid function pointers.
  • When evaluating a float expression of the form a / (a + e) where the variable a and the expression e are positive, and a + e is > 0, the analysis now infers that the result is in the range [0.0, 1.0].
  • Improved analysis for loops that are not already statically unrolled (using directives or heuristics). Such loops may now be unrolled dynamically to increase precision. Whether dynamic unrolling is applied and for how long it continues depends on the exit condition of the loop and the cost of analyzing the loop body. The maximum cost is controlled by the new option dyn-unroll-cost.
  • Improved the interaction between octagon and symbolic domain to improve precision.
  • Improved __ASTREE_global_assert on pointers. After reporting a global_assert_failure alarm the analysis now proceeds with only the asserted pointer bases instead of adding INVALID in some cases.
  • Improved precision of the interaction between symbolic domain and other domains when partitioning a variable.
  • To further improve precision, the analysis now discards program executions that involve a function call with incompatible parameter conversion from integer to pointer type when the size of the integer is not equal to the size of the pointer type. Such incompatible conversions are already reported as a type-A alarm incompatible_parameter_type.
  • Improved the efficiency of dynamic octagon packs that are created inside of partitions.
  • Improved precision when starting processes. Only program points at which a corresponding __astree_start_process intrinsic is reached are taken into account. Processes for which no such intrinsic is reached are assumed to never run.

Options

  • Added new heuristics for forming packs for boolean variables that are used to encode first writes to other variables. The new heuristics is controlled by the new option first-logic-packs.
  • The partition option for controlling the partitioning domain is now also available for C++ (analysis mode astree-cxx).
  • The new option globals-are-initialized controls whether global and static variables without explicit initializer are considered initialized (globals-are-initialized=yes) or uninitialized (globals-are-initialized=no). The option is enabled by default. Disabling it does not affect the initial value of such variables.
  • Corrected the detection of boolean variables in boolean packs to ensure that the upper bound provided by the option max-bool-vars is respected.
  • The smashing of string literals is no longer controlled by the option smash-threshold, but by the new option smash-const-threshold.
  • Removed support for the deprecated ABI setting alignof_char_array.

Directives

  • New directives:
    • __ASTREE_add_widening_thresholds
      allows to manually supply widening thresholds for variables.
    • __ASTREE_partition_bases
      allows partitioning according to the different memory blocks that a pointer may point to.
    • __ASTREE_partition_merge_closest
      merges partitions opened by the syntactically closest partitioning directive.
  • C++-specific changes (astree-cxx mode):
    • Fixed directive handling to prevent unexpected output from __ASTREE_alarm or __ASTREE_print directives when the input string contains escape sequences, as well as unexpected frontend errors (e.g. when using __ASTREE_absolute_address with anonymous structs/unions).
    • Fixed the behavior of __ASTREE_comment and __ASTREE_suppress directives that are inserted into code using original-source annotations for C++. When using relative source ranges without file IDs, they now apply relative to the point at which they were inserted.
    • __ASTREE_boolean_pack directives are no longer reported as “semantic hypotheses”.
    • Astrée now allows using a const-qualified void pointer as first argument for the __ASTREE_access directive.
    • Precision-related directives (for loop unrolling, partitioning, etc.) can now be added to C++ constexpr functions, to improve precision for invocations in non-const evaluated contexts.
  • Improved handling of invalid arguments:
    • Invalid uses of the __ASTREE_max_clock directive with an argument ≤0 are now rejected. In such cases the tool reports a violation of the check invalid-directive.
    • Invalid domain names in __ASTREE_log_vars are now reported not as errors but as a violation of the check invalid-directive.
    • The directives __ASTREE_attributes((...)) and /* ASTREE_attributes */ are now validated more strictly. If any of the specified attributes is invalid, the whole directive is discarded with an alarm check_invalid_directive.
    • Invalid arguments of function type in __ASTREE_octagon_pack and __ASTREE_boolean_pack directives are now rejected immediately.
    • The __ASTREE_comment directive now requires at least one finding-key.
  • The __ASTREE_octagon_pack directive now supports the use of the dereference operators * and -> within access paths for the provided variables.
  • The directive __ASTREE_modify can now be used in global scope to express modification after initialization but before starting the analysis entry function.
  • The __ASTREE_global_assert directive no longer overrides implicit initializers of asserted variables. This can lead to new alarms when the initial 0 value is not in the asserted range.
  • Const variables that are modified by an __ASTREE_modify directive with a range argument are now considered written and initialized after the directive.
  • The directive __ASTREE_alarm(()) now allows using a custom message text when raising alarms about rule violations.
  • The directive __ASTREE_global_assert can now be used for asserting that a variable (or part of it) is always initialized. The new syntax is 
    __ASTREE_global_assert((Vp; initialized));
  • The __ASTREE_modify directive now accepts the new keyword restrict_enum_values. It can only be used with variables of enum type. The directive then sets the value to the set of enumerator values instead of the range of the underlying type.
  • The __ASTREE_volatile_input directive now accepts the new keyword restrict_enum_values. If the target variable or a member is of enum type, the keyword restricts the range of possible values to values of the enumerated type, rather than to the range of values of the underlying integer type.

TargetLink

  • Added support for TargetLink 24.1.
  • Fixed double import of annotations and comment patterns from DAX when the toolbox options “Exclude TargetLink standard files from project coverage” and “Additional analysis files/DAX file” are both enabled.
  • Prevented implicit conversion of Float32 min/max bounds to double when generating Astrée directives for ranges specified in the data dictionary by appending an F suffix to such bounds.
  • Ensured that min/max bounds from the data dictionary are preserved literally when no scaling is specified (offset is 0 and factor is 1).
  • Fixed ranges in generated directives for scaled signals with a resolution >231 or <2−31.
  • Fixed stub generation for lookup and interpolation routines when TargetLink base types (e.g. Float32) have been renamed.

General improvements

  • Fixed an issue that could cause the octagon domain to stop the analysis with an exception when analyzing certain expressions with left shifts.
  • Calling __astree_set_process_core with an imprecise core argument no longer raises an invalid_usage_of_concurrency_intrinsic alarm. Instead, the analyzer approximates the core as unknown, allowing interactions with all other cores.
  • Improved the reporting and display of context information for definite runtime error messages. The new representation makes it clearer which contexts are stopped.

Transport layer security

If you are upgrading your client from a release older than 23.10, make sure that your License Manager is upgraded as well. This is necessary due to the TLS-encrypted connection between the client and the Manager that was introduced in 23.10.

Linux support

In light of the Cyber Resilience Act, support for RHEL 7 is now deprecated.
In the near future, the Linux version will require at least RHEL 9 (or compatible).

Quick overview

The following rules are affected by this release.

CWE
242
252
398
467
468
475
478
479
480
481
482
484
561
570
571
676
1007
1420
1422
1423
CERT
ARR.38
CON.33
CON.35
ENV.31
ENV.32
FIO.34
FLP.36
INT.30
INT.35
INT.36
MSC.32
MSC.33
MSC.40
MSC.41
POS.34
POS.47
POS.49
POS.51
POS.52
POS.53
POS.54
STR.31
STR.32
MISRA C:2025
all new
MISRA C:2023
1.1
2.5
5.4
9.7
11.4
11.5
12.4
14.3
20.7
21.17
21.26
22.11
22.14
22.15
22.16
22.17
22.18
22.20
23.7
D.2.1
D.4.3
D.5.3
MISRA C:2012
1.1
2.5
5.4
11.4
11.5
12.4
14.3
20.7
D.2.1
D.4.3
A1.21.17
A3.23.7
MISRA C:2004
1.1
2.1
8.5
11.3
12.11
19.4
C++
AUTOSAR.5.2.8M
AUTOSAR.10.3.2A
CERT-CPP.EXP.34C
CERT-CPP.STR.31C
M2008.5.2.8
M2023-CPP.8.1.1
M2023-CPP.8.1.2
M2023-CPP.8.2.6
M2023-CPP.13.3.1
Other
A.1.8
A.3.1
A.3.4
A.5.1
A.5.8
A.6.2
B.1.1
B.1.5
B.1.6
B.1.8
T.9.1
X.E.5.2.2.19

Rule sets and checks for C

  • Added the new MISRA C:2025 rule set.

  • Added dedicated rules for the following CWE guidelines:

    • CWE.242
    • CWE.252
    • CWE.398
    • CWE.467
    • CWE.468
    • CWE.475
    • CWE.478
    • CWE.479
    • CWE.480
    • CWE.481
    • CWE.482
    • CWE.484
    • CWE.561
    • CWE.570
    • CWE.571
    • CWE.676
    • CWE.1007
    • CWE.1420
    • CWE.1422
    • CWE.1423

  • Added support for the following MISRA C:2023 rules:

    • M2023-C.9.7
    • M2023-C.21.26
    • M2023-C.22.11
    • M2023-C.22.14
    • M2023-C.22.15
    • M2023-C.22.16
    • M2023-C.22.17
    • M2023-C.22.18
    • M2023-C.22.20
    • M2023-C.23.7
    • M2023-C.D.5.3

  • Added support for the following CERT rules:

    • CERT.ARR.38
    • CERT.CON.33
    • CERT.CON.35
    • CERT.ENV.31
    • CERT.ENV.32
    • CERT.FIO.34
    • CERT.FLP.36
    • CERT.INT.35
    • CERT.MSC.32
    • CERT.MSC.33
    • CERT.MSC.41
    • CERT.POS.34
    • CERT.POS.47
    • CERT.POS.49
    • CERT.POS.51
    • CERT.POS.52
    • CERT.POS.53
    • CERT.POS.54
    • CERT.STR.31
    • CERT.STR.32
    • CERT-CPP.STR.31C
  • Extended support for the rules CERT.INT.30 and CERT-CPP.EXP.34C.
  • Added support for rule M2012A3.23.7.

Rule sets and checks for C and C++

The new diagnostic check ineffective-file-list-entry (rule B.1.8) warns about nonexistent paths in path inclusion/exclusion lists (<paths/>) in rules and reached-code configurations.

Rule sets and checks specific to Astrée

  • New diagnostics checks:
    • unused-directive (B.1.5)
      reports the following directives if the respective domain is not active:
      • __ASTREE_boolean_pack
      • __ASTREE_octagon_pack
      • __ASTREE_partition_begin
      • __ASTREE_partition_calls
      • __ASTREE_partition_control
      • __ASTREE_partition_expr
      • __ASTREE_partition_merge
      • __ASTREE_partition_merge_last
      • __ASTREE_partition_ranges
      • __ASTREE_states_merge
      • __ASTREE_states_track
    • zero-size-alloc (A.3.4)
      reports if a memory allocation function in the standard library is called with an allocation size of 0.
    • fixpoint-computation (B.1.6)
      informs when the analyzer performs a fixpoint computation on a loop that has no explicit unroll directive.
    • value-specification-ignored (A.5.1)
      warns if the keyword restrict_enum_values is used in an __ASTREE_volatile_input directive with a variable or member of union type.
  • Updated the diagnostics check ignored-volatile (B.1.1) to only report volatile-qualified variables that are lacking an __ASTREE_volatile_input directive.
  • Removed false positives for the check constant-expression-wrap-around (CERT.INT.30, M.12.11, M2012.12.4, M2023-C.12.4). The check no longer reports conversion of integer values to _Bool.

Enhancements, clarifications, refinements, and fixes

Both C and C++

  • Improved the handling of constant conditions in the computation of the PATH metric to exclude impossible paths from the counting. This may remove violations of rule T.9.1 (max-number-of-paths).
  • The check cast-pointer-void (AUTOSAR.5.2.8M, M2008.5.2.8, M2012.11.5, M2023-C.11.5, M2023-CPP.8.2.6) no longer warns if the operand of the conversion is a call to one of the allocation functions malloc, calloc, realloc or aligned_alloc.

C code

  • Improved handling of sizeof().
    • Fixed non-termination of rule checks for long chains of “sizeof(...) +” in macros.
    • Removed false positives of the check macro-expansion (M.19.4) for parenthesized expression containing the sizeof operator.
    • Removed false negatives of the check macro-parameter-unparenthesized-expression (M2012.20.7, M2023-C.20.7) which did not report unparenthesized expressions containing the sizeof operator.
  • The check loose-asm (M.2.1, M2012.D.4.3, M2023-C.D.4.3) no longer warns about assembler code that is encapsulated in macros.
  • Violations of the check max-macros-defined (M.1.1, M2012.1.1, M2023-C.1.1) are now reported per translation unit.
  • The check unused-macro (M2012.2.5, M2023-C.2.5) now states the name of the respective macro, and additionally reports macros defined in the preprocessor configuration.
  • The check distinct-macro (M2012.5.4, M2023-C.5.4) now also reports conflicts with macro names stemming from the preprocessor configuration.
  • The diagnostic check excessive-interval (A.5.1) now also reports when no interval is provided for a value of enum type and the implicitly assumed interval (based on the underlying type of the enum) contains more values than the enum type.
  • Improved reported location for violations of the check header-definition (M.8.5). The alarm is now reported once per defined identifier, at the location of the declaration instead of the initializer.
  • Removed false negatives for the check header-definition (M.8.5), which only reported violations in files named *.h instead of files being subject to #include.
  • Improved reporting for the check pointer-integral-cast (A.3.1, CERT.INT.36, M.11.3, M2012.11.4, M2023-C.11.4). It now reports the types being converted.
  • The check macro-parameter-unparenthesized-expression (M2012.20.7, M2023-C.20.7) no longer warns about unparenthesized expressions delimited by square brackets or braces. Those cases are now reported by the check macro-parameter-unparenthesized-expression-strict (M2012.20.7, M2023-C.20.7).
  • The behavior of the checks controlling-invariant and controlling-invariant-expression (CWE.570, CWE.571, M2012.14.3, M2023-C.14.3) has changed. The exception for infinite loops and do while(0) no longer requires essentially boolean conditions, but literally 0 or 1.
  • Improved reporting of violations of the check strcpy-limits (CERT.STR.31, M2012A1.21.17, M2023-C.21.17). The message now provides the target type and the size of the copied string.
  • Previously reported as a fatal error, a string literal that is used within an initializer of an array and exceeds the size of the array being initialized is now reported as a violation of the diagnostics check initializer-excess (A.1.8, CERT.MSC.40, M.1.1, M2012.1.1, M2012.D.2.1, M2023-C.1.1, M2023-C.D.2.1, X.E.5.2.2.19).

C++ code

  • The diagnostic check config-function-unknown (A.5.8) is now also available for C++ (astree-cxx mode).
  • Violations of the check implicit-override (AUTOSAR.10.3.2A, M2023-CPP.13.3.1) are now only reported once per method instead of repeatedly at every redeclaration.
  • Removed false positives in uninstantiated templates for the following checks:
    • assignment-operator-return-value
    • cast-pointer-to-integer
    • cast-pointer-to-intptr
    • cast-function-pointer-to-integer
    • cast-pointer-void
    • cast-pointer-void-to-function-pointer
    • cast-pointer-void-to-integer
    • cast-pointer-void-to-intptr
    • cast-integer-to-function-pointer
    • cast-integer-to-pointer
    • cast-enum-to-pointer
    • function-pointer-cast
    • member-function-missing-const
    • member-function-missing-static
    • unary-assign-separation
    • unrelated-pointer-conversion
  • Removed false negatives for the checks implicitly-captured-this (M2023-CPP.8.1.1) and implicitly-captured-variable (M2023-CPP.8.1.2) when the violating lambda has a parameter with specified auto type.
  • The check clang_warning (A.6.2) can now be reported multiple times at the same code location if it reports different warnings generated by the clang frontend.

Improved tooltips

Tooltips in the Editor view have been improved and extended.

  • The tooltips now use syntax highlighting.
  • Large tooltips are now handled much better.
  • Tooltips for alarms now provide links to the Findings view and the user manual.

Server and server controller

  • The analysis server no longer considers global git configurations. This prevents unexpected failures in case of incompatible settings.
  • If a port number or data directory has been specified explicitly on the command line but is not available, the Astrée server now immediately reports the error and refuses to start, instead of starting with a random port and/or temporary directory.
  • Analyses can now be removed from the analysis queue using the server controller, via the new context menu action “Dequeue analysis” in either the Analyses or Analysis Queue view.

DAX import and export

  • DAX and AAF files can be imported into the client by drag & drop from a file browser (e.g. Windows Explorer).
  • The new DAX tag <aaf/> allows adding a reference analysis run to the imported project. It is equivalent to the command line option --aaf.
  • DAX import now ensures that AAL files from multiple uses of the <annotations/> tag are imported in the order in which they appear in the DAX file.
  • The following are now rejected already during DAX import:
    • Option and ABI values with incorrect type
    • Invalid comment classifications in original-source annotations
  • The import attribute is now available for all direct children of the <dax/> tag, except for the <base/> tag. It is now also available for the <dax/> tag itself to allow a full import of another DAX file.
  • DAX export now always asks for saving the analysis project to ensure that the exported DAX file contains the latest state of the project configuration.
  • Delta comments are now also applied when the file name specification in DAX differs from the effective file name used in the analysis. Such situations can occur when files are specified using symbolic links or network drive names.
  • The rule violations section of custom report configurations now allows reducing the reported violations to specific rule sets and/or MISRA categories (e.g. only mandatory rules of the MISRA-2023 rule set). The DAX format has been extended by appropriate tags that allow expressing such restrictions in the the rules configuration section.

Export of comments and directives

The export of comments and directives inserted by users has been improved.

  • The DAX export and import dialog now allows to selectively export each of the following sets of directives:
    • comment directives,
    • directives generated by TargetLink integration,
    • directives that are neither comments nor generated by the TargetLink integration.

    By default, the export now omits directives generated by the TargetLink integration.

  • New batch-mode command line options:
    • --export-comments <dax file>
      exports all comments of all comment modes as DAX and the corresponding AAL file
    • --export-aal-omit-generated
      allows omitting all directives generated by the TargetLink tool coupling when exporting annotations via the --export-aal command line option
  • The new menu entry “Project” → “Export” → “Comments to DAX…” exports the DAX and the corresponding AAL that contains all comments.

Other changes to client GUI, batch mode, and report files

  • Improved character encoding in all the integrated editors.
  • If a rule configuration is imported via Project → Import → Configuration and its name matches the name of an already existing configuration, the existing configuration is now overwritten as expected.
  • Ensured that AAL annotations are loaded into a new project even when a base revision (by analysis ID or reference AAF file) is specified during project import.
  • The GUI now preserves the specified order of external declarations instead of showing and applying type declarations first. The behavior is now consistent with batch mode.
  • Original-source annotations for C++ now also work in files that are referenced in the analysis configuration using symbolic links. Annotations for such files can be specified using either the symbolic link name or the actual file name.
  • After an analysis run, the Original Source Annotations view now always displays the actual insertion location, even if the code changed after creating the annotation.
  • Clicking Save in the Edit dialog of an original-source annotation for C++ now automatically regenerates the annotation if the code around the annotation has changed.
  • Modified the format of reached code statistics in the XML report, as introduced with the latest major release, to match the format used in DAX files. The new format is: 
     <reached_code_statistics_configuration>
     <paths>
         <path action="add|remove" kind="file|folder">path</path>
     </paths>
 </reached_code_statistics_configuration>
  • Analysis reports in mode=rulechecker (or in mode=astree with the option skip-analysis=yes) now list comment and suppress directives in the sections “Further directives” and “Semantic hypotheses”.
  • The new command line option --list-projects allows users to list all (visible) projects on the server in batch mode.
  • The new batch mode option --no-analysis skips the (re)computation of analysis results. It replaces the options --import-only, --export-only, --preprocess-only, and --report-only, which are still accepted but deprecated. We recommend removing the deprecated options from scripts and replacing them with --no-analysis.
  • The new batch mode option --no-reports skips report generation, except for reports that are explicitly specified on the command line using the options --report-file or --xml-report-file.
  • Pressing the “Start analysis” button of the GUI no longer starts the Astrée analysis if preprocessing failed with a fatal error.
  • Changed the SARIF report to use the "file" URI scheme instead of plain absolute file paths in the artifacts section.
  • Child tags of <separate-function/> that appear in a DAX file but are not supported in mode astree-cxx are now reported as errors when running the analysis in that mode.
  • When importing preprocessor configurations from another DAX file, the <preprocess><base> tag of the imported DAX is no longer ignored for OS configurations.
  • Alarm classifications in finding comments are now always printed in lowercase in the Output view and in text report files.
  • Rule configurations in the <rulechecks/> section of the XML report now list the added/removed source paths instead of the checked files. The new format is: 
     <configuration>
   <paths>
     <path action="add|remove" kind="file|folder">...</path>
   </paths>
 </configuration>

Fixes

  • Fixed report generation in batch mode for tool runs that do not involve importing a DAX file.
  • Fixed the import of preprocessor configurations from AAF files exported with build 12875094 (release 22.10i) or older.
  • Fixed an issue that could cause comments for original-source annotations for C++ to be missing from the analysis output view of the GUI after deleting, adding, or moving such annotations between two analysis runs.
  • Fixed an issue that could prevent the client from taking into account modifications of AAL comment directives if no other settings were changed.
  • Fixed “Import failed” errors which could occur when importing projects with the --id command line option (or the DAX tag <id/>) and a project with the specified ID already existed on the server.

Frontends and preprocessor

  • Updated the Clang/LLVM frontend to version 19.1.4.
  • The JSON compilation database importer now extracts more ABI settings from the compiler information for the following types: size_t, ptrdiff_t, wchar_t, wint_t, char16_t, char32_t, intptr_t, intmax_t, sig_atomic_t.
  • The JSON compilation database importer now also supports C++20.
  • The C frontend now rejects __ASTREE_partition_begin with float type argument by raising an invalid_directive alarm.
  • Improved location information for macro invocations. It now refers exactly to the macro name in the source code.
  • Fixed the application of “Patterns to ignore” immediately after escaped new lines (C11 ยง5.1.1.2, translation phase 2). The application of patterns at such locations could break RULECHECKER_comment(...) source directives at subsequent code locations, or shift findings reported at original-source locations by one line.
  • Improved the handling and reporting of fatal frontend errors (such as an #include file not found).
  • Parser filters can now be configured to apply to only original, only preprocessed, or all source code.

Stub libraries, ABIs, OS and compiler configurations

  • Updated alignment settings in the pre-defined ABI for “CompCert x86 32”.
  • Improved extraction of information about cores from multiple ARXML files.
  • When the option to use analysis stubs for standard libraries is enabled, the include paths of the built-in stubs are now also propagated to the OS-specific preprocessor configuration.
  • Replaced __ASTREE_attribute((...)) by /* ASTREE_attribute(...) */ in the stub libraries. This improves the efficiency of the frontend when parsing translation units that include stub library headers, in particular for C++, and removes spurious alarms about rule violations related to the check multiple-include (M.19.15, M2012.D.4.10, M2023-C.D.4.10).
  • The ARXML converter has been extended to extract information about cores from the ECUC Hardware Configuration.
  • Errors that occur during the processing of ARXML files are now reported as “ERROR autosar: …”.

Qualification Support Kits

  • Improved driver program with a re-designed GUI.

New test cases in the Astrée QSK

  • qk_check_assignment_conditional
  • qk_check_bad_function
  • qk_check_bad_function_use
  • qk_check_clang_warning
  • qk_check_fixpoint_iteration
  • qk_check_function_name_usage
  • qk_check_function_return_unused
  • qk_check_ineffective_file_list_entry
  • qk_check_scaled_pointer_arithmetic
  • qk_check_signal_handler_unsafe_call
  • qk_check_sizeof_array_parameter
  • qk_check_spectre_vulnerability
  • qk_check_switch_clause_break
  • qk_check_switch_default
  • qk_check_unused_directive
  • qk_check_zero_size_alloc
  • qk_commandline_no_analysis
  • qk_commandline_no_reports
  • qk_directive_add_widening_thresholds
  • qk_directive_partition_merge_closest
  • qk_directive_partition_bases
  • qk_filter_expressions_alternatives
  • qk_filter_expressions_begin_and_end_of_line
  • qk_filter_expressions_char_set
  • qk_filter_expressions_dot_repetition
  • qk_filter_expressions_naming
  • qk_filter_expressions_special_characters
  • qk_filter_expressions_word_boundaries
  • qk_filter_ignore
  • qk_filter_more_functions
  • qk_filter_one_function
  • qk_filter_one_function_with_stub
  • qk_filter_replacement
  • qk_option_dyn_unroll_cost
  • qk_option_first_logic_packs
  • qk_option_globals_are_initialized
  • qk_rule_a_3_4
  • qk_rule_a_5_1
  • qk_rule_a_5_3
  • qk_rule_a_6_2
  • qk_rule_b_1_2
  • qk_rule_b_1_8
  • qk_rule_cwe_242
  • qk_rule_cwe_252
  • qk_rule_cwe_398
  • qk_rule_cwe_467
  • qk_rule_cwe_468
  • qk_rule_cwe_475
  • qk_rule_cwe_478
  • qk_rule_cwe_479
  • qk_rule_cwe_480
  • qk_rule_cwe_481
  • qk_rule_cwe_482
  • qk_rule_cwe_484
  • qk_rule_cwe_561
  • qk_rule_cwe_570
  • qk_rule_cwe_571
  • qk_rule_cwe_676
  • qk_rule_cwe_1420
  • qk_rule_cwe_1422
  • qk_rule_cwe_1423
  • qk_rule_cert_con_35
  • qk_rule_cert_int_35
  • qk_rule_cert_pos_49
  • qk_rule_cert_pos_51
  • qk_rule_cert_pos_52
  • qk_rule_cert_pos_54
  • qk_rule_iso17961_argcomp
  • qk_rule_m2012_22_1
  • qk_rule_m2025_c_d_4_7
  • qk_rule_m2025_c_d_4_13
  • qk_rule_m2025_c_d_5_1
  • qk_rule_m2025_c_d_5_2
  • qk_rule_m2025_c_1_3
  • qk_rule_m2025_c_2_1
  • qk_rule_m2025_c_9_1
  • qk_rule_m2025_c_9_7
  • qk_rule_m2025_c_12_2
  • qk_rule_m2025_c_14_3
  • qk_rule_m2025_c_18_1
  • qk_rule_m2025_c_18_6
  • qk_rule_m2025_c_19_1
  • qk_rule_m2025_c_22_1
  • qk_rule_m2025_c_22_14
  • qk_rule_m2025_c_22_20

The obsolete test cases qk_abi_alignof_char_array, qk_commandline_export_only, and qk_commandline_preprocess_only have been removed from the Astrée QSK.

Astrée QSK test cases extended to C++

  • qk_check_config_function_unknown
  • qk_check_ignored_partitioning
  • qk_check_ignored_states_track
  • qk_check_imprecise_memcpy
  • qk_check_legacy_alarm_annotation
  • qk_check_unused_suppress_directives
  • qk_directive_attributes_source
  • qk_directive_check
  • qk_directive_check_separate_targets
  • qk_directive_comment
  • qk_directive_comment_source
  • qk_directive_global_assert
  • qk_directive_ignore
  • qk_directive_import
  • qk_directive_initialize
  • qk_directive_known_fact
  • qk_directive_known_range
  • qk_directive_log_vars
  • qk_directive_octagon_pack
  • qk_directive_partition_merge
  • qk_directive_state_merge
  • qk_directive_state_track
  • qk_directive_partition_begin
  • qk_directive_partition_calls
  • qk_directive_partition_control
  • qk_directive_partition_expr
  • qk_directive_partition_ranges
  • qk_directive_partition_merge_last
  • qk_option_partition
  • qk_directive_print
  • qk_directive_smash_variable
  • qk_rule_a_5_4
  • qk_rule_b_1_5
  • qk_rule_b_1_6
  • qk_rule_b_1_7

New test cases in the RuleChecker QSK

  • qk_check_bad_enumerator
  • qk_check_cnd_mtx_relation
  • qk_check_constant_call_argument
  • qk_check_exit_handler_bad_function
  • qk_check_extern_declaration_in_non_header
  • qk_check_generic_selection_unsafe
  • qk_check_implicit_null_comparison
  • qk_check_imprecise_int_to_float_cast
  • qk_check_imprecise_int_to_float_conversion
  • qk_check_include_guard_identifier_unique
  • qk_check_ineffective_file_list_entry
  • qk_check_invalid_thread_operation
  • qk_check_mtx_double_unlock
  • qk_check_mtx_double_lock
  • qk_check_mtx_init_type
  • qk_check_mtx_timedlock_type
  • qk_check_mtx_without_unlock
  • qk_check_putenv_arg_local
  • qk_check_stdlib_array_size
  • qk_check_stdlib_string_termination
  • qk_check_string_initializer_null
  • qk_check_tentative_definition_in_header
  • qk_check_thrd_create_position
  • qk_check_tss_creation
  • qk_check_uninitialized_atomic_access
  • qk_check_uninitialized_cnd_t
  • qk_check_uninitialized_mtx_t
  • qk_check_value_specification_ignored
  • qk_commandline_no_analysis
  • qk_commandline_export_aal
  • qk_commandline_no_reports
  • qk_filter_attribute_enabled
  • qk_filter_attribute_replacement
  • qk_filter_attribute_source_kind
  • qk_option_dump_hypotheses
  • qk_rule_autosar_0_4_2a
  • qk_rule_b_1_8
  • qk_rule_cert_arr_38
  • qk_rule_cert_con_33
  • qk_rule_cert_cpp_str_31c
  • qk_rule_cert_env_31
  • qk_rule_cert_env_32
  • qk_rule_cert_fio_34
  • qk_rule_cert_flp_36
  • qk_rule_cert_msc_32
  • qk_rule_cert_msc_33
  • qk_rule_cert_msc_41
  • qk_rule_cert_pos_34
  • qk_rule_cert_pos_47
  • qk_rule_cert_pos_53
  • qk_rule_cert_pos_54
  • qk_rule_cert_str_31
  • qk_rule_cert_str_32
  • qk_rule_cert_int_30
  • qk_rule_cert_int_35
  • qk_rule_cwe_242
  • qk_rule_cwe_252
  • qk_rule_cwe_398
  • qk_rule_cwe_467
  • qk_rule_cwe_468
  • qk_rule_cwe_478
  • qk_rule_cwe_479
  • qk_rule_cwe_480
  • qk_rule_cwe_481
  • qk_rule_cwe_482
  • qk_rule_cwe_484
  • qk_rule_cwe_561
  • qk_rule_cwe_570
  • qk_rule_cwe_571
  • qk_rule_cwe_676
  • qk_rule_cwe_1007
  • qk_rule_m2012a3_23_7
  • qk_rule_m2023_c_9_7
  • qk_rule_m2023_c_21_26
  • qk_rule_m2023_c_22_11
  • qk_rule_m2023_c_22_14
  • qk_rule_m2023_c_22_15
  • qk_rule_m2023_c_22_16
  • qk_rule_m2023_c_22_17
  • qk_rule_m2023_c_22_18
  • qk_rule_m2023_c_22_20
  • qk_rule_m2023_c_d_5_3
  • qk_rule_m2023_c_22_19
  • qk_rule_m2023_c_23_7
  • qk_rule_m2025_c_d_1_1
  • qk_rule_m2025_c_d_1_2
  • qk_rule_m2025_c_d_2_1
  • qk_rule_m2025_c_d_3_1
  • qk_rule_m2025_c_d_4_1
  • qk_rule_m2025_c_d_4_2
  • qk_rule_m2025_c_d_4_3
  • qk_rule_m2025_c_d_4_5
  • qk_rule_m2025_c_d_4_6
  • qk_rule_m2025_c_d_4_7
  • qk_rule_m2025_c_d_4_8
  • qk_rule_m2025_c_d_4_9
  • qk_rule_m2025_c_d_4_10
  • qk_rule_m2025_c_d_4_11
  • qk_rule_m2025_c_d_4_12
  • qk_rule_m2025_c_d_4_13
  • qk_rule_m2025_c_d_4_14
  • qk_rule_m2025_c_d_5_3
  • qk_rule_m2025_c_1_1
  • qk_rule_m2025_c_1_3
  • qk_rule_m2025_c_1_4
  • qk_rule_m2025_c_1_5
  • qk_rule_m2025_c_2_1
  • qk_rule_m2025_c_2_2
  • qk_rule_m2025_c_2_3
  • qk_rule_m2025_c_2_4
  • qk_rule_m2025_c_2_5
  • qk_rule_m2025_c_2_6
  • qk_rule_m2025_c_2_7
  • qk_rule_m2025_c_2_8
  • qk_rule_m2025_c_3_1
  • qk_rule_m2025_c_3_2
  • qk_rule_m2025_c_4_1
  • qk_rule_m2025_c_4_2
  • qk_rule_m2025_c_5_1
  • qk_rule_m2025_c_5_2
  • qk_rule_m2025_c_5_3
  • qk_rule_m2025_c_5_4
  • qk_rule_m2025_c_5_5
  • qk_rule_m2025_c_5_6
  • qk_rule_m2025_c_5_7
  • qk_rule_m2025_c_5_8
  • qk_rule_m2025_c_5_9
  • qk_rule_m2025_c_5_10
  • qk_rule_m2025_c_6_1
  • qk_rule_m2025_c_6_2
  • qk_rule_m2025_c_6_3
  • qk_rule_m2025_c_7_1
  • qk_rule_m2025_c_7_2
  • qk_rule_m2025_c_7_3
  • qk_rule_m2025_c_7_4
  • qk_rule_m2025_c_7_5
  • qk_rule_m2025_c_7_6
  • qk_rule_m2025_c_8_1
  • qk_rule_m2025_c_8_2
  • qk_rule_m2025_c_8_3
  • qk_rule_m2025_c_8_4
  • qk_rule_m2025_c_8_5
  • qk_rule_m2025_c_8_6
  • qk_rule_m2025_c_8_7
  • qk_rule_m2025_c_8_8
  • qk_rule_m2025_c_8_9
  • qk_rule_m2025_c_8_10
  • qk_rule_m2025_c_8_11
  • qk_rule_m2025_c_8_12
  • qk_rule_m2025_c_8_13
  • qk_rule_m2025_c_8_14
  • qk_rule_m2025_c_8_15
  • qk_rule_m2025_c_8_16
  • qk_rule_m2025_c_8_17
  • qk_rule_m2025_c_8_18
  • qk_rule_m2025_c_8_19
  • qk_rule_m2025_c_9_1
  • qk_rule_m2025_c_9_2
  • qk_rule_m2025_c_9_3
  • qk_rule_m2025_c_9_4
  • qk_rule_m2025_c_9_5
  • qk_rule_m2025_c_9_6
  • qk_rule_m2025_c_9_7
  • qk_rule_m2025_c_10_1
  • qk_rule_m2025_c_10_2
  • qk_rule_m2025_c_10_3
  • qk_rule_m2025_c_10_4
  • qk_rule_m2025_c_10_5
  • qk_rule_m2025_c_10_6
  • qk_rule_m2025_c_10_7
  • qk_rule_m2025_c_10_8
  • qk_rule_m2025_c_11_1
  • qk_rule_m2025_c_11_2
  • qk_rule_m2025_c_11_3
  • qk_rule_m2025_c_11_4
  • qk_rule_m2025_c_11_5
  • qk_rule_m2025_c_11_6
  • qk_rule_m2025_c_11_8
  • qk_rule_m2025_c_11_9
  • qk_rule_m2025_c_11_10
  • qk_rule_m2025_c_11_11
  • qk_rule_m2025_c_12_1
  • qk_rule_m2025_c_12_2
  • qk_rule_m2025_c_12_3
  • qk_rule_m2025_c_12_4
  • qk_rule_m2025_c_12_5
  • qk_rule_m2025_c_12_6
  • qk_rule_m2025_c_13_1
  • qk_rule_m2025_c_13_2
  • qk_rule_m2025_c_13_3
  • qk_rule_m2025_c_13_4
  • qk_rule_m2025_c_13_5
  • qk_rule_m2025_c_13_6
  • qk_rule_m2025_c_14_1
  • qk_rule_m2025_c_14_2
  • qk_rule_m2025_c_14_3
  • qk_rule_m2025_c_14_4
  • qk_rule_m2025_c_15_1
  • qk_rule_m2025_c_15_2
  • qk_rule_m2025_c_15_3
  • qk_rule_m2025_c_15_4
  • qk_rule_m2025_c_15_5
  • qk_rule_m2025_c_15_6
  • qk_rule_m2025_c_15_7
  • qk_rule_m2025_c_16_1
  • qk_rule_m2025_c_16_2
  • qk_rule_m2025_c_16_3
  • qk_rule_m2025_c_16_4
  • qk_rule_m2025_c_16_5
  • qk_rule_m2025_c_16_6
  • qk_rule_m2025_c_16_7
  • qk_rule_m2025_c_17_1
  • qk_rule_m2025_c_17_2
  • qk_rule_m2025_c_17_3
  • qk_rule_m2025_c_17_4
  • qk_rule_m2025_c_17_5
  • qk_rule_m2025_c_17_7
  • qk_rule_m2025_c_17_8
  • qk_rule_m2025_c_17_9
  • qk_rule_m2025_c_17_10
  • qk_rule_m2025_c_17_11
  • qk_rule_m2025_c_17_12
  • qk_rule_m2025_c_17_13
  • qk_rule_m2025_c_18_1
  • qk_rule_m2025_c_18_2
  • qk_rule_m2025_c_18_3
  • qk_rule_m2025_c_18_4
  • qk_rule_m2025_c_18_5
  • qk_rule_m2025_c_18_6
  • qk_rule_m2025_c_18_7
  • qk_rule_m2025_c_18_8
  • qk_rule_m2025_c_18_9
  • qk_rule_m2025_c_18_10
  • qk_rule_m2025_c_19_1
  • qk_rule_m2025_c_19_2
  • qk_rule_m2025_c_20_1
  • qk_rule_m2025_c_20_2
  • qk_rule_m2025_c_20_3
  • qk_rule_m2025_c_20_4
  • qk_rule_m2025_c_20_5
  • qk_rule_m2025_c_20_6
  • qk_rule_m2025_c_20_7
  • qk_rule_m2025_c_20_8
  • qk_rule_m2025_c_20_9
  • qk_rule_m2025_c_20_10
  • qk_rule_m2025_c_20_11
  • qk_rule_m2025_c_20_12
  • qk_rule_m2025_c_20_13
  • qk_rule_m2025_c_20_14
  • qk_rule_m2025_c_20_15
  • qk_rule_m2025_c_21_3
  • qk_rule_m2025_c_21_4
  • qk_rule_m2025_c_21_5
  • qk_rule_m2025_c_21_6
  • qk_rule_m2025_c_21_7
  • qk_rule_m2025_c_21_8
  • qk_rule_m2025_c_21_9
  • qk_rule_m2025_c_21_10
  • qk_rule_m2025_c_21_11
  • qk_rule_m2025_c_21_12
  • qk_rule_m2025_c_21_13
  • qk_rule_m2025_c_21_14
  • qk_rule_m2025_c_21_15
  • qk_rule_m2025_c_21_16
  • qk_rule_m2025_c_21_17
  • qk_rule_m2025_c_21_18
  • qk_rule_m2025_c_21_19
  • qk_rule_m2025_c_21_20
  • qk_rule_m2025_c_21_21
  • qk_rule_m2025_c_21_22
  • qk_rule_m2025_c_21_23
  • qk_rule_m2025_c_21_24
  • qk_rule_m2025_c_21_25
  • qk_rule_m2025_c_21_26
  • qk_rule_m2025_c_22_1
  • qk_rule_m2025_c_22_2
  • qk_rule_m2025_c_22_3
  • qk_rule_m2025_c_22_4
  • qk_rule_m2025_c_22_5
  • qk_rule_m2025_c_22_6
  • qk_rule_m2025_c_22_7
  • qk_rule_m2025_c_22_8
  • qk_rule_m2025_c_22_9
  • qk_rule_m2025_c_22_10
  • qk_rule_m2025_c_22_11
  • qk_rule_m2025_c_22_12
  • qk_rule_m2025_c_22_13
  • qk_rule_m2025_c_22_14
  • qk_rule_m2025_c_22_15
  • qk_rule_m2025_c_22_16
  • qk_rule_m2025_c_22_17
  • qk_rule_m2025_c_22_18
  • qk_rule_m2025_c_22_19
  • qk_rule_m2025_c_22_20
  • qk_rule_m2025_c_23_1
  • qk_rule_m2025_c_23_2
  • qk_rule_m2025_c_23_3
  • qk_rule_m2025_c_23_4
  • qk_rule_m2025_c_23_5
  • qk_rule_m2025_c_23_6
  • qk_rule_m2025_c_23_7
  • qk_rule_m2025_c_23_8

The obsolete test cases qk_abi_alignof_char_array, qk_commandline_preprocess_only, qk_filter_ignore, qk_filter_more_functions, qk_filter_one_function_with_stub, and qk_filter_replacement have been removed from the RuleChecker QSK.

RuleChecker QSK test case extended to C

  • qk_check_source_character_set

RuleChecker QSK test cases extended to C++

  • qk_check_commented_file
  • qk_check_max_commented_lines
  • qk_check_max_suppressed_lines
  • qk_check_suppressed_file
  • qk_check_unused_suppress_directives
  • qk_rule_a_5_1
  • qk_rule_a_5_2
  • qk_rule_a_5_6
  • qk_rule_b_1_3
  • qk_rule_b_1_4

Known issues

ID Short summary
2504-00831In astree-cxx mode, global initialization assertion failures may not be reported under specific circumstances
2504-10873Under a specific set of circumstances, global initialization assertion failures may not be reported
2504-24492When the symbolic domain is enabled, the analysis may not account for all effects of rounding mode changes at runtime
2504-34536With rounding_mode=to_nearest, the symbolic domain may compute wrong values
2504-48729Calling __astree_set_process_priority with precise-priorities=yes changes the priority of the wrong process

All five issues will be resolved in the upcoming stable release 25.10. In the mean time, please write to support@absint.com to receive further details, code examples, tell-tale symptoms, and known workarounds.