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 

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


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


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

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


▲ 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.
    <config name="My C files">
      <language>C <!-- Mandatory in DAX 1.10. -->

▲ 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">
  △ 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 

▲ 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 

▲ 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 Copyright 2020-2021 AbsInt.
An HTML version of these release notes is available at