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. Extensive 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.