Astrée/RuleChecker Release 23.10

Astrée
RuleChecker
GUI & server
Frontends & libraries
QSKs
Plain text

AbsInt License Server (ALM)

All network connections between the ALM server and its clients are now TLS-encrypted.

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.

alauncher

alauncher now supports scanning for installed products in arbitrary directories specified via the option --dir <path>

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

Improved precision for:

computations that involve bit masks
dynamic memory allocations from within C++ virtual methods
modulo operations in the congruence intervals domain
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).

Other improvements

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.
Astrée now accepts union expressions in struct and array initializers.
Updated malloc context limits to ensure that the calculation of malloc contexts does not take too long.
Improved the octagon packing heuristics to create more useful octagon packs on some code patterns.
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.
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;
```

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 pecifying additional includes and defines for the generated preprocessor configuration via an additional DAX file, as configured in the toolbox preferences.

Eclipse plugin

Support for automatic includes.
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 for C++

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.

C code

Removed false positives for:
- cast-integer-implicit (M.10.1) with initializers for bit-fields and at function return
- 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 of 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.

C++ code

Server and server controller

All network connections between analysis servers and clients are now TLS-encrypted.
Added support for external user authentication via 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. In addition, the context menu of graph nodes now offers actions to fold subtrees and display all call sites 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.

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.

Astrée and RuleChecker release 23.10