Astrée and RuleChecker release 21.04

Improved precision

  • to avoid false alarms when comparing pointers to absolute addresses
  • to avoid false alarms for accessing uninitialized memory
  • of the symbolic domain on comparisons involving (implicit or explicit) casts
  • of the interpolation domain
  • on initialization of folded and smashed variables
  • on loops containing break or return statements
  • when more than one process runs in an intermediate concurrent phase
  • regarding the possible states of mutex locks, which in many cases also reduces memory consumption and analysis time
  • of __ASTREE_modify((*ptr; full_range)) when ptr is of type float* and might point to several different memory locations. The directive then no longer adds ±Inf/NaN to *ptr.

New and improved options

  • Added new options for bounded analysis, to obtain incomplete results in shorter time.
    • global-iteration-limit allows bounding the number of global iterations of the analyzer. The option is off by default.
    • global-iteration-limit-per-phase allows bounding the number of global iterations for each asynchronous phase of the analysis. The option is off by default.
  • The new option warn-on-memory-leaks raises alarms when
    • there is a terminating trace where dynamically allocated memory isn't freed prior to termination or
    • there is a non-terminating trace where the memory consumption grows indefinitely.
    Enabling the option also configures the C stub library to assume that malloc never returns NULL.
  • Enabling the new option ais-export-source-location switches the export of AIS annotations for AbsInt's WCET and stack analysis tools from the default "routine calls" annotations to more precise source-code relative annotations.
  • Improved the specification of functions for context-insensitive analysis. The option separate-function now accepts new parameters for fine-tuning separate functions for different analysis phases and processes.
  • Setting the option text-report-tables to empty now removes all tables from the text report instead of printing the default tables.
  • In analyses that use the option separate-function for context-insensitive analysis, the analyzer now covers separate contexts with possibly recursive functions up to true recursions. The alarm message
    ALARM (A) stopped separate context: context may be recursive
    that warned about not fully covered separate contexts has been removed.
  • The pre-computation of static dependencies for the arithmetic-geometric abstract domain (enabled by dev-geo=yes) now stops if the dependency graph grows very large.

General improvements

  • Improved the loop unrolling heuristic to work with loop conditions that contain shift operations.
  • Local variables names in the data flow view and text report table are now extended by the corresponding function names as var@function, to help distinguish multiple occurrences of the same variable name.
  • Improved the propagation of information from local variables to global variables or to variables from other functions. The improvement only affects analyses that directly or indirectly enable the equality relational domain.
  • Significantly improved the analyzer’s performance on analysis projects with concurrent processes and/or context insensitively analyzed functions.
  • Extended the __ASTREE_global_assert directive so that it is now possible to assert the variables and functions a pointer may point to. The associated syntax is described in the documentation.
  • In the case of an __ASTREE_global_assert violation on a smashed variable of union type, Astrée now computes more precisely in which cases the violation cannot occur and continues the analysis with these cases.

Improvements for C

  • Extended the syntax of the AAL annotation language by insert comment to permit insertion of ASTREE_comment and ASTREE_suppress directives in comment blocks within original source files. For example:
    __ASTREE_annotation((
      "main.c" insert comment: ASTREE_comment(...)
      "main.c" insert comment: ASTREE_suppress(...)Ii  
    ));

Improvements for C++

  • The reachability information (option list-not-reached and gray markings in the GUI) has been improved for C++, in particular in the presence of templates. A statement is completely grayed out in the code view only if it cannot be reached at all. If parts of a statement are unreachable, e.g. the increment in a for-loop or the operands of lazily evaluated operators (||, &&), only these parts are grayed out.
  • Improved precision of relational comparisons of null pointers in C++.
  • Astrée's C++ analysis mode now supports the suppression of alarm messages via the context menu of the Findings view.
  • The new alarm message
    cxx_invalid_this_pointer: this pointer may be null or invalid
    is raised when calling a member function with an object pointer that may be null or dangling.
  • Improved naming of constructors/destructors in C++.
  • Improved reported code locations for template declarations without definition.
  • Improved precision of __ASTREE_partition_control if (cond) ... and __ASTREE_partition_expr((cond)); when cond is an expression that uses the lazily evaluated logical operators || or &&.
  • The state machine domain is now available for C++ analyses. The domain is controlled by the option state-machine and by the directives __ASTREE_states_track and __ASTREE_states_merge.
  • Improved precision on lazily-evaluated logical conditions in loops.
  • Astrée’s C++ run-time stub library now supports the analysis of an arbitrary number of global objects destructors. The number of analyzed destructors was formerly limited to the first 1024 global objects.
  • The C++ analysis mode now provides additional, more abstract stub implementations for the following STL containers:
    • std::list
    • std::forward_list
    • std::deque
    • std::set
    • std::multiset
    • std::map
    • std::multimap
    • std::unordered_set
    • std::unordered_multiset
    • std::unordered_map
    • std::unordered_multimap
    The new stubs are disabled by default and can be enabled by setting the preprocessor option "Use more abstract stubs for the C++ standard template library" in the GUI or by adding the tag <abstract-cxx-stl-stubs>yes</abstract-cxx-stl-stubs> to the <preprocess/> section of DAX files.
  • When enabling the new, more abstract stubs for STL containers, Astrée reports erroneous uses of STL iterators in C++ using the new alarm cxx_invalid_usage_of_iterator. The alarm is reported in the following situations:
    • usage of an invalidated iterator
    • comparison of incomparable iterators, like invalidated iterators or iterators of different container objects
    • incrementing a valid but non-incrementable iterator, e.g. a one-past-end iterator
    • decrementing a valid but non-decrementable iterator, e.g. an iterator pointing to the first element
    • dereferencing a non-dereferencable iterator, e.g. a one-past-end iterator
    • insert into a sequence container using a range of iterators from the same container

Fixes

  • Fixed exceptional aborts of the analyzer related to dynamic smashing of variables.
  • Fixed an exceptional abort in the analyzer when using a predicate function In the condition of a loop which was not unrolled at all.

RuleChecker

  • Rule checks that are concerned with preprocessing (phase source) now require the use of the built-in preprocessor of RuleChecker/Astrée.
  • Enabling the new option cycl-simplify-switch causes the switch statement to be counted as a single decision when computing the CYCL metric. The new option is disabled by default.
  • RuleChecker now also checks input and output operands of extended asm statements (GCC language extension).

Rule sets and checks for C

  • Improved the check unused-macro. It now also reports macros that are defined using the following scheme:
    #ifndef M // this check is no longer considered a use of M
    #define M
    #endif
  • Removed the checks builtin-constant-p and builtin-sel in favor of the new check builtin-function (rule A.2.20) that warns about the use of all supported compiler builtin functions.
  • Added new informational diagnostic rules:
    • B.1.3 for detecting suppress directives that apply to a whole file or to more than a specific number of source lines.
    • B.1.4 for detecting comment directives that apply to a whole file or to more than a specific number of source lines.
  • Improved checks for the following rules:
    • CERT.MSC.12
    • CERT.MSC.40
    • M.1.1
    • M2012.1.1
    • M2012.2.2
  • Added support for the following CERT rules:
    • CERT.EXP.35
    • CERT.MSC.7
  • Added support for the CWE rule CWE.563.
  • Added support for the following MISRA rules:

    • M.2.1
    • M2012.22.1
    • M2012.22.3
    • M2012.22.4
    • M2012.22.6
    • M2012.17.5
    • M2012.D.1.1
    • M2012.D.2.1
    • M2012.D.3.1
    • M2012.D.4.2
    • M2012.D.4.3
    • M2012.D.4.5
    • M2012.D.4.13
    • M2012A1.D.4.14
    • M2012A1.21.13
    • M2012A1.21.17
    • M2012A1.21.18
    • M2012A1.21.20
    • M2012A1.22.7
    • M2012A1.22.8
    • M2012A1.22.9
    • M2012A1.22.10
  • Improvements for customer-specific rule sets:
    • The check compound-alignment (X.B.6.2, X.D.7.6.d) now handles if ... else if ... constructs as one entity. This means that each nested block in such an if else cascade is checked for being aligned with the first if instead of the closest preceding if.
    • The check compound-alignment (X.B.6.2, X.D.7.6.d) is now performed on original source code to avoid the impact of the preprocessor on indentation.
    • RuleChecker now supports the new customer-specific rule X.B.5.9.

Rule sets and checks for C++

MISRA C++

Added support for rule M2008.7.4.1.

AUTOSAR

Added support for the following AUTOSAR rules:

  • AUTOSAR.0.1.2A
  • AUTOSAR.2.13.6A
  • AUTOSAR.2.3.1A
  • AUTOSAR.3.3.2A
  • AUTOSAR.4.5.1A
  • AUTOSAR.5.1.1A
  • AUTOSAR.5.1.9A
  • AUTOSAR.5.3.1A
  • AUTOSAR 5.10.1A
  • AUTOSAR.6.5.2A
  • AUTOSAR.7.1.5A
  • AUTOSAR.7.2.1A
  • AUTOSAR.7.4.1M
  • AUTOSAR.8.2.1A
  • AUTOSAR.8.4.4A
  • AUTOSAR.8.4.5A
  • AUTOSAR.8.4.7A
  • AUTOSAR.8.5.4A
  • AUTOSAR.8.4.6A
  • AUTOSAR.12.8.2A
  • AUTOSAR.13.3.1A
  • AUTOSAR.18.9.2A

Enhancements, clarifications, refinements, and fixes

For rule checks on C code

  • Removed false positives for check parameter-missing-const (CERT.DCL.0, CERT.DCL.13, M.16.7, M2012.8.13), which warned about non-const pointer parameters even when passed to a function pointer call and the callee required them to be non-const.
  • Removed false positives for check assignment-to-non-modifiable-lvalue (A.1.7, CERT.EXP.40, CERT.MSC.40, M.1.1, M2012.1.1, X.E.5.2.2.1), which warned about assignments to struct types with flexible array members, which does not constitute a constraint violation.
  • Removed false positives for check uninitialized-local-read (CERT.EXP.33, CWE.456, CWE.457, CWE.665, CWE.824, CWE.908, ISO17961.uninitref, M.9.1, M2012.9.1).
  • Revised the handling of Astrée directives in rule checks related to side effects:
    • Variables in the directives __ASTREE_assert, __ASTREE_known_fact, and __ASTREE_known_range are now considered to be written by the directive statement.
    • This can cause new violations of the checks side-effect-in-logical-exp (M2012.13.5),
      side-effect-in-initializer-list (M2012.13.1),
      evaluation-order (A.4.1, CERT.EXP.10, CERT.EXP.30, M.12.2, M2012.1.3, M2012.13.2, X.A.5.34),
      evaluation-order-initializer (A.4.2, M2012.1.3, X.A.5.34),
      multiple-volatile-accesses (CERT.EXP.10, CERT.EXP.30, M.12.2, M2012.1.3, M2012.13.2),
      side-effect-in-conditional (X.E.5.2.1.2),
      logop-side-effect (CERT.EXP.2, M12.4), and
      for-loop-condition-sideeffect (M2012.14.2).
    • This possibly removes violations of the checks statement-sideeffect (M.14.2, CERT.MSC.12),
      expression-statement-pure (M2012.2.2, CWE.561), and
      expression-statement-dead (M2012.2.2, CWE.561).
  • Reverted the modification to treat variables in __ASTREE_volatile_input directives as volatile, introduced in the last intermediate release 20.10i b8841650.
  • Removed false positives for check essential-type-assign (M2012.10.3) which did use the wrong type for bit-fields of essentially Boolean type.
  • Fixed RuleChecker’s handling of __has_include_next and #include_next for uncommon mixtures of relative and absolute paths in the preprocessor configuration that previously lead to spurious parse errors.
  • Removed false negatives for check cast-implicit (X.A.5.44) which did not report integer conversion at switch conditions nor implicit conversions at case statements.
  • Removed false negatives for check unsigned-bitfield-promotion (X.E.5.2.1.1) which did not report integer promotion for the switch condition expression.
  • Fixed errors caused by #include directives using backslash as path separator.

For rule checks on C++ code

  • Removed false negatives for check undefined-extern on C++ (AUTOSAR.3.2.2M, AUTOSAR.3.2.4M, CERT-CPP.DCL.60, M2008.3.2.2, M2008.3.2.4) which did not warn about undefined variables introduced by explicit template instantiation, such as in
    /* template even providing a function body */
    template<class T> void f(T) {}
    /* explicit instantiation which does not create a definition */
    extern template void f<>(int);
  • Removed false positives for rule check implicitly-virtual-method (M2008.10.3.2), which did warn about out-of-line definitions of virtual methods.
  • Removed false positives for rule check implicit-virtual (AUTOSAR.10.3.1A), which did warn about out-of-line definitions of virtual methods.
  • Removed false positives of the check scattered-data-member-initialization (AUTOSAR.12.1.3A) that warned about constructor member initialization with non-constant constructor call as being constant.
  • Removed false negatives of the check scattered-data-member-initialization (AUTOSAR.12.1.3A) that did not warn about constant non-numeric member initialization in constructor, e.g. pointer initialization with nullptr.
  • Removed false positives for check non-pod-struct (AUTOSAR.11.0.1A) in templates.
  • Removed false negatives for check non-pod-struct (AUTOSAR.11.0.1A).
  • Removed false positives for check non-private-non-pod-field (AUTOSAR.11.0.1M, M2008.11.0.1) in templates.
  • Removed false positives of the checks
    • underlying-bitop-width (M2008.5.0.20, AUTOSAR.5.0.20M)
    • bitfield-signed-size (M2008.9.6.4, AUTOSAR.9.6.4M)
    • underlying-cvalue-conversion (M2008.5.0.3, AUTOSAR.5.0.3M)
    • underlying-signedness-cast (M2008.5.0.9, AUTOSAR.5.0.9M)
    • cvalue-float-int-cast (M2008.5.0.7, AUTOSAR.5.0.7M)
    • cvalue-int-float-cast (M2008.5.0.7, AUTOSAR.5.0.7M)
    • underlying-widening-cast-float (M2008.5.0.8, AUTOSAR.5.0.8M)
    • underlying-widening-cast-int (M2008.5.0.8, AUTOSAR.5.0.8M)
    within templates if the expressions under check depend on template parameters. The check now only reports actual violations in the respective template instantiations.
  • Removed false positives for check digraph-token (AUTOSAR.2.5.2A, M2008.2.5.1) for template parameters starting with :: (resulting in the character sequence <::).
  • Removed false positives for check definition-duplicate (AUTOSAR.3.2.2M, AUTOSAR.3.2.4M, M2008.3.2.2, M2008.3.2.4) which warned about inline variables of external linkage.
  • Removed false negatives for check scattered-data-member-initialization (rule AUTOSAR.12.1.3A). The check did not warn when fields were initialized to the same effective value using different initialization, e.g. for bool field; it did not report
    : field() // initialized with false
    vs.
    : field(false) // initialized with false.
  • The instantiations of generic lambda functions are now checked as well. This removes false negatives.
  • Checks involving generic parameters and functions in the sense of MISRA C++ 2008 now also consider template parameter packs. This is an extension of the relevant checks to modern C++11 features. Rules affected are M2008.14.5.1, M2008.14.5.2, M2008.14.5.3, AUTOSAR.14.5.3M.

New DAX version 1.12

  • The special tag <arxml-file> has been replaced by a <files/> list to enable specification of multiple ARXML files for AUTOSAR. For example:
    <autosar>
      <files>
        <file>f1.arxml</file>
        <file>f2.arxml</file>
      </files>
    </autosar>
  • Extended the <separate-function/> tag to enable expressing separate functions for different analysis phases and processes.
  • Added new <dax><base>PATH</base></dax> tag to configure the project base directory.
  • Added new environment variables A3_PROJECT_BASE_DIR, A3_PREPROCESS_BASE_DIR, and A3_CONFIG_BASE_DIR for use in DAX files.
    • A3_PREPROCESS_BASE_DIR corresponds to the former A3_GLOBAL_BASE_DIR variable, which is considered deprecated and will be removed in a future release.
    • A3_CONFIG_BASE_DIR corresponds to the former A3_BASE_DIR variable, which is considered deprecated and will be removed in a future release.

Windows support

This is the last release to officially support Windows 7. Future releases will require at least Windows 10.

JSON Compilation Database Importer

The new Compilation Database Importer tool allows to automatically extract a preprocessor configuration from a compile_commands.json file as generated by modern build systems like e.g. cmake. It is available via the Tools menu and via a new batch mode option. The extracted configuration can be exported into a .dax file or imported directly into the current analysis project.

Integration with dSPACE TargetLink

Fixed a syntax error in the generated directive for multidimensional output variables.

Integration with KEIL μVision

  • Improved preprocessor configuration extraction.
  • Added header files for ARM-specific intrinsics.
  • Rule checks are now restricted to the project folder.
  • Added the command line option --symbols %Y to make the compiler symbols available in RuleChecker projects.
  • The arm_compat.h header file is included automatically if ARMCLANG is used. This can be disabled using the command-line option --no-compat.

Eclipse plugin

  • Now automatically adding the wrapper file set by option config-file to the analysis project.
  • Now choosing the appropriate Astrée analyzer mode depending on the project nature (astree-cxx for C++ projects, astree for C projects).
  • The Eclipse plugin now allows stopping a running analysis.

Miscellaneous

  • Updated to LLVM/Clang 11 toolchain.
  • Improved compression speed and ratio for AAF files.
  • The new option space-overhead=n allows to configure the space overhead of the garbage collection during analysis runs.
  • The XML report file format has been updated to improve consistency and clarify the meaning of its entries. The modifications concern the tags <messages/>, <alarm_types/>, <alarm_categories/>, and their children. The following (simplified) example illustrates the changes. Here is the structure of these XML tags from previous releases:
    <messages>
      <alarm_message type="a21581" key="array_out_of_bounds" />
      <error_message type="a21541" key="error_analysis_stopped"/>
    </messages>
    <alarm_types>
      <alarm_type id="a21581" category_id="c2" class="A" key="array_out_of_bounds"/>
      <alarm_type id="a21541" category_id="c11" class="E" key="error_analysis_stopped"/>
    </alarm_types>
    <alarm_categories>
      <alarm_category id="c2">Invalid usage of pointers and arrays</alarm_category>
      <alarm_category id="c11">Errors</alarm_category>
    </alarm_categories>
    Here is the same example using the new structure:
    <findings>
      <finding kind="alarm" class="A" key="array_out_of_bounds"/>
      <finding kind="error" key="analysis_stopped"/>
    </findings>
    <finding_categories>
      <finding_category category_group_id="c2" finding_key="array_out_of_bounds" finding_kind="alarm" class="A"/>
      <finding_category category_group_id="c11" finding_key="analysis_stopped" finding_kind="error"/>
    </finding_categories>
    <category_groups>
      <category_group id="c2">Invalid usage of pointers and arrays</category_group>
      <category_group id="c11">Errors</category_group>
    </category_groups>
  • Improved and clarified the display of error messages.
    • Error message categories have been revised to clearly distinguish errors from the 4 different frontends, the 3 main error situations of the Astrée analyzer, and other, unspecified errors. The new error categories are:
      • frontend_clang
      • frontend_c
      • frontend_cxx
      • frontend_source
      • analysis_stopped
      • analysis_stopped_unexpectedly
      • analysis_ignored_directive
      • other
    • Error message categories are now also displayed in the analysis log and in the text report file.
  • Parser filters are now also available for C++.

Client GUI, batch mode, and report files

  • Added a new "project base directory" feature, serving as a global base directory for files and directories specified with relative paths. It can be configured in the "Information" view of the GUI and by the new <base> DAX tag in global scope (see also the release notes about DAX changes).
    The base directory in the preprocessing section can also extend the project base directory if specifying a relative path. In the GUI it has been renamed into "Preprocess base directory". Similarly, the base directory for a preprocessor configuration has been renamed into "Config base directory".
  • Batch mode no longer performs any preprocessing (not even for the C stub library) if the list of files to preprocess is empty. The new behavior is consistent with interactive analysis runs using the GUI.
  • Fixed an issue that caused the GUI's Overview to remain empty after analysis runs with fatal errors (e.g. preprocessing errors).
  • Improved the generation of alarm comments for multiple findings at once via the context menu of the Findings view. It now produces correct AAL syntax which can be properly imported back into the tool.
  • Fixed incomplete loading of large sets of parser filters and external declarations.
  • In Overview → Filter, the files to filter can now also be displayed hierarchically in a directory tree.
  • Restored the automatic loading of results into the GUI overviews when analyses terminate due to errors.
  • Fixed the known issue from intermediate release 20.10i b8841650. Fatal errors of analysis results imported from previous Astrée versions are now displayed again in the overviews of the GUI.
  • Increased contrast for alarm messages in dark mode.
  • When inserting an annotation via the GUI, the annotation is now immediately shown at the precise insertion location.
  • Fixed an issue that prevented the loading of original source code into the editor in case of different capitalization in line directives.
  • If the connection between client and a temporary server is interrupted, the client is now able to reconnect.

Server and server controller

  • A temporary loss of license server connection no longer stops all analysis servers and running analyses. Analysis servers automatically recover when the license server can be reached again. Analyses are only stopped if the license server is unavailable for more than 30 minutes.
  • The analysis server can now be configured to reject client connections from remote hosts, either by adding the command line option --block-remote-connections when starting the server, or by setting "Block connections from remote hosts" in the server controller.
  • The server now supports optional password constraints for users. Password constraints can be enabled and configured in the "User" tab of the server controller and via its new batch mode option --password-constraints.

Frontends and preprocessor

  • Added new analyzer built-in function __astree_eof() to implement the macro EOF.
  • The C and C++ frontends now report and discard all __ASTREE_volatile_input directives that refer to (parts of) variables that are already affected by a preceding __ASTREE_volatile_input directive.
  • C frontend:
    • Now accepting arbitrarily parenthesized expression as arguments for the analyzer built-in function __astree_va_start.
    • No longer rejecting pointer arithmetic with pointer to struct with flexible array member.
    • Improved function filters (patterns to ignore during parsing) to prevent interaction with the contents of comments placed in or after function declarations.
    • Added support for the following GCC builtin functions:
      • __builtin_huge_val
      • __builtin_huge_valf
      • __builtin_huge_vall
      • __builtin_inf
      • __builtin_inff
      • __builtin_infl
      • __builtin_isfinite
      • __builtin_isinf
      • __builtin_isnan
      • __builtin_nan
      • __builtin_nanf
      • __builtin_nanl
      • __builtin_nans
      • __builtin_nansf
      • __builtin_nansl
      • __builtin_expect
    • Added support for designating members of anonymous unions in initializers. For example, the following code is now accepted:
      typedef union { unsigned _v;  struct { unsigned v1:1; }; } ut;
      unsigned u = ((ut){.v1 = 1}._v);
    • The ABI option enum_preferred_size has been extended to accept a new value best corresponding to the Diab compiler's -Xenum-is-best option. The effect of the value smallest has been modified to correspond to the Diab compiler's -Xenum-is-small and the GCC compiler's -fshort-enums options. This modification may lead to differently sized enums for analyses configured to enum_preferred_size=smallest and enum_preferred_sign=unsigned. The new choices are more compatible with the majority of compilers. Users of the Diab compiler that use the -Xenum-is-best option should switch to enum_preferred_size=best.
  • C++ frontend:
    • Fixed an issue that could lead to missing code location information for Astrée alarm messages raised in lambda functions.
    • Removed unjustified error messages of the C++ frontend regarding assembler code.
    • The preprocessor macro NDEBUG is no longer implicitly defined.
  • Original C source frontend:
    • Improved the performance of the original source frontend's internal preprocessing stage.
    • Source comment directives are now always collected and applied, even if rule checks and metrics are disabled.

Stub libraries, ABIs, and compiler configurations

  • The C stub library now provides a macro for offsetof (mapping it to the analyzer built-in offsetof).
  • Added ABI for CompCert AArch64.
  • Updated support for built-in functions of the CompCert compiler.
  • Added a stub implementation for the __builtin_copysignf built-in function of the CompCert compiler.
  • Improved precision of the C library stub implementations for pow and powf.
  • Add implementations for tanh, tanhf, imaxabs, and llabs to the C stub library.

OS configuration

  • Added support for ARXML files generated by ETAS.
  • Added support for AUTOSAR projects in which the OS configuration is split among several ARXML files.
  • Improved the handling of trusted functions in AUTOSAR. Three new macros can be used in the preprocessor configuration to customize the generated data for trusted functions:
    • TRUSTED_FUNCTION_NAME
    • DEFINE_TRUSTED_FUNCTION
    • DEFINE_TRUSTED_FUNCTION_WRAPPER
    The use cases for the macros and their effects on the configuration are detailed in the user manual.

QSK improvements

  • Added DO-330 objectives 6.2.1ff to table of addressed DO-330 objectives in VTP document.
  • Restructured the QSK for the customer-specific rule set X.B. Removed obsolete customer-specific rule sets X.B.3 and X.B.4.

New test cases in the Astrée QSK

  • qk_abi_atomic_attributed_pointer_1, qk_abi_atomic_attributed_pointer_2, qk_abi_atomic_attributed_pointer_3
  • qk_alarm_memory_leak
  • qk_check_dead_assignment, qk_check_dead_initializer
  • qk_intrinsic_eof
  • qk_option_ais_export_source_location
  • qk_option_global_iteration_limit, qk_option_global_iteration_limit_per_phase
  • qk_option_warn_on_memory_leaks
  • qk_option_space_overhead
  • qk_rule_m2012_d_4_13

The test case qk_option_stopped_separate_context has been removed from the Astrée QSK.

New test cases in the RuleChecker QSK

  • qk_abi_atomic_attributed_pointer_1, qk_abi_atomic_attributed_pointer_2, qk_abi_atomic_attributed_pointer_3
  • qk_aal_insert_comment
  • qk_check_ambiguous_label, qk_check_ambiguous_ordinary, qk_check_ambiguous_member, qk_check_ambiguous_ordinary, qk_check_ambiguous_tag
  • qk_check_array_argument_size
  • qk_check_builtin_function
  • qk_check_catch_class_by_value
  • qk_check_chained_errno_function_calls
  • qk_check_closed_file_pointer_use
  • qk_check_commented_file
  • qk_check_cvalue_float_int_cast
  • qk_check_cvalue_int_float_cast
  • qk_check_dead_assignment
  • qk_check_dead_initializer
  • qk_check_early_catch_all
  • qk_check_embedded_directive
  • qk_check_enum_bitfield
  • qk_check_eof_small_int_comparison
  • qk_check_errno_test_after_wrong_call
  • qk_check_exception_handler_member_access
  • qk_check_exception_specification_mismatch
  • qk_check_function_documentation
  • qk_check_function_template_specialization_location
  • qk_check_implicitly_virtual_method
  • qk_check_inaccessible_external_object
  • qk_check_include_guard_missing
  • qk_check_invalidated_system_pointer_use
  • qk_check_library_reuse_define
  • qk_check_library_reuse_undef
  • qk_check_macro_expansion_expression
  • qk_check_main_function_catch_all
  • qk_check_max_commented_lines
  • qk_check_max_suppressed_lines
  • qk_check_multi_declaration
  • qk_check_non_dynamic_virtual_downcast
  • qk_check_non_private_non_pod_field
  • qk_check_polymorphic_downcast
  • qk_check_pragma_asm
  • qk_check_simultaneous_read_and_write_stream
  • qk_check_strcpy_limits
  • qk_check_stdlib_string_size
  • qk_check_stdlib_use_string_unbounded
  • qk_check_suppressed_file
  • qk_check_switch_into_try_catch
  • qk_check_temporary_object_modification
  • qk_check_throwing_empty_outside_catch
  • qk_check_underlying_cvalue_conversion
  • qk_check_underlying_narrowing_conversion
  • qk_check_underlying_widening_cast_int
  • qk_check_undocumented_asm
  • qk_check_unnamed_namespace_header
  • qk_check_untrusted_return_use
  • qk_check_using_declaration_header
  • qk_check_using_declaration_straddle
  • qk_check_using_directive_header
  • qk_check_using_directive_non_header
  • qk_check_write_to_read_only_stream
  • qk_intrinsic_eof
  • qk_option_cycl_simplify_switch
  • qk_option_space_overhead
  • qk_rule_autosar_0_1_2a
  • qk_rule_autosar_3_3_1a
  • qk_rule_autosar_3_9_3m
  • qk_rule_autosar_5_0_3m
  • qk_rule_autosar_5_0_6m
  • qk_rule_autosar_5_0_7m
  • qk_rule_autosar_5_0_8m
  • qk_rule_autosar_5_0_15m
  • qk_rule_autosar_5_2_2m
  • qk_rule_autosar_5_2_3m
  • qk_rule_autosar_6_6_2m
  • qk_rule_autosar_7_2_4a
  • qk_rule_autosar_7_3_3m
  • qk_rule_autosar_7_3_4m
  • qk_rule_autosar_7_3_6m
  • qk_rule_autosar_7_4_2m
  • qk_rule_autosar_8_0_1m
  • qk_rule_autosar_8_4_2a
  • qk_rule_autosar_11_0_1m
  • qk_rule_autosar_15_0_3m
  • qk_rule_autosar_15_3_3a
  • qk_rule_autosar_15_1_3m
  • qk_rule_autosar_15_3_3m
  • qk_rule_autosar_15_3_5a
  • qk_rule_autosar_15_3_7m
  • qk_rule_autosar_16_0_5m
  • qk_rule_autosar_16_0_6m
  • qk_rule_autosar_16_2_3m
  • qk_rule_autosar_16_3_1m
  • qk_rule_autosar_17_0_2m
  • qk_rule_autosar_18_0_4m
  • qk_rule_autosar_18_0_5m
  • qk_rule_b_1_3
  • qk_rule_b_1_4
  • qk_rule_cert_cpp_dcl_59
  • qk_rule_cert_cpp_err_53
  • qk_rule_cert_cpp_err_61
  • qk_rule_cert_cpp_msc_37c
  • qk_rule_cert_cpp_msc_52
  • qk_rule_cert_exp_35
  • qk_rule_cert_msc_7
  • qk_rule_cwe_563
  • qk_rule_m_2_1
  • qk_rule_m2008_3_3_1
  • qk_rule_m2008_3_9_3
  • qk_rule_m2008_5_0_3
  • qk_rule_m2008_5_0_6
  • qk_rule_m2008_5_0_7
  • qk_rule_m2008_5_0_8
  • qk_rule_m2008_5_0_15
  • qk_rule_m2008_5_2_2
  • qk_rule_m2008_5_2_3
  • qk_rule_m2008_6_6_2
  • qk_rule_m2008_7_3_3
  • qk_rule_m2008_7_3_4
  • qk_rule_m2008_7_3_5
  • qk_rule_m2008_7_3_6
  • qk_rule_m2008_7_4_2
  • qk_rule_m2008_8_0_1
  • qk_rule_m2008_8_4_3
  • qk_rule_m2008_8_5_3
  • qk_rule_m2008_9_6_3
  • qk_rule_m2008_10_3_2
  • qk_rule_m2008_11_0_1
  • qk_rule_m2008_14_7_3
  • qk_rule_m2008_15_0_3
  • qk_rule_m2008_15_1_3
  • qk_rule_m2008_15_3_2
  • qk_rule_m2008_15_3_3
  • qk_rule_m2008_15_3_5
  • qk_rule_m2008_15_3_7
  • qk_rule_m2008_16_0_5
  • qk_rule_m2008_16_0_6
  • qk_rule_m2008_16_2_2
  • qk_rule_m2008_16_2_3
  • qk_rule_m2008_16_3_1
  • qk_rule_m2008_17_0_2
  • qk_rule_m2008_18_0_4
  • qk_rule_m2008_18_0_5
  • qk_rule_m2012_d_1_1
  • qk_rule_m2012_d_2_1
  • qk_rule_m2012_d_3_1
  • qk_rule_m2012_d_4_2
  • qk_rule_m2012_d_4_3
  • qk_rule_m2012_d_4_5
  • qk_rule_m2012_d_4_13
  • qk_rule_m2012_17_5
  • qk_rule_m2012_22_1
  • qk_rule_m2012_22_3
  • qk_rule_m2012_22_4
  • qk_rule_m2012_22_6
  • qk_rule_m2012a1_d_4_14
  • qk_rule_m2012a1_21_13
  • qk_rule_m2012a1_21_17
  • qk_rule_m2012a1_21_18
  • qk_rule_m2012a1_21_20
  • qk_rule_m2012a1_22_7
  • qk_rule_m2012a1_22_8
  • qk_rule_m2012a1_22_9
  • qk_rule_m2012a1_22_10

The test cases qk_check_builtin_sel and qk_check_builtin_constant_p have been removed from the RuleChecker QSK.

RuleChecker QSK test case extended to C

qk_check_loose_asm

RuleChecker QSK test cases extended to C++

  • qk_check_backjump
  • qk_check_dangling_elsegroup
  • qk_check_enum_definition
  • qk_check_float_bits_from_pointer
  • qk_check_hash_macro_multiple
  • qk_check_include_time
  • qk_check_macro_parameter_parentheses
  • qk_check_pointer_arithmetic
  • qk_check_return_implicit