Astrée and RuleChecker Release 22.04 New, removed, and modified options * Removed the analyzer options symb-max-depth and list-decls. * The options cut-arithmetic-operations-on-null and cut-write-to-const are now enabled by default. The new defaults improve the analyzer's precision and performance and are suitable for most analysis projects. * The option assume-unknown-pointers-are-valid has been removed. For analysis projects that used this option it is advised to enable the more efficient option continue-on-definite-rte instead. * Added two new options smash-const-threshold and dynamic-smash-const-threshold for controlling the static and dynamic smashing of const arrays independently from the settings for non-const arrays. The options smash-threshold and dynamic-smash-threshold no longer apply to const arrays. To retain the behavior of previous releases, set smash-const-threshold to the same value as smash-threshold, and dynamic-smash-const-threshold to the same value as dynamic-smash-threshold. * The threshold value for the option dynamic-smash-threshold is now handled consistently in all cases. Dynamic folding is triggered when the number of possible targets of a read or write access is greater or equal to the configured threshold. In previous versions, the smashing was sometimes only triggered when the number of targets was strictly greater than the threshold. * Removed the filter domain sub-options filter1, filter_real, and filter_complex to simplify the use of the filter domain. * Overhauled and improved the implementation of the automatic octagon packing heuristics (controlled by the option automatic-octagon-packing). The former sub-options fewer-oct and max-variable-size-in-octagon are no longer needed and have been removed. * The new option taint-control-flow-context enforces taint propagation to the branches of control statements when their controlling expression is tainted. Improved precision * Improved communication between non-relational domains to enhance analysis precision. * Improved precision when evaluating switch statements. This also avoids duplicate alarms in switch selectors. * Improved precision of the modulo interval domain. * The analyzer-intrinsic function __astree_bzero is now handled more precisely and it no longer triggers dynamic smashing or folding. * The analyzer is now more precise on integer calculations of the form a + (b - a) * f / d when 0 <= f <= d. Such calculations typically appear in PT1 filters, low-pass filters, and linear interpolations. * Improved precision of __astree_memcpy and assignments when source and destination are folded differently. * Improved precision of congruence intervals, in particular for more precise handling of __ASTREE_global_assert on multi-dimensional arrays. Performance improvements * Improved performance of big array initialization. * Improved performance of analyzing loops that contain __ASTREE_partition_ranges directives. * Improved performance of analysis runs that enable multiple relational domains. Improvements for C++ * Astrée directives can now access private and protected members of objects. * Improved the reporting of unreachable code locations for template instantiations in the XML report and in the GUI. Further changes * When reporting an offset_overflow alarm, Astrée now cuts the corresponding offset to its valid range instead of allowing the offset to wrap around, as in previous versions. Consequently, the classification of the alarm has changed from ALARM (C) to ALARM (A). For example, in char arr[4294967295]; char *ptr = &arr[0] + 4294967296; the second line now also causes a definitive runtime error, since the offset is definitely too large. * After raising an ignored_recursive_call alarm, Astrée now cuts the context that leads to the recursive call, instead of ignoring the call and continuing with an under-approximation. * The __ASTREE_modify directive has been extended to allow the specification of additional distance constraints between neighboring array elements. These constraints can be taken into account by the interpolation domain to compute more precise bounds in interpolations over arrays. * Fixed the global counter of memory locations affected by data race alarms, as displayed in the analysis summary, with regard to dynamically allocated memory blocks. * Overhauled the implementation of the automatic partitioning heuristics. In rare cases, the new behavior may differ from the old one, causing changes in precision and performance of affected analyses. * Extended the syntax of the __ASTREE_ignore directive, such that it now also accepts regular expressions for matching multiple or very complex function names (e.g. for C++). * The alarm invalid_memory_operation is now only raised when the size argument that is supplied to an __astree_memcpy, __astree_bzero, __ASTREE_access, or __ASTREE_trash is not an integer value between 0 and 2^62 - 2. The invalid memory operation is no longer ignored. Instead it is performed with the admissible range of values for the size argument. * The analyzer no longer reports write_to_constant_memory alarms for bytes that are declared both const and non-const, which happens when const- and non-const-qualified members of a type overlap in memory, like in the union {int m; const int c;} or with bitfield members of a struct. * Dynamic folding and smashing are now applied more consistently when evaluating assignments or __astree_memcpy. * Improved the wrapper generator (Tools → Wrapper generator...). The generated wrapper code for an asynchronous program now assumes that user tasks can be started more than once. * Fixed an issue that sometimes caused __ASTREE_octagon_pack directives to be unexpectedly ignored. Rule sets and checks for C * Extended the documentation of the MISRA 2012 rule set to include examples and explanations from the MISRA document. * Added support for rule CWE.704. * Rule M2012.1.1 has been extended to check for violations of translation limits defined by the C standard. * The new diagnostic rule A.1.15 with check element-type-incomplete warns if the element type of an array is incomplete at the point of declaration. * The new diagnostic rule A.2.23 with check empty-initializer-list warns about braced initializer lists that are empty. * The new diagnostics check mixed-const-qualification (rule A.5.6) warns about mixed const and non-const qualification on shared bytes in struct/union, which will not be considered for reporting write_to_constant_memory alarms by the Astrée analyzer. * Added support for rule CERT.PRE.31 and CERT.DCL.39. * Alarms about violations of the following checks now also report the involved types: * object-pointer-diff-cast-strict (M.11.4) * object-pointer-diff-cast-strict-implicit (M.11.4) * object-pointer-diff-cast (M.11.4, M2012.11.3) * object-pointer-diff-cast-implicit (M.11.4, M2012.11.3) * Improved rule checks for M2012.21.4, M2012.21.5, M2012.21.6, M2012.21.10, M2012.21.11. The analyzer now additionally warns about the use of entities defined in the respective header files. * The new check newline-eof (M2012.1.3) warns about C source files not ending in a newline, which is a requirement imposed by the C standard. * Extended the rule checks for M2012.2.2 and CERT.MSC.12 to also report arithmetic operations with unused result (check expression-result-unused), and operations that do not have an effect on the operand, like +0 (check redundant-operation). * The new rule check unused-function (CERT.MSC.12, CWE.561, M.14.1, and M2012.2.1) reports static and external functions which are declared or defined but then never used in the project. Rule sets and checks for C++ * Extended the documentation of the MISRA-C++ 2008 rule set to include examples and explanations from the MISRA document. * The rules M2008.0.1.1 and AUTOSAR.0.1.1M now support the check unreachable_code. This check is only available when analyzing C++ code with Astrée (analysis mode astree-cxx). * The checks unused-parameter (M2008.0.1.3, AUTOSAR.0.1.3M, AUTOSAR.0.1.4A, M2008.0.1.11) and unused-parameter-virtual (M2008.0.1.3, AUTOSAR.0.1.3M, AUTOSAR.0.1.5A) no longer warn about parameters that are explicitly marked as [[maybe_unused]]. * The new check unused-private-method (AUTOSAR.0.1.3A) warns about unused private member functions. * The new check memcpy-overlapping-array (M2008.0.2.1, AUTOSAR.0.2.1M) reports uses of memcpy on overlapping parts of the same array, without depending on the Astrée analyzer. * Added the new checks deprecated-declarations, deprecated-implicit-copy, deprecated-implicit-copy-with-destructor, deprecated-exception-specification (AUTOSAR.1.1.1A) to report more deprecated features and, in some cases, replace less specific clang_warning diagnostics. Enhancements, clarifications, refinements, and fixes * RuleChecker now fully supports // file path separators in #include directives. * Metrics computation now distinguishes functions with identical names but different definitions in the source code, e.g. functions with internal linkage or explicit function template specializations. This also fixes false negatives and false positives for the corresponding metric threshold checks. * Fixed metrics calculations for CALLING and RPATH metrics. This also fixes false negatives and false positives for the corresponding metric threshold checks. * Removed spurious rule violations reported on C files in astree-cxx mode. They are now only reported on C++ files as documented. * Rules from the MISRA-C:2012 amendments (M2012A1 and M2012A2) can now be reclassified as "mandatory". * #pragma message no longer triggers the check clang-warning. * Streamlined message texts for metric threshold checks. * Removed false positives for the check integral-type-name (AUTOSAR.3.9.1A, M2008.3.9.2, M.6.3, M2012.D.4.6, X.A.5.6) regarding uses of the plain char type, and int as argument in C++ postfix operator declarations that are mandatory for overload resolution. * The check integral-type-name-extended (X.A.5.6) now reports uses of the char keyword in plain char type. * The following checks now also report violations for analysis projects with mixed C/C++ code: * check_definition_duplicate (A.CPP.7.2, M.8.9, M2008.3.2.2, M2008.3.2.4, AUTOSAR.3.2.2M, AUTOSAR.3.2.4M, CERT-CPP.DCL.60, M2012.8.6) * check_external_file_spreading (M.8.8, M2008.3.2.3, AUTOSAR.3.2.3M, CERT-CPP.DCL.60, M2012.8.5) * check_undefined_extern (M.8.9, M2008.3.2.2, AUTOSAR.3.2.2M, M2008.3.2.4, AUTOSAR.3.2.4M, CERT-CPP.DCL.60, M2012.8.6) This removes false positives for check_undefined_extern and false negatives for check_definition_duplicate and check_external_file_spreading in analysis projects with mixed C/C++ code. For rule checks on C code * Improved reported code locations for the check unreachable-code (CERT.MSC.12, CWE.561, M.14.1, M2012.2.1, X.A.5.22) for complex expressions statements. * Removed false negatives for the check definition-duplicate. The check now also warns about duplicate definition of functions. * Improved precision for the checks controlling-invariant and boolean-invariant to avoid false negatives. * Improved the reported location for call arguments (M.6.1, M.6.2). * Removed false negatives for the check extern-function-declaration (M.8.1, M2012.8.4) which did not warn about non-compliant function definitions when an already processed translation unit contained a declaration of this function. * Improved reporting for the check type-compatibility-link (A.1.1, CERT.DCL.40, CERT.MSC.40, ISO17961.funcdecl, M.1.1, M.8.4, M2012.1.1, M2012.D.2.1). Each symbol is now only reported once per translation unit. * 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), which now also reports variables introduced by C90 implicit function declarations. * Removed false positives for the check unused-parameter (M2012.2.7) which reported parameters solely used in Astrée directives. * Removed false negatives for the check implicit-zero-comparison (M.13.2), which did not warn about the operand of the logical operators !, &&, ||. * Removed false negatives for the check unreachable-code-after-jump (CERT.MSC.12, CWE.561, M.14.1, M2012.2.1), which failed to warn about unreachable code at the end of a function body and in switch case clauses. * Rule checks concerning type conversions are now also available for the constant expression of a case statement and the size expression at an array declaration. * Removed false positives for the check if-condition-lvalue (X.A.5.24). * Removed false positives for the checks identifier-unique-relaxed and identifier-unique-extern-relaxed (X.C.NAM.5) which did warn about local static objects. * Removed false negatives for the check local-object-scope (CERT.DCL.19, M.8.7, M2012.8.9) for variables used only in the initializers of function-local static objects within the same function. * Removed false negatives for the check external-redeclaration (M2012.8.5), which did not warn about redeclarations in the same line of source code. * When multiple functions have the same name and their definitions are in different original source files, metrics are now computed and displayed for all of them. This also fixes false negatives for the corresponding metric threshold checks. * The CDFUN metric considers more functions. This also fixes false negatives for the corresponding metric threshold checks. * The CALLING and RPATH metrics now deal with static functions whose names are also used for extern functions. This also fixes false negatives for the corresponding metric threshold checks. * The CALLS, CALLING, and RPATH metrics now correctly ignore function pointer calls, calls of Astrée analyzer intrinsic functions, and function calls in a switch statement that precede the first case or default tag. This also fixes false positives for the corresponding metric threshold checks. * Removed false negatives inside of macro definitions and false positives in code excluded by the preprocessor for the following checks: * no-whitespace-after-prefix (X.A.4.14) * no-whitespace-before-postfix (X.A.4.14) * statement-whitespace (X.A.4.9) * whitespaces-around-binary (X.A.4.12) * whitespaces-around-function-call (X.A.4.14) * Extended the check macro-unused (M2012.2.5) to report unused macros that are defined as: #ifndef MAKRO /* was formerly considered a use of MAKRO */ #define MAKRO 42 #endif * Removed false positives for the check assignment_overlapping (M.18.2, M2012.19.1). * Removed false negatives for the check pointer-integral-cast-implicit (A.1.4, CERT.INT.36, CERT.MSC.40, M.1.1, M.11.3, M2012.D.2.1, M2012.1.1, M2012.11.4) for expressions of array type, which are first converted to pointer and then to integral type. For example: int arr[10]; int var = arr; // the address of arr is converted to int, which was not reported * Removed false positives for the check pointered-deallocation (CERT.DCL.30, CERT.ARR.30, CWE.562, ISO17961.addrescape, M.17.6, M2012.18.6), which in rare cases was reported for calls to separately analyzed functions. * Removed false negatives for the following checks, which in rare cases ignored array sizes provided by a second declaration for the same entity: * incompatible-function-pointer-conversion and incompatible-object-pointer-conversion (A.1.11, CERT.MSC.40, M.1.1, M.11.1, M2012.D.2.1, M2012.1.1, M2012.11.1), * type-compatibility and type-compatibility-link (A.1.1, CERT.DCL.40, CERT.MSC.40, ISO17961.funcdecl, M.1.1, M.8.4, M2012.D.2.1, M2012.1.1), * incompatible-argument-type (CERT.EXP.37, ISO17961.argcomp, M.1.2, M2012.1.3), For rule checks on C++ code * Removed false negatives for the checks long-double (AUTOSAR.0.4.2A), wchar-t (AUTOSAR.2.13.3A), and integral-type-name (AUTOSAR.3.9.1A, M2008.3.9.2), which in some cases did not warn about explicit template parameters. * Improved reported code locations for the checks long-double (AUTOSAR.0.4.2A), wchar-t (AUTOSAR.2.13.3A), and integral-type-name (AUTOSAR.3.9.1A, M2008.3.9.2). * Removed false positives for the check unparenthesized-binary-logop-operand (AUTOSAR.5.2.6A) which erroneously reported parenthesized expressions that were subject to implicit type conversion. * Removed false negatives for the check member-function-missing-const (AUTOSAR.9.3.3M, M2008.9.3.3) for methods in class template specializations and false positives for out-of-line method template specializations. * Removed false negatives for the check uninitialized-member-modification-in-constructor (AUTOSAR.12.6.1A) when members are initialized in the constructor body by the array subscript operator []. * Removed false negatives and false positives for the check member-function-missing-const (AUTOSAR.9.3.3M, M2008.9.3.3) when members are accessed or modified by the array subscript operator []. * Removed false positives for the check include-guard-missing (AUTOSAR.16.2.3M, M2008.16.2.3). It no longer warns if a properly guarded header file includes itself. * Removed false negatives for the check include-guard-missing (AUTOSAR.16.2.3M, M2008.16.2.3). It now also warns about trailing comments behind the #endif of an include guard. * Removed false negatives for the check ambiguous-identifiers (AUTOSAR.2.10.1M, M2008.2.10.1) for preprocessor macro identifiers conflicting with non-macro identifiers. * Removed false positives for the check identifier-unique-tag (M2008.2.10.4) for definitions and forward declarations of structs within the same translation unit. Furthermore, violations of this check are now only reported once per translation unit. * Removed false positives for the check check-undefined-extern (AUTOSAR.3.2.2M, AUTOSAR.3.2.4M, CERT-CPP.DCL.60, M2008.3.2.2, M2008.3.2.4) which reported violations in generic template entities, even if definitions were available for all instantiations. * Removed false negatives for the checks numeric-char-usage and plain-char-usage for function call arguments (AUTOSAR.5.0.11M, AUTOSAR.5.0.12M, M2008.5.0.11, M2008.5.0.12). * Removed false positives and false negatives for the check exception_specification_mismatch_link. Implicit or default definitions of destructors, default/copy/move constructors, and copy/move assignment operators without explicit exception specification no longer participate in this check. * Removed false positives for the check class_inconsistent_definitions (A.CPP.7.2, M2008.3.2.2, M2008.3.2.4, AUTOSAR.3.2.2M, AUTOSAR.3.2.4M, CERT-CPP.DCL.60) for certain cases of class members of anonymous struct type. * Metric threshold checks now use the same rounding for metric values that is used when displaying and reporting the metric. * Removed false negatives (missing rule violations inside of named namespaces) and false positives (for method declarations) for the check static-function-declaration (M2008.3.3.2, AUTOSAR.3.3.2M, M.8.11, M2012.8.8, CERT.DCL.36). New DAX version 1.14 * Restructured the DAX specification of the AUTOSAR and OSEK OS configuration interface and introduced the new tag <sources/>. The new structure of these sections is now as follows: <autosar> <files/> <sources> <base/> <includes/> <defines/> <automatic-includes/> </sources> </autosar> <osek> <oil-file/> <oil-includes/> <sources> <base> <includes/> <defines/> <automatic-includes/> </sources> </osek> * Removed restriction about combining the option <relational>no</relational> with relational domain options. If <relational>no</relational> is present in a DAX file, it deactivates all relational domains, regardless of their individual settings. General * Updated the default for the C++ language version (option cxx-version) to C++17. When importing older DAX files that do not specify the cxx-version option, please add a <cxx-version>C++14</cxx-version> tag to preserve the former behavior. * The new option inline-semantics allows to configure the semantics of the inline specifier. Available values are "standard", which corresponds to the C language standard (default), and "gnu89", which implements GCC's -fgnu89-inline. * The new command-line option --import-only imports an AAF file without automatically starting the analysis. * Improved the handling of directory and file names that include non-ASCII characters. * Original source directives (ASTREE/RULECHECKER_suppress/comment) that are inserted via AAL annotations are now always applied to the same findings that they would be applied to if they were written as comments in the original source code. * Updated design of user manuals and other provided documents. * Improved support for Unicode file names in all tools. On Unices we assume the locale is set to a UTF-8 variant for the wanted language. * Updated sections about EN 50128 and EN 60657 in the Safety Manual. Integration with dSPACE TargetLink * Added support for TargetLink 5.2. * Added a new RuleChecker menu for creating RuleChecker projects and removed the RuleChecker entries and settings from the Astrée menu. * Renamed the report files <model>-astree-alarms.html to <model>-alarms.html and <model>-astree-log.xml to <model>-log.xml. Both reports are also available when using RuleChecker. Client GUI, batch mode, and report files * Updated the appearance of the graphical user interface to improve usability. * Added new views that show all C++ classes and class templates and their relationships within the current analysis project. * Overhauled the display of control flow information and improved its usability. It now follows the same logic as the data flow view, with a table in the Output area that can be filtered and explored via the corresponding Control Flow view in the results overview. * Added actions for exporting AAL files that only contain alarm comment annotations. * Improved the lookup of original source files to make it more robust in corner cases. * Fixed accidental horizontal scrolling in the dialog "Analysis time" clicking on an entry. * Fixed reappearance of hidden columns in the Findings view. * Fixed empty files table in the XML differences viewer tool. * Fixed unusually long loading times for certain analysis projects, in particular with clients running on Windows. * Improved the "Copy part" feature of the Findings view to enable copying from messages that exceed the width of the GUI. * The GUI now marks all code locations that cause alarms which are propagated to the calling function using the attribute raise_at_caller (e.g. in the C stub library). * The global result filter no longer influences the data and control flow information. * In custom report files, the list of selected files no longer influences the data and control flow information. * Fixed an issue that could cause AAL annotations to be marked as defect even if the analyzer did not report any findings for it. * Fixed duplicate reporting of AAL files in the report files section of the XML report. * Extended the Findings view to simplify the investigation of alarms in stub libraries that are raised at function calls into the library (see also the documentation of the raise_at_caller feature). * Extended the filtering in the Findings view so that it applies to all ALARM and CAUSE lines of all messages that are associated with the findings. The extended search can be disabled by deselecting the option "All message lines" in the menu that opens when clicking on the filter icon. * Added a new column "Message/Cause" which can replace the standard "Message" column. If an alarm is raised_at_caller, it shows the CAUSE line of the first message instead of the ALARM line. The preferred column can be configured via the context menu of the table header in the Findings view. * Report files can now be specified with a relative instead of an absolute file path. Relative paths are resolved with respect to the project's base directory. * Alarm comments that use the comment pattern mechanism are now included in XML report files generated by analysis runs in batch mode. * When reporting "Only modified" ABI settings during a DAX export and the ABI settings refer to a reference target that is not found on the file system during DAX export, the DAX export now creates an additional <export>-abi.dax that contains the ABI settings of that reference target. * Added new command line options to include invariants (--export-invariants) and analysis revisions (--export-revisions) in batch-mode exported AAF files (specified using the option --export). Server and server controller The server no longer creates a new "admin" user with default password when an existing data directory with all its contents is moved to a new directory using the server controller. Frontends and preprocessor * Updated the LLVM/clang toolchain to version 13. * C frontend: * Improved the reporting of (invalid) lvalues of incomplete type. * Improved the reporting of invalid __ASTREE_partition_ranges directives. Stub libraries, ABIs, OS and compiler configurations * C++ standard library: Added stub implementations for stream-related functions. The missing stub implementations could cause the analyzer to stop with a cxx_invalid_this_pointer alarm. * OS stub libraries: Revised Astrée directives for issue reporting and logging in the stub library for the ARINC_653 OS. * AUTOSAR ARXML-Converter: * Improved detection of RTA-OS. * Fixed generation of functions corresponding to schedule tables in AUTOSAR projects, which could be empty when using RTA-OS or Elektrobit OS. New test cases in the Astrée QSK * qk_abi_misspelled * qk_check_expression_result_unused * qk_check_mixed_const_qualification * qk_check_newline_eof * qk_check_redundant_operation * qk_check_unused_function * qk_directive_variable_at_function * qk_option_dynamic_smash_const_threshold * qk_option_inline_semantics * qk_option_smash_const_threshold * qk_option_taint_control_flow_context * qk_rule_a_5_6 * qk_rule_cwe_704 * qk_rule_m2012_1_3 The following test cases have been removed: * qk_option_assume_unknown_pointers_are_valid * qk_option_fewer_oct * qk_option_filter1 * qk_option_filter_real * qk_option_filter_complex * qk_option_list_decls * qk_option_max_variable_size_in_octagon * qk_option_symb_max_depth New test cases in the RuleChecker QSK * qk_abi_misspelled * qk_check_bad_header_macro_expansion * qk_check_element_type_incomplete * qk_check_empty_initializer_list * qk_check_expanded_side_effect_multiplied * qk_check_expanded_side_effect_not_evaluated * qk_check_function_argument_with_padding * qk_check_side_effect_not_expanded * qk_check_memcpy_overlapping_array * qk_check_mixed_const_qualification * qk_check_newline_eof * qk_check_redundant_operation * qk_check_unused_function * qk_check_unused_private_method * qk_option_inline_semantics * qk_option_misspelled * qk_rule_a_1_15 * qk_rule_a_2_23 * qk_rule_a_5_6 * qk_rule_autosar_8_4_2m * qk_rule_autosar_16_0_8m * qk_rule_autosar_19_3_1m * qk_rule_cert_dcl_39 * qk_rule_cert_pre_31 * qk_rule_m2008_8_4_2 * qk_rule_m2008_16_0_8 * qk_rule_m2008_19_3_1 * qk_rule_m2012_1_3 * qk_rule_m2012_21_11 The test case qk_check_include_tgmath has been removed from the RuleChecker QSK. RuleChecker QSK test case extended to C * qk_check_expression_result_unused RuleChecker QSK test cases extended to C++ * qk_check_extra_tokens * qk_check_include_errno * qk_check_parameter_name_match * qk_check_pointer_qualifier_cast_volatile ------------------------------------------------------------------------------ Last updated on 2 May 2022 by alex@absint.com. Copyright 2022 AbsInt. ------------------------------------------------------------------------------ An HTML version of these release notes is available at absint.com/releasenotes/astree/22.04