Astrée and RuleChecker release 24.10

Collaborative reviews of analysis findings

Users can now contribute comment suggestions to analysis projects that are owned by other users and not marked as private.

The analysis owner can see comment suggestions from other users in the new GUI view “Contributors”, which offers features for accepting, rejecting, and merging of suggestions.

Accepted or merged suggestions turn into proper comments that can be stored and exported as usual.

Improved precision

• The analysis precision has been improved for:
  • interval computations for modulo operations
  • comparisons that involve casts from integer to float with large values
  • the interpolation domain
  • octagons on expressions with bitwise AND (&) when one argument is a constant
  • boolean relations with floats when the float distance to 0 of the numeric variable depends on the boolean variable
  • expressions that involve pointer differences;
    if an invalid_pointer_arithmetics alarm definitely occurs in one of the sub-expressions, the analyzer now raises a definite runtime error and stops the context, instead of proceeding with an over-approximation
• Octagons now widen to the range of variables instead of infinity, resulting in more precise analyses.
• More accurate reached code statistics for C++.
• Statements are no longer reported to be unreachable (marked gray in the editor view) if sub-statements are reachable, e.g. via goto.
• The partition-array-access heuristics now also consider array accesses inside function calls.

Improved analysis of C++ code

• Astrée can now report data races and deadlocks in C++ and mixed C/C++ code. The corresponding options warn-on-data-race and warn-on-deadlocks are now available in the astree-cxx analysis mode.
• The following options are now also available for C++ analyses:
  • precise-priorities
  • list-not-reached
  • boolean-type
• The domain of boolean relations is now also available for C++, with the following options:
  • boolean-relation
  • automatic-boolean-packing
  • max-bool-vars
  • max-numeric-dep-in-bool-packs
• The directive __ASTREE_boolean_pack is now also available for C++.
• The context of an original source annotation for C++ may now contain empty lines comprised entirely of whitespaces. Such annotations are no longer rejected.
• Improved linking of results to code locations for frontend-generated temporaries.
• Corrected reached code statistics for non-global scope function declarations, and fixed sporadic counting of labels and empty statements.

Improved performance

• Improved the analysis of the main phase when the option separate-function is used. This may significantly reduce the overall analysis time for projects that have this option enabled.
• The tool can now be configured to run multiple tasks of the clang_frontend in parallel. This allows for a significant speedup of that analysis phase (in particular preprocessing and parts of rule checking, as well as C++ parsing) on multi-core systems.

SARIF support

Analysis findings can now be exported in the Static Analysis Results Interchange Format (SARIF).

Transport layer security

• All the tools on all platforms now uniformly use OpenSSL. Please keep your OpenSSL libraries up-to-date.
• When upgrading your client from a release older than 23.10, make sure to upgrade your License Manager as well. This is necessary due to the TLS-encrypted connection between the client and the License Manager that was introduced in release 23.10.

Options

• New option build-taint-graph to generate additional information about taint propagation. This information can be explored as a taint graph in the GUI to help understand the results of taint analysis.
• The float modulo relation domain is now disabled by default. It can be enabled by setting the new option float-modulo to yes. The mod option for disabling the domain has been removed. Entries of the form <mod>no</mod> can be removed from existing analysis configurations due to the new default.
• Added two new options for controlling the heuristics for automatic insertion of finite state machine directives:
  • switch-based-state-machine
    enables the tracking of switch-based state machines
  • state-machine-on-local-booleans
    enables a new strategy for automatic tracking of local boolean variables
• Improved boolean packing heuristics and added the following new options for enabling and controlling the heuristics:
  • automatic-boolean-packing
  • interproc-bool-packs-depth
  • max-numeric-dep-in-bool-packs
• Removed the option auto-generate-stubs. The default behavior of the analyzer does not change, but it is no longer possible to disable the automatic stub generation.
• Removed the deprecated options fewer-oct and max-variable-size-in-octagon.

Directives

• When an __ASTREE_assert directive definitely fails in a context and thus triggers a definite assertion failure error, the corresponding assertion failure alarm is now reported even if the directive is in the scope of an __ASTREE_suppress directive.
• Alarms raised in the scope of at_caller attributes are now always printed if they occur definitely in a given context (definite run-time error) even if suppress directives exist at the reporting locations.
• The directives __ASTREE_access((address, size)) and __ASTREE_trash((address, size)) now promote their arguments to void* and size_t, respectively.
• Astrée now raises an invalid-directive alarm when an __ASTREE_boolean_pack directive does not specify any boolean variable.
• When __ASTREE_taint_remove is applied to all bytes of a variable, the taints are now removed even when the variable is folded.
• Non-integer arguments to __ASTREE_states_track and __ASTREE_states_merge are now rejected by the frontend, with a violation of the check invalid-directive reported.
• The directives __ASTREE_partition_merge and __ASTREE_partition_merge_last no longer merge partitions of enclosing partitioned if/switch statements. Directives that do not merge any partitions are reported by the analyzer.
• The directives __ASTREE_octagon_pack and __ASTREE_boolean_pack now accept the var@"file" syntax in general, rather than only within wrapper-and-stubs files.

TargetLink

• Added support for TargetLink on Linux.
• Reworked the translation of input ranges from the TargetLink data dictionary into Astrée directives to improve analysis results.
• In exported DAX files, paths within <targetlink/> tags are now made relative to the directory in which the DAX file is exported.

Eclipse

The preprocessor option <abstract-cxx-stl-stubs/> is now only displayed for Astrée C++ projects. This prevents erroneous uses, e.g. in RuleChecker projects.

Jenkins

The Jenkins plugin for Astrée has been updated.

General improvements

• Updated Clang/LLVM to version 18.1.3.
• Error messages about definite runtime/assert failures are now more systematically reported for the whole statement, rather than only for a sub-expression. This may influence the per-location alarm counters in case of further findings at the affected extents.
• When a process is assigned to a phase range and the maximal phase where it can run is not the final phase of the project, Astrée will now try to prove that the process is definitely started and emit an alarm when it cannot prove it. In any case, Astrée always assumes that the process will have run at least once until its maximal phase.
• Fixed rare cases of unjustified dangling_pointer_use alarms.

RuleChecker

• Removed unjustified warnings about missing .../[Configuration.Annotations] file.
• Enabling a rule or rule set that is not available in the current analysis mode or with the current license now triggers an error.
• Alarm comments can now be reliably applied to rule violations that refer to whole source files.

Rule sets and checks for C

• New diagnostics rules:
  • A.2.24 warns about the use of #pragma pack
  • A.2.25 warns about the use of GCC’s conditionals with omitted operands in C code, i.e. (a ?: b)
• The MISRA-C:2023 rule set configuration now supports recategorization of individual rules.

Rule sets and checks for C++

Added support for the MISRA C++:2023 rules M2023-CPP.10.2.3, M2023-CPP.15.1.4, and M2023-CPP.18.3.1.

Rule sets and checks specific to Astrée

• Moved the checks conflicting-absolute-addresses and config-function-unknown from diagnostic rule A.5.4 to the new rule A.5.8 to highlight that they are only relevant for semantic runtime error analysis.
• The check conflicting-absolute-addresses (A.5.8) is now also supported in the C++ mode.

Enhancements, clarifications, refinements, and fixes

Both C and C++

• Fixed an issue which caused false positives and/or false negatives when re-running an analysis project on the server (incremental run).
• Fixed an issue that could cause rule violations to not be reported for some files referenced using “..”, for example in #include directives such as #include "/some/path/into/../file.h"

C code

• Corrected coverage claim for M2023-C.18.9 to “fully checked + exact”.
• Extended the checks dead-assignment (CERT.MSC.7, CERT.MSC.12, CWE.563, M2012.2.2, M2023-C.2.2) and dead-initializer (CERT.MSC.7, CERT.MSC.12, CWE.563) to report more definite violations in the presence of function calls. Removed false positives for both checks, which did not consider the use of a variable inside the array size of a declaration.
• Violations of the check macro-expansion (M.19.4) now state the macro expansion and refer to the respective macro definition.
• Removed false negatives for the check unnamed-constant (X.B.5.1) which failed to report constants in macro arguments for specific chained macro expansion patterns.
• Improved precision of the check return-implicit (CERT.MSC.37, M.16.8, M2012.17.4, M2023-C.17.4, X.F.41). It no longer reports functions which have dead code behind the return statement.
• Removed false positives for the checks macro-parameter-unparenthesized-expression and macro-parameter-unparenthesized-expression-strict (both M2012.20.7, M2023-C.20.7). They are now only checked for fully expanded macros.
• The check null-pointer-constant (M2012.11.9, M2023-C.11.9) now takes expansions of the macro NULL into account. It no longer relies on the expansion of NULL being of pointer type.
• The check cast-implicit (X.A.5.44) no longer warns about NULL being converted to pointer type.
• The check unused-function (CERT.MSC.12, CWE.561, M.14.1, M2012.2.1, M2023-C.2.1) no longer warns about functions that are called via __ASTREE_wrapper_call directives only.
• Improved precision of the check return-implicit (CERT.MSC.37, M.16.8, M2012.17.4, M2023-C.17.4, X.F.41). It no longer reports functions which have dead code behind the return statement.

C++ code

• The check incomplete-data-member-construction (AUTOSAR.12.1.1A) has been split into the checks incomplete-data-member-construction and incomplete-aggregate-data-member-construction. Note that the latter check no longer warns at aggregate definitions, but rather warns about aggregate object creations that leave the object uninitialized.
• The rule AUTOSAR.12.1.1A no longer warns in dependent contexts and about fields of class type that have proper constructors or implicitly-declared default constructors that are not used.
• Removed false positives for the check incomplete-data-member-construction (AUTOSAR.12.1.1A) w.r.t. unions.
• Fixed false negatives for the check incomplete-data-member-construction (AUTOSAR.12.1.1A). The check missed violations for implicitly-defined default and inheriting constructors.
• Fixed an issue that prevented certain rule checks from being applied to function parameter default expressions, template arguments, and array size expressions. This removes false negatives for the following checks:
  • evaluated-assignment-use (M2023-CPP.8.18.2)
  • potentially-throwing-static-initialization (AUTOSAR.15.2.1A, CERT-CPP.ERR.58)
  • global-initialization-callee-without-noexcept (M2023-CPP.18.4.1)
  • expression-result-unused (AUTOSAR.0.1.9M, M2008.0.1.9)
  • character-category-conversion (M2023-CPP.7.0.3)
• Fixed counting of operators for the LSCOPE metric on C++ code. This removes false positives and false negatives for the check max-language-scope (T.13.1).
• Adapted the check main-function-catch-all (AUTOSAR.15.3.3A, M2008.15.3.2, M2008.15.5.3, CERT-CPP.ERR.51) to the interpretation of rule M2023-CPP.18.3.1. MISRA C++:2023 only requires that a try catch(...) handler exists, not that it is the topmost statement followed only by a return statement. See also the following note for the new check exception-propagation-outside-catch-all.
• The new check exception-propagation-outside-catch-all (AUTOSAR.15.3.3A, M2008.15.3.2, M2008.15.5.3, M2023-CPP.18.3.1, CERT-CPP.ERR.51) covers situations explicitly mentioned in rule M2023-CPP.18.3.1, which used to be implicitly covered by the former (stricter) interpretation of the check main-function-catch-all, compare the release note above.
• Removed false positives of the check declaration-type-mismatch (AUTOSAR.3.9.1M, M2008.3.9.1) for declarations of the operator new.
• Removed false positives for the check unreachable-code (AUTOSAR.0.1.1M, M2008.0.1.1, M2023-CPP.0.0.1).
• Improved the handling of try-catch blocks when computing the PATH metric for C++.

Server and server controller

• The command line option --stop can now be used to remove analyses from the queue:

  a3cservercontroller --stop --id <ID of queued analysis>

• Fixed the automatic registration of the Astrée server as a Windows service.
• Improved startup performance of the Astrée server when a substantial amount of large projects is present in the data directory.

Processes

• The new table Processes in the Locations view displays the list of started processes and the relationship between processes that start each other.
• The new Process graph view displays the started processes and the relationship between processes that start each other.

DAX import and export

• Pattern and diff comments can now be imported into an already opened analysis project and immediately applied to existing findings, via “Project” → “Import Configuration…”. For pattern comments, this requires adding the new optional DAX tags <start-line/>, <start-column/>, <end-line/>, <end-column/> to the <comment-pattern/> section of the imported DAX files. The new tags are automatically added when exporting DAX from the client GUI.
• Improved the import of DAX files that contain relative paths:
  • Relative paths within <diff-comments/>, <rulechecks/>, and <original-source-annotations/> are now resolved relative to the directory that contains the DAX file in which these tags appear, even if they are imported by another DAX file.
  • The resolution of relative paths within <original-source-annotations/> tags now takes into account the (optional) global <base/> tag of the current DAX file.
  • When importing a configuration into an existing project, paths within <rulechecks/> tags are now resolved relative to the directory of the DAX file instead of using the current working directory of the client.
• Fixed path handling in the DAX export feature. Paths are once again made relative to the specified project base directory. Release 24.04 only generated absolute paths.
• Improved the export of DAX files that contain relative paths. Paths within <diff-comments/> and <targetlink/> tags are now made relative to the directory in which the DAX file is exported.

Editor view

• Analysis findings (alarms and errors) are now included in tooltips for affected code locations.
• Tooltips now indicate the code locations where parser filters were applied.
• The editor view now provides links above function definitions for:
  • callers/callees
  • findings
  • call graph

  Clicking on these links opens the Control flow, Findings, or Call graph view respectively, and filters it for the selected function.

• New navigation features for variables in the editor view:
  • Ctrl + mouse click on a variable jumps to the variable’s definition.
  • Ctrl + mouse click on a variable definition opens and filters the Data flow view.
  • Gray labels above variable definitions indicate the number of reads and writes. Clicking on the links opens the Data flow view filtered for reads or writes, respectively.
• Statements are no longer marked as unreachable in the editor view if sub-statements are reachable, e.g., via goto.

Reached code statistics

New and improved configuration of files and directories to consider for reached code statistics. The new interface provides the same expressiveness as the “Files and folders to check” feature of rule configurations.

• In the GUI, the relevant file paths to consider or ignore in the statistics can be configured in the new "Reached code" view in the configuration section.
• In DAX, the relevant file paths to consider or ignore in the statistics are configured via the following tags:

  <reached-code-statistics>
      <paths>
          <path action="add|remove" kind="folder|file">path</path>
      </paths>
  </reached-code-statistics>

• In the XML report, the relevant file paths to consider or ignore in the statistics are reported via the tags:

  <reached_code_statistics_configuration>
      <path is_file="0|1" include="0|1">path</path>
  </reached_code_statistics_configuration>

Custom reports

• When findings are ordered by file in the custom reports, the list now also includes findings that are reported outside the scope of a function.
• The Taints section in the custom report configuration dialog can now be reliably enabled.

Navigation shortcuts

• Searching by pressing Ctrl+Shift+F now automatically pre-fills the search field with the current selection. If nothing is selected, the word currently under the text cursor is used.
• The views “Patterns to ignore” and “External declarations” now allow filtering their entries via Ctrl+F.
• It is now possible to move annotations in the Annotations view using Alt+↑ and Alt+↓.

Data flow view

• Fixed the display of byte offsets in the “Locations” → “Data flow” view for values larger than 32 bit.
• The data flow view now displays access paths in addition to the range of byte offsets for each access. These access paths are displayed next to the variable names, using the same syntax as in C code and Astrée directives. For the case when these paths may not be precise enough, a tooltip is associated with each byte offset range, to display exactly what the analyzer knows about the offsets.

Rules configuration

The MISRA category selectors in the Rules configuration view have been improved:

• Users can now configure to which MISRA rule sets the category selection will be applied.
• Improved GUI performance when configuring MISRA categories.

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

• Improved performance when working with large numbers of taints.
• Fixed C++ original source annotation generation. It no longer fails or produces annotations that cannot be inserted properly when rerunning the analysis on the unmodified source code.
• The C++ specific preprocessor option “Use abstract stubs for the C++ standard template library” can now be saved persistently in the analysis project and in AAF files.
• Report file names that contain the % character are now accepted and correctly handled.
• Fixed a crash that could be triggered by dragging-and-dropping in the Preprocess view.
• The view “Findings per file” provides new context-menu actions to filter for findings that are reported outside the scope of a function.
• Changed the name and title of the former "Predefined: coverage" report to "Predefined: Reached code".
• When running the Astrée client in batch mode, the first SIGINT (Ctrl+C in the terminal that runs the command) now results in a soft stop. SIGTERM or any subsequent SIGINT result in a hard stop as before.
• AAL paths now support $ characters in function names.
• Fixed edit dialog for rule parameters that take lists or maps as arguments.
• The frontend now reports a list of locations where parser filters, as configured via “Patterns to ignore”, are applied. The verbosity of this list can be configured using the new option list-filtered-code.
• In the XML report, filtered code locations are no longer listed under

  <analysis><coverage><not_reached_location>

  but instead have moved to the new dedicated section

  <analysis><filtered_locations>

• Tooltips, __ASTREE_alarm, and __ASTREE_print directives now use the var@"file" syntax for referring more precisely to specific static variables.

Fixes

• Fixed an issue that caused the view “Locations” → “Not reached” to be empty when opening a project on the server or loading an AAF file.
• Fixed an issue that caused newly added diff comments (not yet present in the last analysis run) to be shown as “unused” after reopening a project.

Frontends and preprocessor

• “Patterns to ignore” with “Function” type are now interpreted as regular expressions, for both C and C++.
• C frontend:
  • Taking the address of a bitfield is now reported as a constraint error.
  • Switch statements are no longer rejected by RuleChecker when case/default labels are not immediately inside of the compound statement forming its body. Rule checks are now fully applied to such switch statements. Only the Astrée runtime error analysis still rejects them.
  • The #pragma pack is now supported in the same way as it is by GCC and Clang.
  • Fixed an issue that prevented anonymous global structs/unions from being visible if their first member was unnamed (such as a nested unnamed structure).
  • Support for GCC’s conditionals with omitted operands (a ?: b).
• C++ frontend:
  • Support for incremental preprocessing, parsing, and rule checking.
  • Support for the __RULECHECKER_comment/suppress aliases for __ASTREE_comment/suppress in analysis mode astree-cxx.
  • Support for __ASTREE/__RULECHECKER_comment/suppress directives in analysis mode rulechecker.
• The source frontend now fully supports the use of __ASTREE_import(()). This prevents unexpected error messages during parsing of the wrapper and stubs file.
• Fixed macro expansion in the source frontend for rule checking, which in rare cases caused syntax errors.
• The tool can now be configured to run multiple tasks of the clang_frontend in parallel. This allows for a significant speedup of that analysis phase (in particular preprocessing and parts of rule checking, as well as C++ parsing) on multi-core systems.
• New macros in the OSEK stub library allow customizing standard types such that they match the rest of the project.

Stub libraries, ABIs, OS and compiler configurations

• Fixed analysis wrapper generation for AUTOSAR software components when multiple ARXML files are specified.
• Fixed the memcmp implementation in the C stub library for analyses that set the ABI setting char_sign to signed.
• CompCert stubs:
  • Improved precision of
    • __builtin_clz, __builtin_clzl, __builtin_clzll,
    • __builtin_ctz, __builtin_ctzl, __builtin_ctzll,
    • __builtin_mulhd, and __builtin_mulhdu.
  • The PowerPC-specific builtins __builtin_get_spr and __builtin_get_spr64 now react to pairs of defines that specify up to three special registers with assumptions about their contents. The naming convention for these defines is

    __ASTREE_COMPCERT_USER_SPR_<N>__
    __ASTREE_COMPCERT_USER_SPR_<N>_MAX__
    
    __ASTREE_COMPCERT_USER_SPR64_<N>__
    __ASTREE_COMPCERT_USER_SPR64_<N>_MAX__
    
    /* where <N> is in 1..3 */ 
    

• Updated generation of stubs for schedule tables in AUTOSAR projects.

Qualification Support Kits

• Faster QSK execution, especially when the network connection betweent the client and the server is slow.
• The default location for report files is now based on the QSK installation path, and no longer on the current working directory.
• QSK runs now pass the --verify-certificate option to tool runs if requested by the Astrée client.

New test cases in the Astrée QSK

• qk_alarm_cxx_pure_virtual_call
• qk_alarm_cxx_exception
• qk_alarm_cxx_invalid_this_pointer
• qk_alarm_cxx_invalid_usage_of_iterator
• qk_check_csa_call_null_object_pointer
• qk_check_unsupported_language_feature_fatal
• qk_dax_reached_code_statistics

• qk_option_automatic_boolean_packing
• qk_option_build_taint_graph
• qk_option_interproc_bool_packs_depth
• qk_option_list_filtered_code
• qk_option_max_numeric_dep_in_bool_packs
• qk_option_skip_clang_static_analyzer_phase
• qk_rule_a_5_8

The test case qk_option_mod has been renamed into qk_option_float_modulo.

Astrée QSK test cases extended to C++

• qk_alarm_dangling_pointer_use
• qk_alarm_deadlock
• qk_alarm_infinite_loop
• qk_alarm_invalid_dynamic_memory_allocation
• qk_alarm_invalid_interval
• qk_alarm_invalid_memory_operation
• qk_alarm_invalid_pointer_arithmetics
• qk_alarm_invalid_usage_of_concurrency_intrinsic
• qk_alarm_invalid_usage_of_os_service
• qk_alarm_user_defined
• qk_alarm_read_write_data_race
• qk_alarm_taint_sink
• qk_alarm_uninitialized_variable_use
• qk_alarm_write_write_data_race
• qk_alarm_wrong_argument_count

• qk_check_annotation_insertion_failed
• qk_check_bitop_type
• qk_check_boolean_switch
• qk_check_conflicting_absolute_addresses
• qk_check_implicit_zero_comparison
• qk_check_invalid_directive
• qk_check_missing_rulechecking_phases
• qk_check_underlying_cvalue_conversion
• qk_directive_absolute_address
• qk_directive_access
• qk_directive_alarm
• qk_directive_analysis_log
• qk_directive_assert
• qk_directive_attributes
• qk_directive_boolean_pack

• qk_option_boolean_relation
• qk_option_boolean_type
• qk_option_list_not_reached
• qk_option_max_bool_vars
• qk_option_precise_priorities
• qk_option_state_machine_on_local_booleans
• qk_option_switch_based_state_machine
• qk_option_warn_on_data_race
• qk_option_warn_on_deadlocks

• qk_rule_m_13_2
• qk_rule_m_15_4
• qk_rule_m2008_5_0_21
• qk_rule_m2008_5_0_3

New test cases in the RuleChecker QSK

• qk_check_conditional_operand_omitted
• qk_check_exception_propagation_outside_catch_all
• qk_option_list_filtered_code
• qk_rule_a_2_24
• qk_rule_a_2_25
• qk_rule_m2023_cpp_18_3_1

The test cases qk_check_conflicting_absolute_addresses and qk_dax_path have been removed.

RuleChecker QSK test cases extended to C++

• qk_check_annotation_insertion_failed
• qk_check_invalid_directive
• qk_check_missing_rulechecking_phases
• qk_option_allow_signed_constant_with_unsigned
• qk_option_boolean_type