Astrée and RuleChecker release 24.04

New DAX version 1.16

  • Comment patterns are now stored in the new section <comment-patterns/>, rather than under <annotations/> as before.
  • Improved DAX export of analysis projects with an automatically generated wrapper and stubs file.
  • The new DAX attribute <annotations reference="<file>"/> can be used to specify an AAL insertion reference file from a previous analysis run.
  • When importing a preprocessor configuration from a DAX file into an already opened project, the base directory is now set to the directory from which the DAX file is imported, so that file paths are resolved relative to this directory.

Improved precision

  • The static analysis is now more precise with regard to:
    • global assertions on folded arrays
    • conditions over integer expressions that involve casts
    • pointer addresses stored in integer variables when the variable may also be zero (null)
    • array index partitioning heuristics (option partition-array-access)
    • the number of times that a process may start another process
  • Improved the precision of float computations such that small values close to zero can now be safely excluded from the result of certain operations.
  • Compute-through-overflow (CTO) calculations are now also available for CTO expressions that involve casts of signed integer constants to a smaller unsigned type (when the option exclude-signed-in-unsigned-overflows is enabled).

Options

  • The option taint-control-flow-context is now enabled by default.
  • The equality domain is now explicitly enabled by default (option equality=yes).
  • The options substitute-functions and dump-hypotheses are now also available for C++ (astree-cxx analysis mode).
  • New option warn-on-enum-overflows to control alarms about enum values that do not correspond to actual enumerators of their type.
  • Replaced the option warn-on-integer-arith-ranges by warn-on-unsigned-integer-arith-ranges which only controls the alarms for unsigned arithmetic overflows (predictable result), while signed overflows (undefined behavior) now always trigger a warning.
  • Replaced the option modular-signed-integers by the new option keep-signed-integers. With default settings, the behavior of the analyzer is unchanged. When the new option is set to no, Astrée tries to remove overflow values after reporting an arithmetic_overflow_unpredictable alarm, in order to improve precision.
  • Removed the options clamp-enum and modular-unsigned-integers.

Directives

  • Improved detection of invalid Astrée directives in C++ analyses.
  • Fixed support for array slice syntax in the __ASTREE_known_ranges directive for C++.
  • C++ analyses can now use the directives __ASTREE_modify, __ASTREE_initialize, and __ASTREE_check_separate_targets with expression access path with array slices. For example, __ASTREE_modify((arr[0:8])); is now accepted.
  • Fixed an issue that caused __ASTREE_initialize, as well as the initialization of arguments of functions called via __ASTREE_wrapper_call, to fail with error when the type of the argument was a struct with bitfield members.
  • Removed false alarm when calling __ASTREE_access or __ASTREE_trash with size 0.
  • Fixed missing annotation_insertion_failed diagnostics when trying to insert certain directives (e.g. __ASTREE_unroll or __ASTREE_partition_control) into a block using AAL, but without specifying the position before a particular statement within that block (as in { +1 loop {}} insert : <directive>).
  • Astrée is now better at estimating the number of cases for __ASTREE_partition_begin.
  • The directive __ASTREE_alarm now enforces using an alarm key of class A when adding the stop argument. To this end, the alarm key user_defined has changed from class C to class A. Moreover, the alarm keys read_write_data_race and write_write_data_race are now rejected in all uses of the directive.
  • Improved the precision of __ASTREE_modify and __ASTREE_known_range when targeting expressions that involve array accesses in which the index is expressed by a variable.

Taint analysis

  • Redesigned interface and clarified semantics of taint analysis. This entails the following changes:
    • Taint hues are expressed as strings.
    • The option track-taint-hues expresses an optional restriction of the set of legal taint hues.
    • The option taint-control-flow-context is enabled by default.
    • New directives __ASTREE_taint_add, __ASTREE_taint_add_if, __ASTREE_taint_remove, and __ASTREE_taint_alarm.
    • The directive __ASTREE_taint has been removed, and is now expressed as an __ASTREE_taint_remove followed by an __ASTREE_taint_add.
    • Clarified that semantics are based on sets of execution traces. Taints must only be added to variables that are directly or indirectly affected by program inputs (modeled via __ASTREE_modify or __ASTREE_volatile_input).
  • Taint analysis is now available for C++. The relevant options track-taint-hues, warn-on-tainted-control-flow, as well as the tainting directives are now also supported in astree-cxx mode.

Further information can be found in the user manual.

Toolbox for TargetLink

Added support for TargetLink 23.1.

Other improvements

  • Corrected the behavior of incremental analysis in the presence of #line directives in original source files. When rerunning an analysis in-place on the server, rule violations in such files were no longer displayed if the files did not change since the previous analysis run.
  • Reduced the use of disk space on the server and on the client side.
  • Updated Clang/LLVM to version 17.0.3.
  • Improved tooltips for C++.
  • An alarm that triggers a definite runtime error is now always reported, even if it is otherwise suppressed due to an __ASTREE_suppress directive.
  • Suppressed alarms no longer affect the proven code statistics.
  • Fixed an issue that prevented printing the content of string variables via %s in __ASTREE_alarm(()) or __ASTREE_print(()).
  • Astrée now raises an alarm (invalid_usage_of_concurrency_intrinsic) when a process tries to start another process that cannot run during the current phase or later.
  • Fixed specific, rare cases of false alarms about dangling pointers.
  • Overflows in signed left shift are now reported as arithmetic_overflow_unpredictable (rather than as arithmetic_overflow).
  • shift_argument alarms (second shift argument not in range) are now reported as class A alarms.
  • The text report and analyzer log output now displays full process names instead of shortened names.
  • Fixed an issue that could cause the analyzer to stop with the error message “Not_bot given bot”.
  • The analyzer now prevents folding consecutive fields in structs when they have incompatible qualifiers (e.g. const and non-const fields) to avoid unexpected alarms.
  • It is now possible to substitute a function (option substitute-functions) that has no definition even when auto-generate-stubs is set to no.
  • Functions that have been filtered from the code due to the options filter-asm-function or filter-pragma-inline-asm are now replaced by stubs when auto-generate-stubs is enabled (which is the default setting).
  • Fixed an efficiency issue in the domain of modulo relations (option mod=yes) that caused analyses to not terminate in acceptable time or to run out of memory.

AbsInt License Manager (ALM)

If you are upgrading your client from a release older than 23.10, you will need to upgrade your License Manager as well. This is due to the new TLS-encrypted connection between the client and the License Manager that was first introduced in release 23.10.

RuleChecker

  • The functional-safety use case description in the safety manual has been completed by mentioning Amendment 3 and 4 for MISRA C:2012 and by adding MISRA C:2023.
  • Improved the option text-report-tables:
    • The option is now also available for RuleChecker-only projects.
    • The new option value rule_violations produces a tabular overview of violated rules including the overall number of violations per rule.
  • Invalid rule numbers and rule set names, e.g. due to typos in DAX files, are now reported as configuration errors:
    ERROR other: Ignoring unknown rule key ... in rule check configuration

Rule sets and checks for C

  • The new diagnostic rule A.1.16 (no-declarator-in-struct) warns about struct/union member declarations which do not have a declarator (constraint violation).

Rule sets and checks for C++

Support for the new MISRA C++:2023 rule set.

Rule sets and checks specific to Astrée

  • The check ignored-partitioning (rule B.1.5) now reports when an __ASTREE_partition_merge_last(()) directive doesn’t have any partition to merge.
  • The new check astree-reserved-name (A.CPP.5.2) warns about usage of names that are used internally by Astrée.

Enhancements, clarifications, refinements, and fixes

Both C and C++

  • Improved the PATH metric to prevent unexpectedly high values in constant expressions and to remove false positives for the check max-number-of-paths (T.9.1).

C code

  • The directives __ASTREE_assert(()), __ASTREE_known_fact, and __ASTREE_known_range no longer influence rule checks about side effects. This removes false positives for the checks:
    • evaluation-order (M2023-C.13.2, M2023-C.1.3, M2012.13.2, M2012.1.3, M.12.2, CERT.EXP.30, CERT.EXP.10, A.4.1),
    • statement-sideeffect (M.14.2, CERT.MSC.12), and
    • expression-statement-pure (M2023-C.2.2, M2012.2.2, CWE.561).
  • The check struct-pointer-not-opaque (M2012.D.4.8, M2023-C.D.4.8) no longer erroneously reports struct types used as array element type, function return type, as type-name in a generic association, or as the operand of certain sizeof expressions.
  • Overhauled the checks ambiguous-identifiers and type-file-spreading to avoid redundant reporting of global identifiers.

C++ code

  • The check inherited-member-function-hidden (AUTOSAR.10.2.1A) no longer reports functions as hidden that are brought into scope of the derived class by a using directive. Moreover, copy and move assignment operators in the base class are no longer reported as hidden.
  • Removed false negatives for the check non-dynamic-virtual-downcast (AUTOSAR.5.2.2M, M2008.5.2.2). Invalid reinterpret_casts are now also reported.
  • The new check global-asm-declaration removes false negatives for the rule AUTOSAR.7.4.1A.
  • The check throwing-empty-outside-catch (M2008.15.1.3, AUTOSAR.15.1.3M) now warns about empty throws in the body of a lambda declared within a catch block. This interpretation now follows the clarified wording of the successor ruleset M2023-CPP.
  • Violations of the check non-pod-struct (AUTOSAR.11.0.1A) are now reported at definitions only and no longer repeated at each declaration.
  • The check stdlib-limits (AUTOSAR.0.4.4A) now uses Astrée analysis results, when available (mode astree-cxx).

Server and server controller

  • The credentials file has a new optional key client_auth_method that configures how to send the client_id and client_secret to the OAuth server.
  • HTTPS is now enforced for OAuth2 endpoint URLs.
  • The server controller now supports the option --credentials-file for batch mode execution with OAuth2 authentication.
  • Improved error message when a TCP connection is closed before the TLS handshake.
  • The server controller now displays warnings for the data directory when
    • access rights are inappropriate,
    • free disc space is below 2 GiB,
    • the directory is on a network filesystem.
  • Upon changing the server data directory in the server controller, a server restart is no longer required in order for clients to display source files and diff comments.
  • Fixed an issue that, depending on the host configuration, prevented the server controller from connecting to a local server that has the “Block connections from remote hosts” option enabled.

Client GUI, batch mode, and report files

  • When starting the client in GUI batch mode (using the option -B) and connecting to a server that requires OAuth authentication, the client now automatically opens the login page in your default Web browser.
  • The Taints view now displays the original location and the name of the affected function for each tainted location. Moreover, its context menu offers new actions to display the control flow information or call graph of the corresponding function.
  • Ctrl + P now opens a new go-to-anywhere HUD for quick navigation in the current project. It keeps a list of recently visited views, and can be searched for views not previously visited. The HUD automatically closes as soon as you click on any item within. Alternatively, click on the HUD’s border to close it without leaving the current view.

Custom reports

  • The custom report configuration has been extended to include taint information, and a new predefined custom report for taint analysis has been added (DAX key @taints).
  • Custom reports now once again include preprocessor configuration information.

Comments

  • Currently selected alarm(s) can now be commented using the new keyboard shortcut Ctrl + Alt + A.
  • The Diff comment mechanism can now also be used for commenting check_failure alarms originating from failed __ASTREE_check directives.
  • The “Unused comments” list in the Findings view has been improved. It now displays the key of the commented alarm, the comment mode used, and extra information for identifying the code location to which the comment was originally added.
  • Fixed the display of alarm comments in editor views for original source code.
  • Diff comments for alarms are now also displayed in the editor views.
  • Comment patterns for alarms are now also displayed in the editor views at the code location where they apply.
  • Fixed an issue that could cause the Diff comments view to display the comments twice.

Frontends and preprocessor

  • Fixed an issue that could cause __ASTREE_volatile_input and __ASTREE_global_assert directives with valid interval bounds to be rejected by the check invalid-directive after parsing them with the C++ frontend.
  • Fixed an issue that could cause the C frontend to run out of memory when encountering a #pragma directive in the last line of a C file.
  • Fixed an issue that could cause frontend error messages to disappear from the results when rerunning an analysis project on the server. The issue could only occur if the translation units in which the errors had been reported were not modified since the last analysis run.
  • It is now possible to specify an alternative base directory in which the tool looks for the stub implementations of the C and C++ standard libraries. This allows users to create modified copies of the stubs that are shipped with the product without modifying the stubs in the installation directory. The base directory for the modified stubs is specified in the Preprocess view or in DAX via the attribute path of the <clibrary/> tag.
  • The C frontend now rejects pointer arithmetic with pointer to function type as constraint violation.
  • Invalid values for the options c-version and cxx-version are now rejected already by the preprocessor.
  • Fixed an issue that in rare circumstances could cause preprocessing to stop with an error.
  • Updated AAL annotation extraction so that it works with all current directives.
  • The options filter-pragma-asm, filter-asm-preprocessor-directive, and filter-pragma-inline-asm no longer apply to text that is not a preprocessor directive.

Stub libraries, ABIs, OS and compiler configurations

  • Fixed the implementation of fesetround in the C stub library. Analysis results on invocations of the function are now more precise.
  • Fixed the implementation of the macro IS_START_CORE in the OSEK stubs. The previous implementation could result in wrong start-up of some cores for AUTOSAR projects with fewer applications than cores.
  • Fixed the stub implementation of __builtin_mulhd() for CompCert for PowerPC when multiplying a negative number with a positive one.

New test cases in the Astrée QSK

  • qk_check_astree_reserved_name
  • qk_check_controlling_invariant_static
  • qk_directive_taint_add
  • qk_directive_taint_add_if
  • qk_directive_taint_alarm
  • qk_directive_taint_remove
  • qk_option_keep_signed_integers
  • qk_option_warn_on_enum_overflows
  • qk_option_warn_on_unsigned_integer_arith_ranges
  • qk_rule_a_cpp_5_2

The test case qk_aal_comment_pattern_basic has been renamed into qk_dax_comment_pattern_basic.

The test cases qk_directive_taint, qk_option_clamp_enum, qk_option_modular_unsigned_integers, qk_option_modular_signed_integers, and qk_option_warn_on_integer_arith_ranges have been removed.

Astrée QSK test cases extended to C++

  • qk_alarm_array_out_of_bound
  • qk_alarm_assert_failure
  • qk_alarm_arithmetic_overflow
  • qk_alarm_arithmetic_overflow_unpredictable
  • qk_alarm_check_failure
  • qk_alarm_control_flow_anomaly
  • qk_alarm_conversion_overflow
  • qk_alarm_conversion_overflow_unpredictable
  • qk_alarm_float_division_by_zero
  • qk_alarm_global_assert_failure
  • qk_alarm_ignored_recursive_call
  • qk_alarm_int_division_by_zero
  • qk_alarm_int_modulo_by_zero
  • qk_alarm_int_undefined_modulo
  • qk_alarm_invalid_float_argument
  • qk_alarm_invalid_function_pointer
  • qk_alarm_invalid_pointer_comparison
  • qk_alarm_invalid_pointer_dereference
  • qk_alarm_invalid_pointer_subtraction
  • qk_alarm_misaligned_dereference
  • qk_alarm_offset_overflow
  • qk_alarm_overflow_upon_dereference
  • qk_alarm_shift_argument
  • qk_alarm_shift_first_argument
  • qk_alarm_square_root_argument
  • qk_alarm_stub_invocation
  • qk_option_dump_hypotheses
  • qk_option_substitute_functions
  • qk_option_track_taint_hues
  • qk_option_warn_on_tainted_control_flow

New test cases in the RuleChecker QSK

  • qk_check_controlling_invariant_static
  • qk_check_no_declarator_in_struct
  • qk_option_text_report_tables
  • qk_rule_a_1_16
  • qk_rule_m2012a3_10_3