Astrée and RuleChecker release 23.10

Diff-based comments

Additional tooltips for value ranges

Improved file trees

MISRA C:2023 compliance checks

Enhanced call graphs

AbsInt License Manager (ALM)

All network connections between the ALM server and its clients are now TLS-encrypted, and the ALM web interface is now served via HTTPS in addition to HTTP.

Upgrading your client to this release requires upgrading your ALM as well. Old client versions will continue to work with the new ALM using the non-encrypted legacy protocol, unless you block the corresponding port in your firewall. The default port for the legacy protocol is 42424, while for the new TLS connection it’s 42426.

A new environment variable AI_LICENSE_TLS is used to configure the license, while old versions use AI_LICENSE. This enables you to set up old and new versions to run in parallel, for example:

AI_LICENSE = alm-server@42424
AI_LICENSE_TLS = alm-server@42426

The default port for the ALM web interface is 42425 for HTTP and 42427 for HTTPS.

alauncher

  • The tool launcher now supports scanning for installed products in arbitrary directories specified via the option --dir <path>
  • The launcher will now auto-discover all a³ tools located in sibling a3* directories. This enables you to unpack the product ZIP files in a directory and use the launcher of any of them to access all of them. For example, if you have a directory with a3_c_123, a3_c_456, and a3_ppc_789, you can now use the launcher in a3_c_456/bin to access all three tools.

DAX changes

  • Removed support for the deprecated DAX preprocessor tags <strip-path/> and <replacements/>. They are no longer needed and can be removed from DAX files.
  • Removed the deprecated DAX option use-relative-paths.

Improved precision

Analysis precision has been improved for:

  • computations that involve bit masks
  • dynamic memory allocations from within C++ virtual methods
  • modulo operations in the congruence intervals domain
  • casts from float to integer in comparisons
  • structs assigned to self
  • the octagon domain when adding positive values, and on expressions that involve casts

Improved C++ mode

  • Improved tooltips.
  • Integer types in alarms messages and tooltips are now displayed as
    (un)signed x-bit integer
    where x is the number of bits used to represent the type.
  • Regular expressions provided as arguments to the options unroll-loops-in-functions and separate-function now match entire function signatures instead of a prefix of function signatures.
  • Statements that are inserted via the original source annotation mechanism are now taken into account when computing the analysis coverage information.
  • Fixed integer signedness assumed by the C++ frontend for fields of union and struct types in the presence of inheritance. This generally improves analysis precision and corrects alarms in Astrée directives that specify bounds for the affected fields (__ASTREE_modify, __ASTREE_volatile_input, __ASTREE_known_range, __ASTREE_global_assert).

Diff-based comments

Introducing a new diff-based comment mechanism which, in case of code changes, identifies commented code locations by comparing the currently analyzed code with a reference from a previous analysis run. The new comment mechanism is available in all analysis modes (astree, astree-cxx, rulechecker).

  • Existing comments that use the comment modes AAL or pattern can be converted to the new comment mode by using a button in the toolbar of the diff comments view or the command line option --convert-to-diff-comments.
  • The command line option --export-diff-comments <dax-file> allows exporting diff-based comments into a DAX file.

Other improvements

  • The tooltips for displaying value ranges have been extended to all sub-expressions. For example, in an expression like x + y Astrée now also shows a tooltip for the + operator, reporting the result of the addition.
  • Improved reporting of ABI settings that are incompatible with the Clang frontend.
  • The JSON compilation database importer now resolves relative paths relative to the location of the provided JSON file instead of relative to the current working directory.
  • The state machine domain is now enabled by default.
  • The symbolic domain now handles:
    • relations that involve shifts, e.g.
      x = in >> 15;
      out = (in << 1) - (x << 16);
      // 'out' is now known to be positive for positive 'in'
    • complex expression that are bounded by comparisons, e.g.
      ((a - b - c) / d) < 8;
  • Improved the octagon packing heuristics to create more useful octagon packs on some code patterns.
  • Astrée now accepts union expressions in struct and array initializers.
  • The calculation of malloc contexts has new limits to ensure that it does not take too long.
  • Removed false alarms when using value-initialized iterators with the preprocessor option "Use abstract stubs for the C++ standard template library" enabled.
  • Improved the error reporting for partitioning directives. The analyzer now avoids reporting alarms that occur in the evaluation of the directive but reports more consistently when such directives are ignored completely.
  • Dynamically allocated memory blocks are now displayed in the global data flow view and marked as possibly shared or affected by data races when being accessed from multiple processes.
  • Improved performance when analyzing assignments from large smashed to non-smashed variables.
  • The automatic loop unroll heuristics now ignore Astrée directives when counting the number of statements in a loop. Introducing directives into loops therefore no longer influences loop unrolling decisions with respect to the option auto-unroll-size.
  • Accesses from multiple processes to the same global variable are no longer reported as shared if the accesses do not happen in the same phase.
  • Replaced the ABI option unaligned_dereference by two new Astrée semantics options:
    • warn-on-misaligned-dereference (default: yes) warns about misaligned dereferences
    • cut-misaligned-dereference (default: yes) cuts traces with misaligned dereferences from the analysis
    • The defaults for the new options correspond to the default of the former option unaligned_dereference=error.
  • The directive __ASTREE_global_assert can now express that a pointer may only point to certain offsets in a variable. For example, if the pointer p may point to the fields a or b of variable v, that can be expressed as
    __ASTREE_global_assert((p; {&v.a, &v.b}));

Fixes

  • Fixed the directive __ASTREE_check_separate_targets for the case that more than two arguments are given.
  • Fixed an issue that could cause crashes when using __ASTREE_octagon_pack with variables of pointer type and the Boolean domain enabled.
  • Fixed an issue that could cause the analyzer to crash when the option generate-undeclared-absolute-addresses was enabled.

Toolbox for TargetLink

  • Fixed an issue that caused the toolbox to fail when supplying an additional DAX file via the toolbox preferences.
  • Improved file handling to prevent configuration errors when the same file name is found multiple times with different capitalization.
  • The generated preprocessor configuration now sets the combine="merge" attribute. This allows specifying additional includes and defines for the generated preprocessor configuration via an additional DAX file, as configured in the toolbox preferences.
  • Fixed capitalization of file names in the preprocessor configuration of AUTOSAR projects and in the generated coverage_ignore attributes.

Eclipse plugin

  • Support for automatic includes.
  • Proper handling of linked files.
  • Improved compatibility with Astrée 21.04i and higher when activating and deactivating checks.

Rule sets and checks for C

  • Added support for MISRA C:2023.
  • Added support for rule CERT.MSC.9.

Rule sets and checks specific to Astrée

  • Rule checks reported during run-time analysis (check phase analysis) are now reported with all analysis contexts instead of only one.
  • The check invalid_directive now also warns about __ASTREE_partition_calls directives that have no function call in scope.

Enhancements, clarifications, refinements, and fixes

Both C and C++

  • Fixed default argument of rule A.5.2 by listing endasm instead of end_asm.
  • Refined the check pragma-usage (A.5.2, AUTOSAR.16.0.1A, AUTOSAR.16.7.1A, M.3.4, M2008.16.6.1, M202x-DRAFT.000213) by restricting it to code sections included by the preprocessor.
  • Improved code location reported for rule violations at preprocessor directives such as #include.
  • Improved the alarm message for the check max-number-of-recursive-paths. It now reports which functions are involved in the recursion.
  • The check unary-assign-separation (AUTOSAR.5.2.10M, M.12.13, M2008.5.2.10) no longer warns about subscript operator uses in operands of increment/decrement operations. For C++, the check treats overloaded operator calls like built-in operators, in accordance with the latest interpretation of the associated rules, to remove undesired alarms.
  • For unused source comment/suppress directives, the check unused-suppress-directive now additionally reports the end location of the affected code area.
  • Reduced memory consumption when activating rule T.12.1.
  • RPATH now stops counting upon encountering 100 000 recursive paths, to keep the analysis runtime under control. The metrics table then displays the value as “>100000”.
  • The diagnostic check unused-suppressed-directive (B.1.2) can now be configured to exclude source directives that are never reached by the preprocessor.
  • Paths without a valid continuation (e.g. after accessing an invalid pointer) are now discarded in the analysis phase clangstaticanalyzer. This removes irrelevant alarms for all checks that run in that phase.
  • Merged the check non-standard-escape-sequence-pp into the check non-standard-escape-sequence (A.2.11, M.1.1, M2012.1.2, X.E.5.2.5.5).

C code

  • Removed false positives for:
    • cast-integer-implicit (M.10.1) and cast-float-implicit (M.10.2, X.F.27) with initializers for bit-fields and at function return
    • static-object-zero-initialization (AUTOSAR.3.3.2A). It no longer warns about out-of-class definitions of static data members without initializer if their in-class declaration features an initializer.
    • global-object-scope (CERT.DCL.15, CERT.DCL.19, M.8.10, M2012.8.7, X.B.5.5, X.F.31). Tentative definitions (without initializer) are now considered a use of the variable as well.
    • implicit-designation (M2012.9.2). In addition to the excluded values {0} and {0U}, arbitrary integer constants of zero value are now excluded as well ({0UL}, {0x0}, etc.).
  • Removed false negatives for the check global-object-scope (CERT.DCL.15, CERT.DCL.19, M.8.10, M2012.8.7, X.B.5.5, X.F.31), which did not report tentative definitions (without initializer) without further use.
  • Fixed calculation of the CDFUN metric for functions whose names result from function-like macro expansions. This removes false positives for the rule T.14.1 (min-comment-density-his).
  • The check sline-comment (M2012.3.1, M2023-C.3.1, CERT.MSC.4) is no longer reported in code that is excluded by the preprocessor.
  • The checks object-pointer-diff-cast and object-pointer-diff-cast-implicit (M2023-C.11.3, M2012.11.3, M.11.4) now report when a pointer to an atomic qualified object type is converted to a pointer of type char, signed char or unsigned char.
  • Added new checks pointer-qualifier-cast-atomic and pointer-qualifier-cast-atomic-implicit (M2023-C.11.8).
  • It is now possible to specify exceptions to the check sline-comment by providing a regular expression option to its associated rules (CERT.MSC.4, M2012.3.1, M2023-C.3.1).

C++ code

  • The check bad-function no longer fails on the use of non-function declarations. This removes false positives for AUTOSAR.15.5.2A, AUTOSAR.18.9.1A, AUTOSAR.26.5.1A, M202x-DRAFT.000202, M202x-DRAFT.000355, M202x-DRAFT.000226, M202x-DRAFT.000223, M202x-DRAFT.000329, CERT-CPP.CON.37C, CERT-CPP.MSC.30C, and CERT-CPP.MSC.50.
  • The check assignment-operator-return-type (AUTOSAR.13.2.1A) has been split into the checks assignment-operator-return-type (which allows void as return type) and assignment-operator-return-type-void.
  • The template instantiation stacks that are reported with rule violations now include variable templates.
  • Improved code location reported for violations of the check mmline-comment (AUTOSAR.2.7.1M, M2008.2.7.1, M202x-DRAFT.000025).
  • Removed false negatives for the check pragma-usage (A.5.2, AUTOSAR.16.0.1A, AUTOSAR.16.7.1A, M202x-DRAFT.000213, M2008.16.6.1) which did not report the use of _Pragma("...").
  • Removed false positives for:
    • clean-global-namespace (M2008.7.3.1, AUTOSAR.7.3.1M) regarding template parameters
    • original-source-annotation-insertion-failed (A.CPP.5.1) when the annotation insertion targets a location that might be excluded by the preprocessor in only some translation units, e.g. due to an include guard
    • mixed-virtual-base (AUTOSAR.10.1.3M, M2008.10.1.3, M202x-DRAFT.000165), which sometimes failed to consider all inheritance edges
  • Removed false negatives for the check potentially-throwing-static-initialization (AUTOSAR.15.2.1A, CERT-CPP.ERR.58). It now also reports violations within variable template (partial) specializations.
  • Removed false negatives for:
    • bitop-type (M2008.5.0.21, AUTOSAR.5.0.21M) regarding the left-hand side of bitwise shift assignment operators <<= or >>=
    • shift-width-constant (M2008.5.8.1, AUTOSAR.5.8.1M) regarding the right-hand side of bitwise shift assignment operators <<= or >>=
  • Removed false positives and false negatives for:
    • underlying-cvalue-conversion (AUTOSAR.5.0.3M, M2008.5.0.3) with respect to reference types and elaborated types
    • underlying-narrowing-conversion (AUTOSAR.5.0.6M, M2008.5.0.6) with respect to elaborated types
    • underlying-signedness-conversion (AUTOSAR.5.0.4M, M2008.5.0.4) with respect to elaborated types
    • non-diamond-virtual-base (AUTOSAR.10.1.2M, M2008.10.1.2), which sometimes failed to consider all inheritance edges
  • Removed false positives and false negatives for:
    • using-directive-header (AUTOSAR.7.3.4M, AUTOSAR.7.3.6M, M2008.7.3.4, M2008.7.3.6)
    • using-directive-non-header (AUTOSAR.7.3.4M, M2008.7.3.4)
    • using-declaration-header (AUTOSAR.7.3.6M, M2008.7.3.6)
    • inaccessible-external-function (AUTOSAR.3.3.1A, M2008.3.3.1)
    • inaccessible-external-object (AUTOSAR.3.3.1A, M2008.3.3.1)
    • unused-internal-function (AUTOSAR.0.1.10M, AUTOSAR.0.1.3A, M2008.0.1.10)
    • unused-internal-variable (AUTOSAR.0.1.3M, M2008.0.1.3)
    • unnamed-namespace-header (AUTOSAR.7.3.3M, CERT-CPP.DCL.59, M2008.7.3.3)
    These checks now consider the locations of macro expansions instead of the locations of their definition in order to decide whether code comes from a header file.
  • The option allow-signed-constant-with-unsigned now only affects non-negative signed constants. This removes false negatives of the checks underlying-signedness-conversion (M2008.5.0.4, AUTOSAR.5.0.4M) and bitop-type (M2008.5.0.21, AUTOSAR.5.0.21M) when the option is enabled.
  • Removed false negatives of the check potentially-throwing-static-initialization (AUTOSAR.15.2.1A, CERT-CPP.ERR.58). In addition to checking for the existence of a noexcept exception specification, it now also checks the condition and thus also catches noexcept(false).
  • The C++ version of the check parameter-name-match (M2008.8.4.2, AUTOSAR.8.4.2M) no longer warns about mismatched parameter names between an explicit function template specialization declaration and the template declaration that is specialized.
  • The check function-return-unused (M2008.0.1.7, AUTOSAR.0.1.2A) now also warns when the overloaded call operator() is used with function call syntax, i.e. with ().
  • The check cast-integer-to-pointer (M2008.5.2.8, AUTOSAR.5.2.8M) no longer warns about conversion from integer type to function pointer. This aspect of the associated rules is now covered by the new check cast-integer-to-function-pointer.
  • The check inconsistent-default-argument (M2008.8.3.1, AUTOSAR.8.3.1M) now treats non-constant expression as having different values. The associated rules are thereby decidable and now fully covered.
  • Removed false negatives for the check ambiguous-identifiers (AUTOSAR.2.10.1M, M2008.2.10.1) for identifiers introduced by friend declarations.

Server and server controller

  • All network connections between analysis servers and clients are now TLS-encrypted.
  • The Astrée server now supports external authentication via authorization servers compatible with OAuth 2.0 or OpenID Connect (OIDC).
  • The list of user names is now displayed in alphabetical order in the server controller.
  • It is now possible to specify in the server controller that newly created analyses be private by default.
  • It is now possible to limit the number of concurrent analyses for an analysis server in that server’s configuration, using any of the following:
    • the server command line option --concurrent-analyses-limit <int>
    • the server controller command line option --set-concurrent-analyses-limit <int>
    • the server controller GUI option “Maximum number of concurrent analyses”

Client GUI, batch mode, and report files

  • The client now warns about the automatic conversion when importing AAF files from older versions. For AAF files generated from release 23.10i onwards, it also points out which Astrée version to use in order to prevent the conversion.
  • Fixed handling of modification state during project loading, to prevent unintentional modification of analysis data when triggering a project save operation while loading.
  • The batch mode option --report-only can now also be used for generating reports from AAF files.
  • Original source annotations for C++ code can now be disabled/enabled from the "Original Source Annotations" view.
  • The call graph view now shows more detailed alarm counters and the analysis time spent per function.
  • The context menu of graph nodes now offers actions for folding subtrees and displaying all callers and callees of a function.
  • The custom report file configuration dialog now supports file selection by folder structure, just like the Filter view.
  • Pressing the “Import to project” button of the compilation database importer now closes the corresponding dialog after importing the generated preprocessor configuration.
  • Fixed an issue that prevented the proper import of AAF files on Linux when the files had been exported on Windows using release 23.04 or 23.04i.
  • The New Project Wizard allows to configure the files to be used for the analysis by extracting the information from a compilation database.
  • Improved the tree view for preprocessed and original source files in the left sidebar. Chains of directories are now collapsed into a single line when appropriate.
  • Improved the tree view for files in Results → Filter. The file paths are now collapsed if possible, to offer a more compact view.
  • Added a new predefined report @data-races that lists the affected variables together with the corresponding alarms about the data races.
  • Findings that concern original source annotations for C++ can now be commented.
  • Fixed the upload of ARXML and OIL files to the analysis server, which was not possible in version 23.04i.
  • Fixed an issue that prevented exclusion of a file from rule checking if the file appeared in a line directive with a relative path that contained a symbolic link.

Frontends and preprocessor

  • Improved performance of the C frontend for Astrée analysis projects.
  • Fixed the reporting of location information for source-level comment and suppress directives in the /* Semantic hypotheses */ and /* Further directives */ sections of the output view and text report.
  • The directive __ASTREE_attributes(()) can now also be used in files that do not require preprocessing, such as the 'Wrapper and Stubs File'.
  • Improved reporting of invalid AAL directives, which no longer are reported as an error, but as a violation of diagnostic rule A.5.4 (check annotation-insertion-failed).
  • Improved the robustness of pattern comments with regard to code changes.
  • In the wrapper and stubs file, the use of extended identifiers (such as var@fun@"file.c") is no longer restricted to Astrée directives only. The syntax can now be used everywhere in that file.

Stub libraries, ABIs, OS and compiler configurations

  • Generalized the ARINC653 OS stubs and added support for the PikeOS personality. Deviations from the ARINC653 defaults can be configured by adding specific defines to preprocessor configurations, as indicated in the user manual.
  • Improved the stub libraries with respect to POSIX coverage and precision when analyzing C++.
  • Added abstract versions of std::vector and std::string to the C++ STL stubs for Astrée. The abstract version of std::vector does not allow the use of low-level pointer arithmetic on the underlying representation, e.g. using the pointer returned by data(). The abstract version of std::string supports efficient analysis of strings up to a total capacity of 100 bytes. API calls that exceed this limit raise an alarm and their effects are ignored.
  • Changed the default of the ABI setting enum_preferred_sign from signed to unsigned. This change also corrects the following target ABIs with respect to the preferred sign for enums:
    • 32-bit Intel x86
    • 64-bit x86
    • 32-bit ARM v6 and higher, ARM compiler, little endian
    • 32-bit ARM v4 or v5, ARM compiler, little endian
    • 16-bit C166, Tasking C166/ST10 compiler
  • The target ABI “16-bit C166, Tasking c166/ST10 Compiler” now uses enum_preferred_size=best to match the actual platform behavior.
  • Modified the AUTOSAR stubs to allow ISRs to interrupt each other when “ISRs may be nested” is set but no priorities for ISRs are specified.
  • Fixed frontend errors when using the deque, forward_list, or list implementations of the abstract stubs for the C++ STL library.

Qualification Support Kits

  • The TOR now include a general requirements section, as well as a section about input files and formats.
  • TOR descriptions are now more consistent and precise.

New test cases in the Astrée QSK

  • qk_rule_a_cpp_4_1
  • qk_rule_a_cpp_5_1
  • qk_rule_a_cpp_7_1
  • qk_rule_a_cpp_7_2
  • qk_rule_m2023_c_1_3
  • qk_rule_m2023_c_2_1
  • qk_rule_m2023_c_9_1
  • qk_rule_m2023_c_12_2
  • qk_rule_m2023_c_14_3
  • qk_rule_m2023_c_18_1
  • qk_rule_m2023_c_18_6
  • qk_rule_m2023_c_19_1
  • qk_rule_m2023_c_22_1
  • qk_rule_m2023_c_d_4_7
  • qk_rule_m2023_c_d_4_13
  • qk_rule_m2023_c_d_5_1
  • qk_rule_m2023_c_d_5_2
  • qk_check_class_inconsistent_definitions
  • qk_check_deadlock
  • qk_check_definition_duplicate
  • qk_check_multiple_atomic_accesses_between_sequence_points
  • qk_check_original_source_annotation_insertion_failed
  • qk_check_return_implicit
  • qk_check_unreachable_code_invariant
  • qk_check_unsequenced_modification
  • qk_commandline_export_entry_functions
  • qk_option_cut_misaligned_dereference
  • qk_option_precise_multiple_return_function
  • qk_option_unroll_loops_in_function
  • qk_option_warn_on_misaligned_dereference

The test case qk_abi_unaligned_derefence has been removed from the Astrée QSK.

Astrée QSK test cases extended to C++

  • qk_option_analysis_timeout
  • qk_option_auto_unroll
  • qk_option_auto_unroll_size
  • qk_option_automatic_octagon_packing
  • qk_option_cache_iterates
  • qk_option_congruence_intervals
  • qk_option_dump_data_dictionary
  • qk_option_dump_dataflow
  • qk_option_dump_escaping_locals
  • qk_option_dynamic_smash_threshold
  • qk_option_dynamic_smash_const_threshold
  • qk_option_dynamic_smash_variables_threshold
  • qk_option_equality
  • qk_option_fields_in_octagon_packs
  • qk_option_fold_contiguous_fields
  • qk_option_global_iteration_limit
  • qk_option_global_iteration_limit_per_phase
  • qk_option_inner_unroll
  • qk_option_interproc_oct_packs
  • qk_option_log_iter
  • qk_option_log_time
  • qk_option_log_parallel_iter
  • qk_option_main_unroll
  • qk_option_max_finite_int_set_size
  • qk_option_max_oct_pack_size
  • qk_option_narrow
  • qk_option_octagon
  • qk_option_octagon_epsilon
  • qk_option_print_packs
  • qk_option_print_widening_parameters
  • qk_option_relational
  • qk_option_smash_const_threshold
  • qk_option_separate_function
  • qk_option_shutdown_timeout
  • qk_option_smash_threshold
  • qk_option_state_machine
  • qk_option_symb
  • qk_option_text_report_tables
  • qk_option_warn_on_control_flow_anomaly
  • qk_option_warn_on_explicit_integer_cast_ranges
  • qk_option_warn_on_implicit_integer_cast_ranges
  • qk_option_warn_on_integer_arith_ranges
  • qk_option_warn_on_signed_integer_lshift_ranges
  • qk_option_widening_with_thresholds

New test cases in the RuleChecker QSK

  • qk_check_atomic_member_access
  • qk_check_atomic_void
  • qk_check_cast_integer_to_function_pointer
  • qk_check_chained_designation
  • qk_check_character_constant
  • qk_check_deprecated_declarations
  • qk_check_deprecated_exception_specification
  • qk_check_deprecated_implicit_copy
  • qk_check_deprecated_implicit_copy_with_destructor
  • qk_check_enable_bounds_checking_interfaces
  • qk_check_header_filename
  • qk_check_implementation_filename
  • qk_check_invalid_thread_object_use
  • qk_check_long_double
  • qk_check_memory_order
  • qk_check_multiple_atomic_accesses_between_sequence_points
  • qk_check_pointer_qualifier_cast_atomic
  • qk_check_pointer_qualifier_cast_atomic_implicit
  • qk_check_pointer_to_vla
  • qk_check_source_character_set
  • qk_check_stdint_constant_macro_small
  • qk_check_string_literal
  • qk_check_unreachable_code_invariant
  • qk_check_thread_resource_storage_duration
  • qk_check_volatile
  • qk_check_wchar_t
  • qk_check_wide_string_literal
  • qk_rule_a_cpp_4_1
  • qk_rule_a_cpp_7_1
  • qk_rule_a_cpp_7_2
  • qk_rule_autosar_0_4_4a
  • qk_rule_autosar_1_1_1a
  • qk_rule_autosar_2_3_1a
  • qk_rule_autosar_2_7_1a
  • qk_rule_autosar_2_11_1a
  • qk_rule_autosar_2_13_3a
  • qk_rule_autosar_2_13_4a
  • qk_rule_autosar_2_13_6a
  • qk_rule_autosar_3_1_2a
  • qk_rule_autosar_3_1_3a
  • qk_rule_cert_msc_9
  • qk_rule_m2023_c_d_1_1
  • qk_rule_m2023_c_d_2_1
  • qk_rule_m2023_c_d_3_1
  • qk_rule_m2023_c_d_4_1
  • qk_rule_m2023_c_d_4_2
  • qk_rule_m2023_c_d_4_3
  • qk_rule_m2023_c_d_4_5
  • qk_rule_m2023_c_d_4_6
  • qk_rule_m2023_c_d_4_7
  • qk_rule_m2023_c_d_4_8
  • qk_rule_m2023_c_d_4_9
  • qk_rule_m2023_c_d_4_10
  • qk_rule_m2023_c_d_4_11
  • qk_rule_m2023_c_d_4_12
  • qk_rule_m2023_c_d_4_13
  • qk_rule_m2023_c_d_4_14
  • qk_rule_m2023_c_1_1
  • qk_rule_m2023_c_1_2
  • qk_rule_m2023_c_1_3
  • qk_rule_m2023_c_1_4
  • qk_rule_m2023_c_1_5
  • qk_rule_m2023_c_2_1
  • qk_rule_m2023_c_2_2
  • qk_rule_m2023_c_2_3
  • qk_rule_m2023_c_2_4
  • qk_rule_m2023_c_2_5
  • qk_rule_m2023_c_2_6
  • qk_rule_m2023_c_2_7
  • qk_rule_m2023_c_2_8
  • qk_rule_m2023_c_3_1
  • qk_rule_m2023_c_3_2
  • qk_rule_m2023_c_4_1
  • qk_rule_m2023_c_4_2
  • qk_rule_m2023_c_5_1
  • qk_rule_m2023_c_5_2
  • qk_rule_m2023_c_5_3
  • qk_rule_m2023_c_5_4
  • qk_rule_m2023_c_5_5
  • qk_rule_m2023_c_5_6
  • qk_rule_m2023_c_5_7
  • qk_rule_m2023_c_5_8
  • qk_rule_m2023_c_5_9
  • qk_rule_m2023_c_6_1
  • qk_rule_m2023_c_6_2
  • qk_rule_m2023_c_6_3
  • qk_rule_m2023_c_7_1
  • qk_rule_m2023_c_7_2
  • qk_rule_m2023_c_7_3
  • qk_rule_m2023_c_7_4
  • qk_rule_m2023_c_7_5
  • qk_rule_m2023_c_7_6
  • qk_rule_m2023_c_8_1
  • qk_rule_m2023_c_8_2
  • qk_rule_m2023_c_8_3
  • qk_rule_m2023_c_8_4
  • qk_rule_m2023_c_8_5
  • qk_rule_m2023_c_8_6
  • qk_rule_m2023_c_8_7
  • qk_rule_m2023_c_8_8
  • qk_rule_m2023_c_8_9
  • qk_rule_m2023_c_8_10
  • qk_rule_m2023_c_8_11
  • qk_rule_m2023_c_8_12
  • qk_rule_m2023_c_8_13
  • qk_rule_m2023_c_8_14
  • qk_rule_m2023_c_8_15
  • qk_rule_m2023_c_8_16
  • qk_rule_m2023_c_8_17
  • qk_rule_m2023_c_9_1
  • qk_rule_m2023_c_9_2
  • qk_rule_m2023_c_9_3
  • qk_rule_m2023_c_9_4
  • qk_rule_m2023_c_9_5
  • qk_rule_m2023_c_9_6
  • qk_rule_m2023_c_10_1
  • qk_rule_m2023_c_10_2
  • qk_rule_m2023_c_10_3
  • qk_rule_m2023_c_10_4
  • qk_rule_m2023_c_10_5
  • qk_rule_m2023_c_10_6
  • qk_rule_m2023_c_10_7
  • qk_rule_m2023_c_10_8
  • qk_rule_m2023_c_11_1
  • qk_rule_m2023_c_11_2
  • qk_rule_m2023_c_11_3
  • qk_rule_m2023_c_11_4
  • qk_rule_m2023_c_11_5
  • qk_rule_m2023_c_11_6
  • qk_rule_m2023_c_11_7
  • qk_rule_m2023_c_11_8
  • qk_rule_m2023_c_11_9
  • qk_rule_m2023_c_11_10
  • qk_rule_m2023_c_12_1
  • qk_rule_m2023_c_12_2
  • qk_rule_m2023_c_12_3
  • qk_rule_m2023_c_12_4
  • qk_rule_m2023_c_12_5
  • qk_rule_m2023_c_12_6
  • qk_rule_m2023_c_13_1
  • qk_rule_m2023_c_13_2
  • qk_rule_m2023_c_13_3
  • qk_rule_m2023_c_13_4
  • qk_rule_m2023_c_13_5
  • qk_rule_m2023_c_13_6
  • qk_rule_m2023_c_14_1
  • qk_rule_m2023_c_14_2
  • qk_rule_m2023_c_14_3
  • qk_rule_m2023_c_14_4
  • qk_rule_m2023_c_15_1
  • qk_rule_m2023_c_15_2
  • qk_rule_m2023_c_15_3
  • qk_rule_m2023_c_15_4
  • qk_rule_m2023_c_15_5
  • qk_rule_m2023_c_15_6
  • qk_rule_m2023_c_15_7
  • qk_rule_m2023_c_16_1
  • qk_rule_m2023_c_16_2
  • qk_rule_m2023_c_16_3
  • qk_rule_m2023_c_16_4
  • qk_rule_m2023_c_16_5
  • qk_rule_m2023_c_16_6
  • qk_rule_m2023_c_16_7
  • qk_rule_m2023_c_17_1
  • qk_rule_m2023_c_17_2
  • qk_rule_m2023_c_17_3
  • qk_rule_m2023_c_17_4
  • qk_rule_m2023_c_17_5
  • qk_rule_m2023_c_17_6
  • qk_rule_m2023_c_17_7
  • qk_rule_m2023_c_17_8
  • qk_rule_m2023_c_17_9
  • qk_rule_m2023_c_17_10
  • qk_rule_m2023_c_17_11
  • qk_rule_m2023_c_17_12
  • qk_rule_m2023_c_17_13
  • qk_rule_m2023_c_18_1
  • qk_rule_m2023_c_18_2
  • qk_rule_m2023_c_18_3
  • qk_rule_m2023_c_18_4
  • qk_rule_m2023_c_18_5
  • qk_rule_m2023_c_18_6
  • qk_rule_m2023_c_18_7
  • qk_rule_m2023_c_18_8
  • qk_rule_m2023_c_18_9
  • qk_rule_m2023_c_18_10
  • qk_rule_m2023_c_19_1
  • qk_rule_m2023_c_19_2
  • qk_rule_m2023_c_20_1
  • qk_rule_m2023_c_20_2
  • qk_rule_m2023_c_20_3
  • qk_rule_m2023_c_20_4
  • qk_rule_m2023_c_20_5
  • qk_rule_m2023_c_20_6
  • qk_rule_m2023_c_20_7
  • qk_rule_m2023_c_20_8
  • qk_rule_m2023_c_20_9
  • qk_rule_m2023_c_20_10
  • qk_rule_m2023_c_20_11
  • qk_rule_m2023_c_20_12
  • qk_rule_m2023_c_20_13
  • qk_rule_m2023_c_20_14
  • qk_rule_m2023_c_21_1
  • qk_rule_m2023_c_21_2
  • qk_rule_m2023_c_21_3
  • qk_rule_m2023_c_21_4
  • qk_rule_m2023_c_21_5
  • qk_rule_m2023_c_21_6
  • qk_rule_m2023_c_21_7
  • qk_rule_m2023_c_21_8
  • qk_rule_m2023_c_21_9
  • qk_rule_m2023_c_21_10
  • qk_rule_m2023_c_21_11
  • qk_rule_m2023_c_21_12
  • qk_rule_m2023_c_21_13
  • qk_rule_m2023_c_21_14
  • qk_rule_m2023_c_21_15
  • qk_rule_m2023_c_21_16
  • qk_rule_m2023_c_21_17
  • qk_rule_m2023_c_21_18
  • qk_rule_m2023_c_21_19
  • qk_rule_m2023_c_21_20
  • qk_rule_m2023_c_21_21
  • qk_rule_m2023_c_21_22
  • qk_rule_m2023_c_21_23
  • qk_rule_m2023_c_21_24
  • qk_rule_m2023_c_21_25
  • qk_rule_m2023_c_22_1
  • qk_rule_m2023_c_22_2
  • qk_rule_m2023_c_22_3
  • qk_rule_m2023_c_22_4
  • qk_rule_m2023_c_22_5
  • qk_rule_m2023_c_22_6
  • qk_rule_m2023_c_22_7
  • qk_rule_m2023_c_22_8
  • qk_rule_m2023_c_22_9
  • qk_rule_m2023_c_22_10
  • qk_rule_m2023_c_22_12
  • qk_rule_m2023_c_22_13
  • qk_rule_m2023_c_23_1
  • qk_rule_m2023_c_23_2
  • qk_rule_m2023_c_23_3
  • qk_rule_m2023_c_23_4
  • qk_rule_m2023_c_23_5
  • qk_rule_m2023_c_23_6
  • qk_rule_m2023_c_23_8

The test case qk_abi_unaligned_derefence has been removed from the RuleChecker QSK.

RuleChecker QSK test cases extended to C++

  • qk_check_sline_splicing
  • qk_check_literal_assignment
  • qk_check_universal_character_name

Known issues

ID Short summary for 23.10 Status in 24.04 Status in 24.10
2310-00298If a process may run in several phases,
the analysis may fail to consider some possible values.
persistsfixed
2310-04870For variables with absolute addresses,
misaligned dereferences may not be reported under certain circumstances.
persistsfixed
2310-08263The Octagon domain computes wrong bounds for divisions in which the dividend is an integer > 9007199254740992 (253).fixedfixed
2310-11244With a specific combination of option settings,
the Equality domain may miss some of the possible values.
fixedfixed
2310-15218Tainting is not propagated
through certain expressions and statements.
fixedfixed
2310-19013Under specific circumstances, the C frontend may assume wrong types in parameter type lists.fixedfixed
2310-21344When the alignment of the underlying type of a bitfield is different from the size of that type, the analysis may compute a wrong layout under specific circumstances.fixedfixed
2310-25228Writing to an array element using a tainted index
does not taint the written array elements.
persistsfixed
2310-31346Analysis uses C99 scoping of iteration- and selection-statements when language version is set to C90.fixedfixed
2310-35245Five additional scenarios for known issue 2310-15218 when the option track-taint-hues is combined with certain directives.fixedfixed
2310-41360Initializers for volatile array elements or volatile struct and union members may be ignored in certain cases.persistsfixed
2310-45261Taints may not be propagated between asynchronous processes when using memcpy or copy assignment.persistsfixed
2310-51367Invalid pointer comparison alarms may be missing when comparing two null pointers in arithmetic expressions.fixedfixed
2310-57206Under specific circumstances, a comparison between pointers converted to integers may be unsound.fixedfixed
2310-61422__ASTREE_partition_ranges may fail to cover all possible floating point values when used with several intervals whose integer bounds relate in a specific way.persistsfixed
2310-67280Analysis of C++ code may fail to alarm about invalid pointer subtraction under specific circumstances.fixedfixed
2310-71615Upon activating the Interpolation domain,
conversion overflow alarms may be missing.
persistsfixed
2310-77822The Partitioning domain and the State Machine domain
may prevent expected effects of control flow tainting.
persistsfixed
2310-81667In two specific scenarios, the Interpolation domain may remove actually possible values and justified alarms about overflows.fixedfixed
2310-87855Taint analysis does not capture interferences due to the status of mutex locks or disabling/enabling all interrupts.persistsfixed
2310-92124The option exclude-signed-in-unsigned-overflows may hide conversion-overflow alarms for expressions that contain casts from signed to unsigned and then to enum.fixedfixed
2310-97864The Gauge domain may miss some of the incoming values
for a variable assigned in a loop.
fixedfixed

If you cannot upgrade to a more recent release for any reason, please write to support@absint.com with any issue IDs of interest to receive further details, code examples, tell-tale symptoms, and known workarounds.