Astrée and RuleChecker Release 25.04 An HTML version of these release notes is available at absint.com/releasenotes/astree/25.04 Support for C++23 Added support for C++23. 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. The documentation has been updated and 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 to allow integration into VS 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 release 23.10. Linux support Support for RHEL 7 is now deprecated. In the near future, the Linux version will require at least RHEL 9 (or compatible). 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 for 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. Enhancements, clarifications, refinements, and fixes for 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). Enhancements, clarifications, refinements, and fixes for 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 MISRA-2023). 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 ▲ 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 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_directive_print qk_directive_smash_variable qk_option_partition 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_19 qk_rule_m2023_c_22_20 qk_rule_m2023_c_23_7 qk_rule_m2023_c_d_5_3 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 ------------------------------------------------------------------------------ Last updated on 24 April 2025 by alex@absint.com. Copyright 2025 AbsInt. ------------------------------------------------------------------------------ An HTML version of these release notes is available at absint.com/releasenotes/astree/25.04