Astrée and RuleChecker Release 20.10 Astrée for C++ and mixed code bases The Astrée run-time error analysis can now be applied to C++ and mixed C/C++ code bases. The new "astree-cxx" analysis mode supports all modern C++ versions up to C++17 and many of the features known from the classic C code analysis. Astrée’s C++ analysis uses the same technology as its C code analysis. It is designed to meet the characteristics of safety-critical embedded software, and is subject to the same restrictions as Astrée for C. The high-level abstraction features and template library of C++ facilitate the design of very complex and dynamic software. A wide use of these features may violate the established principles of safety-critical embedded software development and lead to unsatisfactory Astrée analysis times and results. The Astrée manual gives recommendations on the use of C++ features to ensure that the code can be well analyzed. For less constrained (less critical) C++ code, we recommend using the standalone RuleChecker. Improved precision ▲ Improved precision of: △ square of floats that may be NaN △ the domain of modulo intervals △ pointer comparisons △ global assertions when the octagon domain is active △ analysis runs for which the option "congruence-intervals" is enabled △ copying pointers from sources that are affected by data races, particularly when using the built-in function "__astree_memcpy" △ type-punning reads of individual bytes from larger integers. ▲ The values of smashed arrays that are subject to an "__ASTREE_global_assert" directive are now cut to the asserted range in more cases, resulting in more precise results. ▲ If a pointer variable is invalidated, e.g. due to an "__ASTREE_modify" directive, the result is now a strictly invalid pointer. ▲ If an integer variable that represents a pointer is invalidated, e.g. due to an "__ASTREE_modify" directive, the variable is set to its full integer range. ▲ The global settings for loop unrolling are no longer overridden by the loop unrolling heuristic, except if the heuristic determines a larger number of iterations to unroll. ▲ Astrée no longer warns when reading uninitialized bytes during "memcpy". Instead it copies their indeterminate values to the "memcpy" target and issues warnings if those bytes are read later. The new behavior eliminates false alarms when memcpying padding bytes while still catching the relevant undefined behaviors of C. ▲ Misaligned read accesses to smashed arrays are now handled more precisely. ▲ Improved widening for analyses using parallel processes and/or context-insensitively analyzed functions. ▲ If an "__astree_bzero" or "__ASTREE_modify" writes to all cells of a smashed array, the array is now considered initialized. This eliminates subsequent false alarms about reading from an uninitialized variable. ▲ Improved the accuracy of analyzed statements statistics. New features ▲ Astrée now raises an alarm: △ if the source of a "memcpy" is a dangling pointer △ for relational comparisons of NULL with itself (like "NULL > NULL") △ for relational comparisons (>, >=, <, <=) if one of the operands is an invalid pointer ▲ Added a new alarm kind "global_assert_failure" for distinguishing assertion failures reported for "__ASTREE_global_assert" directives from assertion failures reported for "__ASTREE_assert" directives. ▲ The new directive "__ASTREE_attributes" allows annotating functions and original source files with pre-defined attributes that modify the analyzer's behavior when analyzing them. The following attributes are available: △ "coverage_ignore" ignores function for coverage statistics △ "raise_at_caller" defers the main location of alarms raised in this function (or deferred to it by its callees) to this function's callers ▲ New options: △ "cut-arithmetic-operations-on-null" forces the analysis to cut all traces leading to arithmetics on null pointers. This new option is disabled by default. △ "equality" controls the equality relational domain, which tracks sets of known equal variables. This domain was formerly only available as part of the filter domain. This new option is disabled by default. △ "dump-escaping-locals" extends the option "dump-dataflow" to report reads and writes of non-static local variables occurring outside of the function in which they are defined. The option is enabled by default. △ "automatic-octagon-packing" disables the automatic creation of octagon packs without disabling the octagon relational domain. Octagon packs can still be created using the "__ASTREE_octagon_pack" directive. The new option replaces the former undocumented support option "automatic-pack" which is no longer accepted by the analyzer. ▲ Alarms raised in the the C stub library are now displayed and reported at the position of the C library call in the user code. ▲ The data flow view now also shows the range of byte offsets for each read or write access to a memory location. Improved program slicer ▲ Improved selection of slicing criteria. ▲ The computed program slices now contain the statements of the slicing criterion. Improved messages ▲ The format of alarm messages in the text report and output view of the analyzer has been modified. They now include a unique identifier for the reported kind of finding (finding key). Further changes have been made to improve clarity and consistency of alarm messages. ▲ Alarm messages about failed "__ASTREE_assert" and "__ASTREE_check" directives no longer print the code of the failed directive. To see the asserted or checked expression, please refer to the code snippet that is printed after the alarm message. ▲ Analyzer messages about the analysis entry function and context-insensitively analyzed functions now refer only to the function name instead of the whole function definition. ▲ If a separate context which may lead to a recursive call is excluded from the analysis, the analyzer now indicates the situation by the new specific alarm message "stopped_separate_context". Previous releases reported the situation less specifically as "recursive function". ▲ Improved the reporting of code locations not reached by the analyzer. In corner cases, code lines not reached were not reported as unreached. Other changes ▲ Renamed several finding-keys to clarify their meaning. Uses of old finding keys in comment directives are reported as errors. The error messages state the new keys to use △ "null_pointer_dereference" → "invalid_pointer_dereference" △ "invalid_memcpy" → "invalid_memory_operation" △ "read_data_race" → "read_write_data_race" △ "write_data_race" → "write_write_data_race" △ "recursive_function" → "ignored_recursive_call" ▲ The default value of the option "analysis-entry" has changed to "main". ▲ Removed support for deprecated syntactic variants of "__ASTREE_volatile_input" and "__ASTREE_global_assert". Such variants are now reported as violations of the diagnostic check "invalid-directive". ▲ Astrée no longer raises "invalid_pointer_comparison" alarms in relational comparisons (">", ">=", "<", "<=") of integers, usually resulting from violations of the diagnostic rule A.3.1. ▲ Removed false alarms about writing to supposedly const-declared memory for variables with declarations that violate the diagnostic rule A.1.1. ▲ Analyzer statement statistics now count "for" loops as either △ a single statement, if they are of the form for (; condition; increment) { loop-body } △ two statements, if they are of the form for (init; condition; increment) { loop-body } Statements in the loop-body are counted as usual. ▲ The analyzer now handles bitfields of length 0. ▲ The loop unrolling heuristic now counts multi-declarations (e.g. "int i,j;") as single statement. ▲ Reached/proven code is now properly highlighted for strong function definitions overriding a previously parsed weak function definition. ▲ If Astrée raises a class A alarm for an argument of an "__ASTREE_modify" directive, it may now cut invalid values. For example, if ptr may be "NULL" before "__ASTREE_modify((*ptr))", then Astrée raises a class A alarm for dereferencing "NULL" and continues assuming "ptr != NULL". If all values are invalid, the analyzer reports an error. ▲ If one of the bounds in an "__ASTREE_modify" directive may overflow the destination type, the bound is now replaced by the minimum/maximum of the destination type. For example, if "x" has an unsigned integer type, then __ASTREE_modify((x; [-10, 10])) now sets "x" to the range "[0,10]" instead of ignoring the effect of the directive. The invalid interval is still reported. ▲ When the option "continue-on-definite-rte" is set and a loop is found definitely non-terminating, then the exit condition of the loop is ignored so that the analysis continues after the loop. Bug fixes Fixed exceptional aborts of the analyzer that could occur: ▲ when combining separate analysis with dynamic variable smashing, ▲ when the option "continue-on-definite-rte" was enabled, ▲ when the option "congruence-intervals" was enabled, ▲ when analyzing code with incompatible type declarations for a global variable, ▲ when analyzing a compound literal in the condition of a loop, ▲ when calling a function with variable argument list via an "__ASTREE_wrapper_call" directive ▲ in rare circumstances when enabling the options "assume-unknown-pointers-are-valid" and "dump-data-dictionary" at the same time. RuleChecker ▲ Type information is now provided with the checks △ "shift-width-constant" (M.12.8, M2008.5.8.1, AUTOSAR.5.8.1M, X.A.5.39), △ "essential-shift-width" (M2012.12.2), and △ "precision-shift-width" (CERT.INT.34). ▲ RuleChecker now honors the order in which automatic includes are provided in the preprocessor configuration. Rule sets and checks for C ▲ New rule checks: △ "local-function-typedef" (rule X.E.5.2.2.11) warns about block-scope function type definitions △ "unreachable-code-after-jump" (M.14.1, M2012.2.1, CERT.MSC.12, CWE.561) reports code following "jump" statements in the same block, which is trivially unreachable ▲ New diagnostic rule A.2.22 that warns about the use of type "signed"/"unsigned long long" when "c-version" is set to "C90", which constitutes a language extension. ▲ All metrics now consistently consider Astrée built-in functions. ▲ The metrics PARAM, CALLS, CALLING, and RPATH now also consider unused static functions. This may trigger additional violations of the associated threshold checks △ "max-parameters" (M.1.1, T.6.1, X.C.LIB.6, and X.D.8.1.e) △ "max-number-of-called-functions" (T.10.1) △ "min-number-of-calling-functions" (T.11.1) △ "max-number-of-calling-functions" (T.11.2) △ "max-number-of-recursive-paths" (T.12.1) ▲ The rule check "unreachable-code" has been linked with rule CWE.561. ▲ "unsupported-language-feature-fatal" (diagnostic rule A.5.3) now also warns about uses of variably modified types (including variable length arrays) that cannot be analyzed with Astrée. ▲ "flexible-array-member" (M2012.18.7) has been extended to flexible array members in structures containing no other members (accepted C language extension). ▲ "empty-struct" (A.2.17) has been extended to report structures containing only a flexible array member (accepted C language extension). ▲ "unsupported-language-feature-fatal" (A.5.3) now also warns about the use of variable length arrays and variable modified types with side effects, as these cannot be analyzed with Astrée. ▲ "side-effect-in-conditional" (X.E.5.2.1.2) has been restricted to the first operand of the conditional operator. ▲ The diagnostic check "unused-suppress-directives" (B.1.2) now also warns about unused suppress and comment directives that are inserted via AAL. ▲ Removed false negatives for the check "evaluation-order" (rule A.4.1, CERT.EXP.10, CERT.EXP.30, M.12.2-required, M2012.1.3-required, M2012.13.2-required, X.A.5.34). It now also considers writes via array look-ups in a called function. ▲ Removed false positives for: △ "distinct-macro" (M2012.5.4) for code containing "#undef" directives △ "stdlib-limits" (M.20.3, M2012.D.4.11, CERT.FLP.32) which warned about the second parameter of "pow" or "powf" being "0" △ "object-type-mismatch" (M2012.8.3), which warned about compliant array declarations that differed only in the array size specification, such as int x[]; int x[10]; ▲ Fixed false negatives for: △ "array-initialization" (M2012.9.3) which did not warn about incomplete initializer lists initializing a sub-array inside of a multi-dimensional array, such as in int a[2][3] = {{1, 2}, {4, 5}}; △ "distinct-ordinary" (M2012.5.2), which did not warn about identifiers with external linkage when not being distinct from identifiers without external linkage (which is correctly not reported by the check "distinct-extern"). △ "distinct-tags" (M2012.5.2) which did not warn about forward-declared enum tags without definition. △ "extra-tokens" (M2012.20.13, M.19.16, X.E.5.2.5.2) which did not warn about non-compliant "#line" directives. △ "field-overflow-upon-dereference" (CWE.118, CWE.119, CWE.120, CWE.121, CWE.122, CWE.123, CWE.125, CWE.126, CWE.127, CWE.129, CWE.131, CWE.680, CWE.823) which did not report violations if the corresponding Astrée option "warn-on-field-overflows" was not enabled. △ "whitespaces-around-array-brackets" (rule X.D.7.1.e) which did not warn about missing spaces in abstract array declarators with no further inner declarator, such as in sizeof(int [ 10 ] ) ▲ Removed error about invalid syntax in "#elif" directives that are not reached by the preprocessor. ▲ Removed false alarms in "#elif" directives that are not reached by the preprocessor for rule checks "macro-undefined" (M.19.11, M2012.20.9) and "if-value" (M2012.20.8). ▲ Improved location information provided with violations of the check "invalid-directive". ▲ Fixed an issue preventing comments being applied to RuleChecker alarms addressing whole source files, such as check_min_comment_density. ▲ Fixed handling of "__has_include" and "__has_include_next". The arguments to these builtin macros had not been subject to macro expansion. ▲ Fixed incomplete lists of violated rules provided with RuleChecker alarms. The issue occurred if a check was used by more than one rule configuration with different rule sets enabled. ▲ Improved context information provided with alarms about violations of the rule check "composite-type-width". Rule sets and checks for C++ ▲ RuleChecker now supports the SEI CERT C++ coding standard. ▲ Extended rule check "float-comparison" to also cover indirect (in)equality tests of the form a - b < c || b - a < c and a - b <= c && b - a <= c ▲ Violations of the check "parameter-name-match" (AUTOSAR.8.4.2M, M2008.8.4.2) are now reported with a reference to the conflicting preceding declaration. ▲ Removed false positives for: △ "expression-statement-line" (AUTOSAR.7.1.7A) at "__ASTREE_*" directives. ▲ certain functions with non-generic parameter (i.e., if the parameter type T was provided by some surrounding class template, not the function template itself, and thus not generic), regarding the checks "missing-non-generic-copy-assignment" (M2008.14.5.3, AUTOSAR.14.5.3M) and "missing-non-generic-copy-constructor" (M2008.14.5.2). △ member functions declared with "=delete" for the following checks: ▲ "assignment-operator-without-ref-qualifier" (AUTOSAR.12.8.7A) ▲ "output-parameter" (AUTOSAR.8.4.8A) ▲ "public-abstract-copy-assignment" (M2008.12.8.2) △ "unused-local-variable" (M2008.0.1.3, AUTOSAR.0.1.3M) for unnamed exception declarations in catch handlers and objects with user-provided constructor or destructor such as "std::unique_lock". △ "precedence" (AUTOSAR.5.0.2M, M2008.5.0.2) for overloaded operators such as "<<" used with streams. △ "logop-postfix-operand" (M2008.5.2.1) for overloaded operators. △ "single-use-pod-variable" (AUTOSAR.0.1.4M, M2008.0.1.4), that erroneously reported a compliant identifier as non-compliant if 1. it did not have block scope, and 2. it did not have external linkage, and 3. it had exactly one use (in terms of the rule) in one translation unit. △ "plain-char-operator" (AUTOSAR.4.5.3M, AUTOSAR.5.0.11M, M2008.4.5.3, M2008.5.0.11) for operand expressions of type "signed char" / "unsigned char" (as opposed to plain "char"). △ "external-file-spreading" (AUTOSAR.3.2.3M, M2008.3.2.3) caused by friend declarations. △ "c-style-initialization" (AUTOSAR.8.5.2A) in for-range-declarations (see [stmt.ranged]). △ "hexadecimal-lower-case-digit" (AUTOSAR.2.13.5A) which did warn about user-defined literals if the ud-suffix contained one of the letters 'a' to 'f'. ▲ Fixed false negatives for: △ "hexadecimal-lower-case-digit" (AUTOSAR.2.13.5A) which did not warn about non-compliant floating literals. △ "integral-type-name" (AUTOSAR.3.9.1A, M2008.3.9.2), "wchar-t" (AUTOSAR.2.13.3A), "long-double" (AUTOSAR.0.4.2A) and "volatile" (AUTOSAR.2.11.1A) which did not warn about template arguments. ▲ The check "underlying-cvalue-conversion" (AUTOSAR.5.0.3M, M2008.5.0.3) no longer warns about △ conversions from "nullptr_t" △ conversions to "void*" pointers △ conversions from lambda expressions. ▲ The checks "member-function-missing-const" and "member-function-missing-static" (AUTOSAR.9.3.3M, M2008.9.3.3) no longer report virtually overriding methods which have to follow the signature of the method they override. ▲ Added metric CDFUN, with threshold check and mapping to rule T.14.1. ▲ The C++ metric STMT now counts null statements, thus removing false positives for the check "min-instructions" (T.5.1) and false negatives for the check "max-instructions" (T.5.2). ▲ Fixed an issue which caused the PATH metric calculation return the value 0 instead of an actually very large value, leading to false negatives for rule T.9.1. MISRA C++ ▲ Added support for the following rules: △ M2008.2.10.2 △ M2008.5.0.10 △ M2008.14.5.1 △ M2008.15.5.3 ▲ Improved support for rule M2008.15.4.1. AUTOSAR Added support for the following rules: ▲ AUTOSAR.2.10.1A ▲ AUTOSAR.10.1.1A ▲ AUTOSAR.10.2.1A ▲ AUTOSAR.12.0.1A ▲ AUTOSAR.12.1.1A ▲ AUTOSAR.12.1.2A ▲ AUTOSAR.12.1.3A ▲ AUTOSAR.12.4.1A ▲ AUTOSAR.12.6.1A ▲ AUTOSAR.12.7.1A ▲ AUTOSAR.12.8.4A ▲ AUTOSAR.12.8.6A ▲ AUTOSAR.13.2.2A ▲ AUTOSAR.13.5.1A ▲ AUTOSAR.13.6.1A ▲ AUTOSAR.14.5.2A ▲ AUTOSAR.14.5.3A ▲ AUTOSAR.14.7.2A ▲ AUTOSAR.15.1.1A ▲ AUTOSAR.15.2.1A ▲ AUTOSAR.15.3.3A ▲ AUTOSAR.15.3.6M ▲ AUTOSAR.15.4.2A ▲ AUTOSAR.15.4.3A ▲ AUTOSAR.15.5.1A ▲ AUTOSAR.15.5.2A ▲ AUTOSAR.15.5.3A ▲ AUTOSAR.18.1.1A ▲ AUTOSAR.18.1.2A ▲ AUTOSAR.18.1.3A ▲ AUTOSAR.18.1.6A ▲ AUTOSAR.18.5.1A ▲ AUTOSAR.18.5.2A ▲ AUTOSAR.18.5.11A ▲ AUTOSAR.18.9.1A ▲ AUTOSAR.18.9.3A ▲ AUTOSAR.20.8.5A ▲ AUTOSAR.20.8.6A ▲ AUTOSAR.26.5.1A ▲ AUTOSAR.26.5.2A Miscellaneous ▲ Removed configuration features for C++ from analysis mode "astree". C++ features are available in the analysis modes "astree-cxx" and "rulechecker". ▲ The analyzers now reject unsupported ABI configurations in which the specified alignment of a type is not a divisor of its specified size. ▲ AAL annotations can now also be inserted into original source code if the inserted directive is available for original code in the selected analysis mode (e.g. the new "__ASTREE_attributes" directive). This only works for top-level insertions (file scope). New DAX version 1.10 ▲ Explicit specification of the programming language (C or C++) in preprocessor configurations is now mandatory. <preprocess> <config name="My C files"> <language>C <!-- Mandatory in DAX 1.10. --> ... </config> </preprocess> ▲ The import of rule configurations from other DAX files has been modified as follows: △ If the importing DAX tag is named, then only the configuration with identical name is imported and its contents are merged with importing configuration. For example: <rulechecks import="file.dax" name="my configuration"> ... </rulechecks> △ If the importing DAX tag is unnamed and otherwise empty (no child tags), i.e. has the form "<rulechecks import="file.dax"/>", all configurations are imported as individual configurations. △ Name attributes of <rulechecks/> tags must be unique. Configurations without a "name" attribute are implicitly named “Configuration”. Client GUI and batch mode ▲ The finding-key of a comment directive can now be modified in the Edit dialog for comment annotations. ▲ New keyboard shortcut Ctrl+Shift+I in editor views for preprocessed code lets you insert an annotation after the current cursor position. ▲ The GUI widget for the parameter list of rule A.3.3 now accepts the input "long long". ▲ New default font for text editors and graphs. ▲ Fixed an off by one column imprecision when inserting AAL annotations in the first column behind a block. ▲ Fixed issues with the display of comments for C++ rule violations in the Findings view. ▲ Improved the performance of syntax highlighting and other markup in the text editor views. ▲ The following batch mode command line options are now also supported in GUI batch mode: △ --export △ --export-aal △ --export-only △ --export-preprocessed △ --queue ▲ Fixed AAL import of "__ASTREE_comment" directives with file name parameter. ▲ Fixed the widget for editing list arguments to RuleChecker rules. ▲ The editor history can now be navigated with the thumb buttons of the mouse. ▲ Results → Overview → Control Flow now also shows the call site. A double click on the ''Caller'' or the ''Call site'' jumps to the call site. A double click on the ''Callee'' jumps to the source code of the callee. ▲ The former 'Data flow' view has been renamed into 'Global data flow' and the corresponding report file sections have been renamed accordingly. The new tab in the 'Overview' view now also shows the location and (optionally) function in which a variable is defined. See also the release notes for the new Astrée option "dump-escaping-locals". ▲ Removed the “Convert directives to intrinsic functions ...” feature from the Tools menu. ▲ When adding a new annotation, the annotation overlay is displayed immediately in the editor view (using a green background). ▲ The GUI now shows tooltips when hovering over the arguments of certain Astrée directives or intrinsics in places where tooltips had not been available yet. ▲ Triggering a rerun of an analysis on the server via batch mode (using the option "--id") no longer updates the original source files on the server. ▲ The GUI’s DAX export dialog provides new options for fine-tuning the handling of file paths and the "config-file" option. ▲ Fixed a crash in Overview → Findings/F when searching files in very big projects. Report files ▲ The analysis reports now also provide code snippets for findings that refer to AAL annotations. ▲ The AAL export now contains alarm locations for comment annotations. This allows importing such comments into existing projects without the necessity of rerunning the analysis to see the comments in the Findings view or in the reports. If an imported comment cannot be applied to an alarm, the previous location is displayed in Findings → Show Unused Comments. ▲ If a rule with a string list or regular expression type option has an empty value, it is now handled as follows: △ in the printed RuleChecker configuration in all reports, except the XML report, it is now reported as "with option <empty>" instead of only "with option". For example: A.5.2 (full: pragma-usage, unsupported-language-feature) with option <empty> △ for the XML or DAX export the tag of the affected rule will now include the attribute "options=""" or "value=""", respectively. ▲ Fixed XML attribute duplication in report generation to ensure that XML report files are always valid XML. Server and server controller When upgrading to a new version, the server controller now imports the server settings of the previous installation. Frontends and preprocessor ▲ The lists of semantic hypotheses and further directives now report source directives w.r.t. their locations in the original source code instead of the code locations that these directives affect. ▲ The C frontend now accepts "__volatile" as a keyword alias of "volatile". ▲ Improved error message for invalid ABI settings of "sizeof_float", "sizeof_double", and "sizeof_long_double". ▲ Improved the handling of invalid "__ASTREE_comment" and "__ASTREE_suppress directives". Unknown alarm keys and comment classifications are now reported as violations of the check "invalid-directive" (diagnostic rule A.5.1) instead of leading to fatal parse errors. ▲ Invalid path specifications in the directives "__ASTREE_boolean_pack" and "__ASTREE_octagon_pack" are no longer reported as errors, but as violations of the diagnostic rule check "invalid-directive" (A.5.1). ▲ Fixed type information determined by the C frontend for "__typeof(f)" where "f" is an expression with function type. ▲ Reduced memory consumption of the C frontend, especially when using RuleChecker. ▲ Fixed the scope of compound literals created in iteration-statements in the C frontend. Their scope is now limited to the loop body. For example: int *p; while(p = &(int){0}, 0) { ... } /* The compound literal is out-of-scope, so 'p' is now a dangling pointer. */ ▲ With the option "anonymous-global-structs-and-unions" enabled, the C frontend also created global instances of struct types with tag, which in rare cases caused name conflicts during parsing. This has been fixed. Stub libraries, ABIs, and compiler configurations ▲ Added ABI configuration for AArch64 (little and big endian, GCC). ▲ Removed ABI configuration for "IAR for RL78 (Near)". ▲ Include paths to Astrée's OSEK and AUTOSAR stub implementations can now be overridden in preprocessor configurations. ▲ The C stub library implementation of "strtok" now modifies its first argument. ▲ Fixed the macros "INT16_C", "INT32_C", and "INT64_C" in the C stub library implementation which added inappropriate unsigned suffixes for certain ABI settings. OS configuration ▲ Added #undefs for all values redefined by the OSEK/AUTOSAR OS stubs and for "osSystemExtendedTask" and "osSystemBasicTask" to enable automatic integration analysis from ARXML files. The #undefs for "osSystemExtendedTask" and "osSystemBasicTask" can be disabled by adding the define "ASTREE_KEEP_EXTENDED_BASIC_TASK". ▲ A vendor-specific "osek.h" header file can be included in the analysis by simply adding its include path to the preprocessor configuration. If necesssary, inclusion of the vendor-specific "osek.h" can also be prevented by adding the define "ASTREE_SKIP_USER_OSEK_H". ▲ Fixed the handling of CAT1 interrupts for AUTOSAR analyses, as configured via the option 'Operating system: AUTOSAR' in the preprocessor configuration. ▲ For analyses with AUTOSAR OS and an ARXML configuration without any core specification, all applications are now executed on a fixed default core. In this case, adding the define "ASTREE_USE_MONO_CORE" to the preprocessor configuration for AUTOSAR OS also enforces a single core OS setup. Adding the define "ASTREE_USE_ANY_CORE" configures all applications to run on any core. QSK improvements ▲ Enhanced error messaging for test run specification errors (.config files). ▲ Renamed outdated term "Revision" for baseline information on title page of TOR/VTP documents to "Build". New test cases in the Astrée QSK ▲ qk_aal_insert_at_file_scope_into_original ▲ qk_aal_insert_source_comment ▲ qk_alarm_global_assert_failure ▲ qk_alarm_stopped_separate_context ▲ qk_alarm_user_define ▲ qk_check_expression_statement_dead ▲ qk_check_expression_statement_pure ▲ qk_check_unreachable_code_after_jump ▲ qk_commandline_analysis_description ▲ qk_commandline_analysis_name ▲ qk_dax_checks ▲ qk_dax_rules ▲ qk_rule_cwe_561 ▲ qk_directive_comment_source ▲ qk_directive_comment_source_external ▲ qk_directive_smash_variables ▲ qk_intrinsic_disable_all_interrupts ▲ qk_intrinsic_enable_all_interrupts ▲ qk_intrinsic_double_extract_exponent ▲ qk_intrinsic_huge_vall ▲ qk_metric_files ▲ qk_option_automatic_octagon_packing ▲ qk_option_cut_arithmetic_operations_on_null ▲ qk_option_dump_escaping_locals ▲ qk_option_equality ▲ qk_option_keep_comments ▲ qk_option_remove_analysis_files ▲ qk_option_use_internal_preprocessor Three test cases have been renamed: ▲ qk_alarm_negative_lshift_argument → qk_alarm_shift_first_argument ▲ qk_alarm_recursive_function → qk_alarm_ignored_recursive_call ▲ qk_option_entry → qk_option_analysis_entry The test cases "qk_option_checks", "qk_option_cxx_version", and "qk_option_rules" have been removed from the Astrée QSK. New test cases in the RuleChecker QSK ▲ qk_check_address_of_overload ▲ qk_check_alignas ▲ qk_check_alignof ▲ qk_check_analysis_run ▲ qk_check_array_argument_to_pointer_decay ▲ qk_check_atomic_qualifier ▲ qk_check_atomic_specifier ▲ qk_check_bad_include ▲ qk_check_bad_macro_expansion ▲ qk_check_case_clause_syntax ▲ qk_check_cast_integer_to_pointer ▲ qk_check_cast_pointer_to_integer ▲ qk_check_cast_pointer_void_to_function_pointer ▲ qk_check_cast_pointer_void_to_integer ▲ qk_check_clean_global_namespace ▲ qk_check_comma_operator ▲ qk_check_comma_overload ▲ qk_check_c_style_cast ▲ qk_check_declaration_type_mismatch ▲ qk_check_delete_operator ▲ qk_check_goto_into_try_catch ▲ qk_check_class_template_specialization_location ▲ qk_check_continue_in_bad_loop ▲ qk_check_direct_recursion ▲ qk_check_exception_caught_by_earlier_handler ▲ qk_check_functional_cast ▲ qk_check_generic_selection ▲ qk_check_impure_copy_constructor ▲ qk_check_inaccessible_base_class ▲ qk_check_inaccessible_external_function ▲ qk_check_include_clibrary ▲ qk_check_incomplete_base_construction ▲ qk_check_inconsistent_default_argument ▲ qk_check_logop_overload ▲ qk_check_long_long_c90 ▲ qk_check_loop_control_modification ▲ qk_check_loop_counter_manipulation ▲ qk_check_loop_counter_modification ▲ qk_check_loop_counter_step_equality ▲ qk_check_main_function ▲ qk_check_member_function_missing_const ▲ qk_check_member_function_missing_static ▲ qk_check_missing_else ▲ qk_check_missing_non_generic_copy_assignment ▲ qk_check_missing_non_generic_copy_constructor ▲ qk_check_mixed_virtual_base ▲ qk_check_new_operator ▲ qk_check_non_boolean_loop_control ▲ qk_check_non_diamond_virtual_base ▲ qk_check_non_explicit_fundamental_constructor ▲ qk_check_noreturn ▲ qk_check_public_abstract_copy_assignment ▲ qk_check_return_position ▲ qk_check_return_reference_parameter ▲ qk_check_return_reference_private_member ▲ qk_check_return_reference_private_member_const ▲ qk_check_return_reference_public_member ▲ qk_check_return_reference_public_member_const ▲ qk_check_switch_default_final ▲ qk_check_thread_local ▲ qk_check_throwing_null ▲ qk_check_throwing_pointer ▲ qk_check_undefined_string_literal_concatenation ▲ qk_check_underlying_signedness_conversion ▲ qk_check_underlying_signedness_cast ▲ qk_check_unrelated_pointer_conversion ▲ qk_check_unreachable_code_after_jump ▲ qk_check_unsequenced_modification ▲ qk_check_unused_internal_function ▲ qk_check_virtual_base ▲ qk_check_virtual_call_in_constructor ▲ qk_dax_checks ▲ qk_dax_rules ▲ qk_directive_attributes ▲ qk_option_code_lines ▲ qk_rule_m_20_3 ▲ qk_rule_m_21_1 ▲ qk_rule_m2012_17_2 ▲ qk_rule_m2012_18_1 ▲ qk_rule_m2012_d_4_1 ▲ qk_rule_m2012_d_4_11 ▲ qk_rule_m2012a2_1_4 ▲ qk_rule_m2012a2_21_3 ▲ qk_rule_m2012a2_21_8 ▲ qk_rule_m2012a2_21_21 ▲ qk_rule_cert_cpp_exp_53 ▲ qk_rule_cert_cpp_err_52 ▲ qk_rule_cert_cpp_err_54 ▲ qk_rule_cert_cpp_oop_50 ▲ qk_rule_cwe_118 ▲ qk_rule_cwe_123 ▲ qk_rule_cwe_124 ▲ qk_rule_cwe_125 ▲ qk_rule_cwe_126 ▲ qk_rule_cwe_127 ▲ qk_rule_cwe_129 ▲ qk_rule_cwe_823 ▲ qk_rule_autosar_0_1_1m ▲ qk_rule_autosar_0_1_3a ▲ qk_rule_autosar_0_1_4a ▲ qk_rule_autosar_0_1_4m ▲ qk_rule_autosar_0_1_6a ▲ qk_rule_autosar_0_1_10m ▲ qk_rule_autosar_0_2_1m ▲ qk_rule_autosar_2_5_2a ▲ qk_rule_autosar_2_7_1m ▲ qk_rule_autosar_2_13_1a ▲ qk_rule_autosar_2_13_2a ▲ qk_rule_autosar_3_9_1m ▲ qk_rule_autosar_4_5_1m ▲ qk_rule_autosar_4_10_1m ▲ qk_rule_autosar_4_10_2m ▲ qk_rule_autosar_5_0_1a ▲ qk_rule_autosar_5_0_2a ▲ qk_rule_autosar_5_0_4m ▲ qk_rule_autosar_5_0_5m ▲ qk_rule_autosar_5_0_9m ▲ qk_rule_autosar_5_0_14m ▲ qk_rule_autosar_5_0_20m ▲ qk_rule_autosar_5_2_2a ▲ qk_rule_autosar_5_2_9m ▲ qk_rule_autosar_5_2_11m ▲ qk_rule_autosar_5_2_12m ▲ qk_rule_autosar_5_3_1m ▲ qk_rule_autosar_5_3_3m ▲ qk_rule_autosar_5_18_1m ▲ qk_rule_autosar_6_2_1m ▲ qk_rule_autosar_6_2_2m ▲ qk_rule_autosar_6_3_1m ▲ qk_rule_autosar_6_4_1m ▲ qk_rule_autosar_6_4_2m ▲ qk_rule_autosar_6_4_4m ▲ qk_rule_autosar_6_4_6m ▲ qk_rule_autosar_6_4_7m ▲ qk_rule_autosar_6_5_2m ▲ qk_rule_autosar_6_5_3m ▲ qk_rule_autosar_6_5_4m ▲ qk_rule_autosar_6_5_5m ▲ qk_rule_autosar_6_5_6m ▲ qk_rule_autosar_6_6_3m ▲ qk_rule_autosar_7_3_1m ▲ qk_rule_autosar_7_3_2m ▲ qk_rule_autosar_7_4_3m ▲ qk_rule_autosar_7_5_2a ▲ qk_rule_autosar_8_3_1m ▲ qk_rule_autosar_8_5_0a ▲ qk_rule_autosar_9_3_1a ▲ qk_rule_autosar_9_3_1m ▲ qk_rule_autosar_9_3_3m ▲ qk_rule_autosar_10_1_1m ▲ qk_rule_autosar_10_1_2m ▲ qk_rule_autosar_10_1_3m ▲ qk_rule_autosar_10_2_1m ▲ qk_rule_autosar_10_3_3m ▲ qk_rule_autosar_12_1_1m ▲ qk_rule_autosar_12_1_4a ▲ qk_rule_autosar_14_5_3m ▲ qk_rule_autosar_15_1_2a ▲ qk_rule_autosar_15_1_2m ▲ qk_rule_autosar_15_3_6m ▲ qk_rule_autosar_16_0_1m ▲ qk_rule_autosar_17_0_5m ▲ qk_rule_autosar_18_0_1a ▲ qk_rule_autosar_18_5_2a ▲ qk_rule_autosar_18_7_1m ▲ qk_rule_autosar_27_0_1m ▲ qk_rule_m2008_0_1_1 ▲ qk_rule_m2008_0_1_4 ▲ qk_rule_m2008_0_1_5 ▲ qk_rule_m2008_0_1_7 ▲ qk_rule_m2008_0_1_10 ▲ qk_rule_m2008_0_1_11 ▲ qk_rule_m2008_0_2_1 ▲ qk_rule_m2008_2_5_1 ▲ qk_rule_m2008_2_7_1 ▲ qk_rule_m2008_2_10_4 ▲ qk_rule_m2008_2_13_1 ▲ qk_rule_m2008_2_13_5 ▲ qk_rule_m2008_3_1_3 ▲ qk_rule_m2008_3_9_1 ▲ qk_rule_m2008_4_5_1 ▲ qk_rule_m2008_4_5_2 ▲ qk_rule_m2008_4_10_1 ▲ qk_rule_m2008_4_10_2 ▲ qk_rule_m2008_5_0_1 ▲ qk_rule_m2008_5_0_4 ▲ qk_rule_m2008_5_0_5 ▲ qk_rule_m2008_5_0_9 ▲ qk_rule_m2008_5_0_13 ▲ qk_rule_m2008_5_0_14 ▲ qk_rule_m2008_5_0_20 ▲ qk_rule_m2008_5_2_4 ▲ qk_rule_m2008_5_2_7 ▲ qk_rule_m2008_5_2_9 ▲ qk_rule_m2008_5_2_11 ▲ qk_rule_m2008_5_2_12 ▲ qk_rule_m2008_5_3_1 ▲ qk_rule_m2008_5_3_3 ▲ qk_rule_m2008_5_18_1 ▲ qk_rule_m2008_6_2_1 ▲ qk_rule_m2008_6_2_2 ▲ qk_rule_m2008_6_3_1 ▲ qk_rule_m2008_6_4_1 ▲ qk_rule_m2008_6_4_2 ▲ qk_rule_m2008_6_4_4 ▲ qk_rule_m2008_6_4_6 ▲ qk_rule_m2008_6_4_7 ▲ qk_rule_m2008_6_5_2 ▲ qk_rule_m2008_6_5_3 ▲ qk_rule_m2008_6_5_4 ▲ qk_rule_m2008_6_5_5 ▲ qk_rule_m2008_6_5_6 ▲ qk_rule_m2008_6_6_3 ▲ qk_rule_m2008_6_6_5 ▲ qk_rule_m2008_7_3_1 ▲ qk_rule_m2008_7_3_2 ▲ qk_rule_m2008_7_4_3 ▲ qk_rule_m2008_7_5_4 ▲ qk_rule_m2008_8_3_1 ▲ qk_rule_m2008_8_5_1 ▲ qk_rule_m2008_9_3_1 ▲ qk_rule_m2008_9_3_2 ▲ qk_rule_m2008_9_3_3 ▲ qk_rule_m2008_10_1_1 ▲ qk_rule_m2008_10_1_2 ▲ qk_rule_m2008_10_1_3 ▲ qk_rule_m2008_10_2_1 ▲ qk_rule_m2008_10_3_1 ▲ qk_rule_m2008_10_3_3 ▲ qk_rule_m2008_12_1_1 ▲ qk_rule_m2008_12_1_2 ▲ qk_rule_m2008_12_1_3 ▲ qk_rule_m2008_12_8_1 ▲ qk_rule_m2008_12_8_2 ▲ qk_rule_m2008_14_5_2 ▲ qk_rule_m2008_14_5_3 ▲ qk_rule_m2008_15_0_2 ▲ qk_rule_m2008_15_1_2 ▲ qk_rule_m2008_15_3_6 ▲ qk_rule_m2008_16_0_1 ▲ qk_rule_m2008_16_0_4 ▲ qk_rule_m2008_16_2_1 ▲ qk_rule_m2008_16_2_6 ▲ qk_rule_m2008_17_0_5 ▲ qk_rule_m2008_18_0_1 ▲ qk_rule_m2008_18_7_1 ▲ qk_rule_m2008_27_0_1 RuleChecker QSK test cases extended to C++ ▲ qk_check_assignment ▲ qk_check_compound_ifelse ▲ qk_check_compound_loop ▲ qk_check_compound_switch ▲ qk_check_float_comparison ▲ qk_check_include_position ▲ qk_check_include_setjmp ▲ qk_check_include_signal ▲ qk_check_include_stdio ▲ qk_check_include_syntax ▲ qk_check_macro_function_like ▲ qk_check_switch_label ▲ qk_check_switch_clause_break ▲ qk_check_union ▲ qk_check_unused_parameter The test cases "qk_option_checks" and "qk_option_rules" have been removed from the RuleChecker QSK. ------------------------------------------------------------------------------ Last updated on 16 August 2021 by alex@absint.com. Copyright 2020-2021 AbsInt. ------------------------------------------------------------------------------ An HTML version of these release notes is available at absint.com/releasenotes/astree/20.10