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.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
  * M2012.17.5
  * M2012A1.21.13
  * M2012A1.21.17
  * M2012A1.21.18
  * M2012A1.21.20
  * M2012.22.1
  * M2012.22.3
  * M2012.22.4
  * M2012.22.6
  * 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++

* Added support for MISRA C++ rule M2008.7.4.1.

* 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 negatives for check non-pod-struct (AUTOSAR.11.0.1A).
* Removed false positives for the checks non-pod-struct (AUTOSAR.11.0.1A) 
  and 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>&lr;/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.

Integration with Eclipse
* The Eclipse plugin now automatically adds the wrapper file 
  set by option config-file to the analysis project.
* The Eclipse plugin now chooses the appropriate Astrée analyzer mode 
  depending on the project nature (astree-cxx for C++ projects, astree for C projects).
* The Eclipse Plug-in allows to stop 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


------------------------------------------------------------------------------
Last updated on 10 May 2021 by alex@absint.com. Copyright 2021 AbsInt.
------------------------------------------------------------------------------
An HTML version of these release notes is available at
absint.com/releasenotes/astree/21.04