Release 26.04 Astrée and RuleChecker

Astrée and RuleChecker Release 26.04

An HTML version of these release notes is available at
absint.com/releasenotes/astree/26.04

A video summary is available at
youtube.com/watch?v=iqTdNtoJjBU


Parallelization

To further speed up the analysis, the server-side parsing 
and checking for frontend-level rules for C
can now be distributed over multiple threads of execution. 
The level of parallelization can be controlled by:

* a new server-side option in the Server Controller
   
* the new server command line option --analyzer-parallelization

When working with --temp-server, the parallelization level 
is controlled by the client’s command line option -j.


Full support for dynamic memory allocation in concurrent programs

Astrée now supports dynamic memory allocation in concurrent programs
after the sequential phase. Memory blocks that are allocated in a process
do not become visible to other processes in the same phase, but may become
visible to later phases if not freed. A process can only free or 
reallocate memory blocks that it previously allocated.


Improved AAF handling

* Large AAF files are now loaded much faster.

* When working with diff comments, delta analysis, and incremental analysis,
  a new kind of much smaller AAF files can now be exported, containing only 
  the data needed by these features. The export is available via:

  * the new menu entry "Project" -> "Export" -> "AAF project (advanced)"
  * the new command line options --export-reduced-reference 
    and --export-skip-analysis-log


General improvements

* Improved the original source location mapping for findings
  that are reported in preprocessed C code. The associated 
  original source location is now column-precise when the internal 
  preprocessor is used. This affects the display of 
  original source locations in the GUI, the XML and SARIF reports,
  and in IDEs that use the Astrée LSP server.
  
* Improved computation and matching of pattern comments to achieve
  better matches after code modifications, in particular when working 
  with generated code. Pattern comments created with previous releases 
  are applied as before.
  
* Optimized storage space usage for analysis projects
  in the server data directory and in AAF exports.
  
* Improved networking performance,
  especially for connections with high latency.
  
* Revised the interpretation of relative locations in 
  __ASTREE_comment, __ASTREE_suppress, RULECHECKER_comment,
  and RULECHECKER_suppress directives:

  * negative offsets are now interpreted relative to the beginning
    of the directive (or enclosing comment)
  * positive offsets are interpreted relative to the end
    of the directive (or enclosing comment)

  This may affect the interpretation of:
  
  * existing source directives in comments with line breaks
  * directives referring to locations on the same line

* Symbolic links to files and directories are now displayed 
  and reported as given.
  
* Proven code statistics now include class A and C alarms
  that are raised already in the C frontend.
  
* After reporting a constant_out_of_range alarm, the analyzer
  no longer assumes the full range for the affected constant,
  but rather a constant value:

  * -∞ or +∞ for floats
  * the wrap-around value for integers
  
* With the default option keep-float-specials=no, casting 
  a too large double precision value to single precision 
  is no longer reported as conversion_overflow, 
  but as conversion_overflow_unpredictable.
  
* The State Machine domain now uses less memory
  when accumulating values for the states in loops
  and when joining if-then-else branches.
    

Improved precision

* The analysis is now more precise for:
 
  * reinterpretations between double-precision floats and 64-bit integers
  
  * right shifts followed by left shifts of the same amount

  * memcpy when the size argument is imprecise,
    or when copying to/from folded (smashed) variables

  * Boolean relations when comparing a Boolean value
    using the operators < or >

  * integer expressions of the form a * f + b * g
    when f, g > 0 and f + g is bounded

  * integer expressions of the form a * b / c
    when a ∈ (−∞, c]
    
  * float expressions of the form (a - b) / c
    when a, b ∈ [0, c]
    
  * float expressions of the form (x - x0) / (x1 - x0)
    when x0 ≤ x ≤ x1 

  * floating point scaling of integer variables, 
    e.g. in expressions like x * k + y * k
    where x, y are integer variables 
    and k is a floating-point constant power of 2
    
  * single-precision float comparisons, now ensuring that 
    the resulting values only contain floating point numbers 
    that can be represented in single precision
    
  * the initialization status of struct fields, 
    avoiding false alarms in specific circumstances

* Enabling the option build-taint-graph no longer reduces analysis precision 
  on code that involves dynamic memory allocation.

* Improved precision for:

  * __ASTREE_modify directives in global scope on statically folded arrays
  
  * the Symbolic domain with the option clamp-out-of-bound-array-index disabled


Improved analysis of C++ code (astree-cxx mode)

* The following features are now also available for C++:

  * the option exclude-complement-overflow
  * the directive __ASTREE_partition_merge_closest

* Misspecified constant arguments to __ASTREE_modify 
  and __ASTREE_known_range directives are now rejected 
  by the frontend (diagnostics rule A.5.1), rather than 
  triggering an error during the analysis.


Reached code statistics

* Unreachable consecutive statements and whole blocks 
  are now reported by a single entry in the “Reached code” 
  view and in the output of the list-not-reached option.

* Reached code statistics in analysis mode "astree" have been refined for:

  * GCC-style statement expressions
   (each nested statement is now considered individually)
   
  * Astrée directives that are irrelevant for the purpose
   (e.g. __ASTREE_octagon_pack)
   
* Goto labels are no longer counted as distinct statements 
  when computing reached code statistics on C code.


Alarms

* Alarms and errors reported in preprocessed C code and without 
  context information now display related macro expansion stacks, 
  if the affected code was expanded from macros.
  
* The following alarms now also list the first conflicting sub-component
  of the involved types if said types are not trivial (e.g. structs):

  * incompatible_parameter_type
  * check_incompatible_argument_type
  * check_incompatible_function_pointer_conversion
  * check_incompatible_object_pointer_conversion
  * check_memory_function_compatible
  * check_type_compatibility
  * check_type_compatibility_link

* invalid_float_argument alarms are now reported on casts 
  from float to double when the float value may be NaN or infinity
  and the option keep-float-specials is disabled.


Options

* Extra data required for later program slicing is now only written 
  if other features that rely on said data are enabled (e.g. export 
  of invariants). In all other cases, program slicing must be enabled 
  expressly by using the new option "enable-program-slicing=yes".
  Keeping the option disabled reduces disc space usage, memory consumption,
  and AAF file size.
  
* New options:

  * partition-boolean-interpolation
    detects and partitions assignments of the form

      flag * a + !flag * b
    
    to improve precision
    
  * partition-boolean-barycenter
    partitions Boolean variables (flags)
    that are used in Boolean barycentric expressions of the form

      (expr)/flag_sum

    where flag_sum is a variable corresponding to the sum of several 
    such Boolean flags
    
* The option dynamic-smash-variables-threshold is now deprecated
  and can be removed from existing analysis configurations.


Directives

* All forms of suppress and comment directives that apply to original
  source code now accept an optional "with_expansions" argument.
  Directives with this argument apply to code that is expanded 
  from the code addressed by the directive. 
  This allows commenting and suppressing alarms at macro-definition level:
  
  // RULECHECKER_comment(1:0, 1:0, with_expansions, rules_category, "ok", true)
     #define M ...non-compliant code...

  The above example creates comments for all rule violations 
  reported in any expansion of the macro M.

* __ASTREE_partition_merge_closest now also matches 
  __ASTREE_partition_control directives that are used 
  to partition Boolean assignments.

* __ASTREE_partition_control is now rejected with an invalid-directive alarm
  when introduced in front of a function call or non-Boolean assignment.
  Partitioning of function calls can instead be achieved by using
  the directive __ASTREE_partition_calls.
  
* __ASTREE_volatile_input now accepts the new keyword "non_volatile":

    __ASTREE_volatile_input((v; non_volatile));
    
  This specification cancels out the effect of the options 
  volatile-global=yes or volatile-auto=yes on the variable v. 
  It can be followed by additional __ASTREE_volatile_input directives 
  to specify parts of v that the analysis should still consider as volatile.
  
* __ASTREE_partition_ranges((v; max_partition=n)) 
  is no longer rejected as invalid if v is a float that can be NaN.
  Instead, the directive then introduces an (n+1)th partition 
  that contains all special values of v (i.e. NaN and/or ±∞).
  
* __ASTREE_smash_variables is now deprecated
  and can be removed from existing analysis configurations.
  This avoids confusion with the directive __ASTREE_smash_variable
 (without the “s”), which is still supported and can be kept.
 
* __ASTREE_print directives with string parameters 
  now output the special strings

  * "TOP" when the contents of the strings, 
     pointed to by the char* argument, are not precisely known,
  
  * "ERROR" when the dereference of the char pointer would raise an alarm.

  Moreover, such directives now raise an invalid_directive alarm 
  when the argument expression does not have a pointer type.

* Automatically inserted __ASTREE_partition_merge directives 
  for array index heuristics (analyzer options partition-array-access
  and aggressive-partition-array-access) are now reported 
  in the analyzer log and text report. This also removes 
  false alarms for the check ignored-partitioning (rule B.1.5).

* Optimized array access partitioning heuristics to prevent 
  high numbers of partitions in corner cases.


LSP Server

* The Single Translation Unit mode now ensures that dependent 
  translation units are always re-analyzed after changing a header file,
  regardless of the specific file paths supplied by the IDE.
  
* When settings related to the LSP server behavior
 (operation mode, project file override, and DAX file monitoring) 
  are changed in the VS Code integration,
  the LSP server now applies them automatically without restart.
  Changing settings related to launching the LSP server
  now only requires restarting the extension and the LSP server.


TargetLink integration

* Upper and lower bounds for scaled fixed-point values 
  in the Data Dictionary are now rounded towards zero 
  when used in automatically generated analysis directives.
  This behavior more accurately represents the TargetLink semantics.
  
* The toolbox now generates valid __ASTREE_assert directives
  for interpolation functions in which TargetLink uses boundary points
  instead of Nx/Ny parameters.
  
* The toolbox now generates additional __ASTREE_octagon_pack directives
  for index and table search functions to improve precision.


GitLab integration

Astrée can now be integrated with GitLab CI/CD
by including the corresponding component from the GitLab CI/CD catalog at:
gitlab.com/explore/catalog/absint/components

Further information is available in the release video at
youtube.com/watch?v=iqTdNtoJjBU


KEIL integration

Astrée and RuleChecker for C and C++
can now be integrated with ARM KEIL Studio.

Further information is available in the release video at
youtube.com/watch?v=iqTdNtoJjBU


JSON integration

The import of JSON compilation database files has been integrated into DAX
and enhanced by a mechanism for excluding user-specified files and directories
from the analysis. Imported information can also be extended by attributes 
in the same DAX file. The JSON import can still be executed in a separate step
before the DAX import. The corresponding option --compilation-database-to-dax 
now also accepts a DAX file as argument.


Fixes

* Fixed crashes related to the use of differently sized pointers
  in analyses using either separate functions or parallel processes 
  and precise-priorities=yes
  
* Calling the __astree_malloc intrinsic in a function in which 
  the control flow is partitioned multiple times before the call 
  no longer causes the analyzer to abort with an exception.
  
* Using the Equality or Filter domain while partitioning 
  with respect to two variables proven to be equal 
  could previously cause the analysis to stop with an error message.
  This issue has been fixed.
  
* When the condition of a loop or if statement contains 
  a logical operator followed by a function call 
  with a compound literal as argument, older releases could crash.
  This issue has been fixed.


General improvements to RuleChecker

* Constructor and destructor calls are now taken into account
  for control flow information, static call graph visualization,
  and threshold checks for relevant metrics such as CALLS, CALLING, and RPATH.
  
* Rule violations reported in preprocessed C code with different
  macro expansion stacks but identical original source code location 
  are now reported as multiple, distinct findings.
  
* RULECHECKER_comment, RULECHECKER_suppress, and RULECHECKER_attributes
  source directives can now be placed at any position in any comment,
  and multiple directives can now be added to the same comment.
  
* The option text-report-tables=control_flow
  is now also available in the standalone RuleChecker mode.

* In the ABI settings, intmax_t is now required 
  to have the same size as the largest configured integer type.
  
* Rule check configurations are no longer reported as erroneous
  for including rules that are disabled.
  
* Automatically inserted __ASTREE_partition_merge directives 
  for array index heuristics (analyzer options partition-array-access
  and aggressive-partition-array-access) are now reported 
  in the analyzer log and text report. This also removes false alarms
  for the check ignored-partitioning (rule B.1.5).


Rule sets and checks for C

* Added support for the following CERT rules:

  * CERT.EXP.0    * CERT.EXP.3    * CERT.EXP.7
  * CERT.EXP.8    * CERT.STR.11   * CERT.FIO.1
  * CERT.FIO.21   * CERT.PRE.2    * CERT.PRE.4
  * CERT.SIG.0    * CERT.DCL.3    * CERT.DCL.6
  * CERT.MSC.22   * CERT.MSC.23   * CERT.POS.44

* Improved coverage:

  * CERT.MSC.24 is now fully covered
  
  * M2023-C.D.4.12 and M2025-C.D.4.12 now also report uses of aligned_alloc
  
  * removed false negatives for M2023-C.21.3 and M2025-C.21.3, 
    for which the use of aligned_alloc was not reported
    

Rule sets and checks for C++

* Added support for rule M2023-CPP.8.14.1.

* Improved precision for all C++ rule sets, 
  removing false positives and false negatives across the board,
  by implementing the following changes.

  - Arguments of decltype are now considered as unevaluated in all cases.
  
  - Converting constructors are now properly considered in all cases.
  
  - Instantiated vs. not instantiated templates are now detected
    much more reliably, in particular:

    * not instantiated alias templates
    * not instantiated converting constructors
    * fully instantiated types of function declarations,
      notably w.r.t. expressions in noexcept exception specifiers
      and parameter declarations
    * enumerations that depend on parameters of an outer template
      but are defined outside of the template in which they appear
    * template (default) arguments that depend on other template parameters

* Elements of initializer lists are now checked in the (type) context
  of their usage, taking into account necessary implicit conversions 
  and object constructions. This removes false negatives for many rules.


Rule sets and checks specific to Astrée

* New check partition-merge-conflicts (B.1.5) 
  warns about potentially ill-formed sequences of partitioning directives,
  in particular when an __ASTREE_partition_merge_last directive 
  merges a partition that would otherwise be merged by a subsequent
  __ASTREE_partition_merge_closest directive.
  
* For analyses of C code, the check invalid-directive
  has been improved to additionally warn about directives 
  that involve an out-of-bound array access with index n 
  when the array is of size n.


Refinements for both C and C++ code

* To avoid highlighting unnecessarily large regions of source code in the GUI,
  the following checks are now reported with more specific code extents:

  * enum (X.A.3.9)
  
  * struct-type-incomplete (M.18.1)
  
  * compound-ifelse (AUTOSAR.6.4.1M, CERT.EXP.19, M.14.9, M2008.6.4.1,
    M2012.15.6, M2023-C.15.6, M2023-CPP.9.3.1, M2025-C.15.6, X.A.4.15)
    
  * switch-branch-termination (M2023-CPP.9.4.2)

* unreachable-code (AUTOSAR.0.1.1M, CERT.MSC.12, CWE.561, M.14.1,
  M2008.0.1.1, M2012.2.1, M2023-C.2.1, M2023-CPP.0.0.1, M2025-C.2.1, X.A.5.22)

  * is now reported only once for consecutive statements 
    and whole blocks that are unreachable
    
  * is no longer triggered by invalid directives that are
    already discarded by the frontend


Refinements for C code

* constant-expression-wrap-around
 (CERT.INT.30, M.12.11, M2012.12.4, M2023-C.12.4, M2025-C.12.4)
  no longer reports when a value is truncated upon conversion to unsigned.

* unused-macro (M2012.2.5, M2023-C.2.5, M2025-C.2.5) 
  is no longer triggered by macros from the preprocessor configuration
  that are actually used in the code.

* identifier-unique-extern (M.5.7, M2012.5.8, M2023-C.5.8, M2025-C.5.8) 
  is no longer thrown off by variables of external linkage that are
  present in both C and C++ files.

* macro-parameter-unparenthesized-expression
 (M2012.20.7, M2023-C.20.7, M2025-C.20.7) is no longer triggered 
  by macro instantiations that involve the member access operator "." 
  in both the macro parameters and the macro expansion.

* The mapping of preprocessed code to original source code
  has been fixed for the case that the preprocessor option
  keep-comments is enabled and the source code contains
  comments with Windows-style CRLF line endings.
  This also removes false positives for the following checks:
  
  * null-pointer-constant (M2012.11.9, M2023-C.11.9, M2025-C.11.9)
  * cast-implicit (X.A.5.44)
  * return-value-type (X.F.39) 

* The new and more precise mapping removes false negatives 
  for the following customer-specific rule checks.

  * compound-brace-line-end (X.F.3) 
    now takes into account code in macro parameters

  * multiple-instructions-per-line (X.F.1)
    now only considers instructions outside of macros
    or within the same macro definition

  * multiple-decls-per-line (X.F.1, X.F.29)
    * is now performed and reported directly on the original source code
    * also applies to declarations that are expanded by the preprocessor
      into the same logical line

  * statement-line (X.A.4.7, X.C.FOR.2)
    * is now performed and reported directly on the original source code
    * also applies to statements that are expanded by the preprocessor
      into the same logical line 
    * additionally reports when the body of a selection statement or loop
      is not placed on a separate line

* eof-small-int-comparison (CERT.FIO.34, CERT.INT.31, M2012A1.22.7, 
  M2023-C.22.7, M2025-C.22.7) no longer relies on the use of the deprecated
  analyzer-intrinsic function __astree_eof.

* uninitialized-local-read (CERT.EXP.33, CWE.456, CWE.457, CWE.665, CWE.824,
  CWE.908, ISO17961.uninitref, M.9.1, M2012.9.1, M2023-C.9.1, M2025-C.9.1)
  now includes the variable name in its alarm message.

* Macros such as UINT8_MAX from stdint.h (C standard library)
  are now considered to be:
  * of the essential type (MISRA-C 2012 and later), or
  * of the underlying type (MISRA-C 2004) as named by the macro 
   (uint8_t in case of UINT8_MAX).

* max-maintainable-code-lines (T.7.1) and 
  function-body-size (X.A.4.10, X.C.FOR.6) 
  have been extended to also report functions in preprocessed code 
  that does not contain line directives. The length of the function body
  is then measured on the preprocessed code.

* compound-indentation (X.B.6.3) is now also applied to original code
  and takes empty macro expansions into account.

* Fixed the reporting of check_unused_suppress_directives for unused 
  pattern comments, where the alarm message could previously point
  to an incorrect location.

* Fixed spurious errors triggered by switch statements with nested
  case/default labels.

* Improved reporting of the check constant-expression-wrap-around
 (CERT.INT.30, M.12.11, M2012.12.4, M2023-C.12.4, M2025-C.12.4).
  The alarm now states the value, type, and range of the affected expression.

* integer-overflow (CERT.INT.30, CERT.INT.32, CERT.INT.8, CWE.128, CWE.190,
  CWE.191, CWE.680, ISO17961.intoflow, X.A.5.35) is no longer reported
  in static initializers when the analyzer option 
  exclude-overflows-in-initializers is set.


Refinements for C++ code

* mutable-local-static (M2023-CPP.6.7.1) no longer reports 
  extern declarations at block scope. While the current wording of the rule
  implies that such a declaration constitutes a violation, MISRA clarified 
  that this is unintended and such code shall be out of scope for this rule.

* self-assignment-copy-move (M2023-CPP.15.8.1) now additionally recognizes

    { if (this == &rhs) { return *this; } ... }
    
  as a safe pattern to handle self-assignment.
  Violations are now only reported for fully instantiated templates.

* The following checks are no longer performed on functions defined
  within the scope of constructors/destructors (lambdas):

  * virtual-call-in-constructor
   (AUTOSAR.12.1.1M, CERT-CPP.OOP.50, M2008.12.1.1, M2023-CPP.15.1.1)

  * dynamic-cast-in-constructor
   (AUTOSAR.12.1.1M, M2008.12.1.1, M2023-CPP.15.1.1)

  * typeid-in-constructor
   (AUTOSAR.12.1.1M, M2008.12.1.1, M2023-CPP.15.1.1)

* The following checks no longer warn about unused variables 
  declared with the attribute [[maybe_unused]]:

  * unused-local-variable
   (AUTOSAR.0.1.3M, M2008.0.1.3, M2023-CPP.0.1.1, M2023-CPP.0.2.1)

  * unused-internal-variable
   (AUTOSAR.0.1.3M, M2008.0.1.3, M2023-CPP.0.2.1)

* Violations of the checks
  inappropriate-copy-signature-parameter (M2023-CPP.15.0.2) and
  inappropriate-move-signature-parameter (M2023-CPP.15.0.2) 
  are now only reported at the first declaration of an offending function.
  This removes duplicate violations at other redeclarations.
  
* Rule M2023-CPP.0.2.1 no longer includes the checks
  unused-parameter and unused-parameter-virtual.
  Parameters are not considered variables with limited visibility.
  
* conversion-from-bool (M2023-CPP.7.0.1)
  now allows bool to 1-bit bitfield conversions
  in member initializer lists and in-class initializers.
  
* unused-parameter
 (AUTOSAR.0.1.3M, AUTOSAR.0.1.4A, M2008.0.1.11, M2008.0.1.3, M2023-CPP.0.2.2) and
  unused-parameter-virtual
 (AUTOSAR.0.1.3M, AUTOSAR.0.1.5A, M2008.0.1.3, M2023-CPP.0.2.2)
  no longer report parameters in explicitly defaulted functions (= default).
  
* non-explicit-fundamental-constructor
 (AUTOSAR.12.1.4A, M2008.12.1.3, M2023-CPP.15.1.3) and
  non-explicit-non-fundamental-constructor
 (M2023-CPP.15.1.3)
  are no longer reported for uninstantiated templates.
  This removes false positives. Template instantiations are required 
  to determine whether a type is fundamental.


Client GUI, batch mode, and report files
 
* Increased the dialog size for editing annotations and comment alarms.

* The "Global data flow" and "Control flow" overviews now support 
  multiselection for more flexibility when filtering the associated 
 "Data flow" and "Control flow" views.

* The data flow overview table now also lists access paths
  to individual struct members and array elements/slices.
  This allows for a more fine-grained filtering of the “Data flow” view.
  
* In tooltips for postfix increment and decrement operators,
  the incremented value and the returned value are now displayed separately.
  
* Improved file synchronization when fixing findings using an external editor.

* Various improvements to the new Projects view introduced in release 25.10.

* DAX files containing an <aaf/> reference tag
  can now be imported when another project is already open in the GUI.

* AAL annotations that are generated by the GUI
 (e.g. inserted via the context menu in editor views)
  now always include the file name in order to avoid ambiguities.

* When importing a DAX file that contains both
 
  1. diff comments (<diff-comments/>) and
  
  2. a link to a reference AAF (<aaf/>)
     or reference analysis on the server (<id/>) 
     that also contains diff comments,

  the two sets of comments are no longer merged.
  Instead, the comments from the reference are now overwritten
  by those supplied in the DAX file.
  
  The same applies to projects that use the command line options 
  --aaf or --id rather than the corresponding DAX tags.
  
* Restored association of context information with <textline kind="cause"/>
  attributes in the XML report, as in releases up to 25.04i.


Server and Server Controller

Uploading data to the analysis server has been optimized.


Custom report files

* Improved location information for findings in original code.

* When files to ignore are specified, the information about reached code 
  is now more precise than before.

* New configuration options:

  * include-source-code 
    to include source code snippets for findings in the report

  * use-original-location 
    to report findings in the original rather than the preprocessed source code

  The new options can be specified in the corresponding DAX section as follows:

    <results include-source-code="yes|no" use-original-location="yes|no">
    
* Alarms about rule violations now include additional information. 
  Below is an example of such an alarm as it appears in the analyzer output
  and text report. The first line is now also included in custom report files.
  
    Size of statement 10 violates the limit of 9 (T.16.1) at …
    ALARM (R) check_max_size_of_statement: check failed (violates T.16.1) at …


Fixes

* Fixed an issue that could prevent further analysis runs 
  after modifying and saving several preprocessed files at once 
 (error message "Failed to initialize file mapping from files DB: 
  invalid file name").

* Fixed synchronization of the source-file lists in the sidebar 
  when accessing an analysis in read-only mode in one client 
  while it is being re-started by a different client.
  
* Fixed an issue that prevented the display of invariants 
  for lvalues in the Watch window.

  
Clang/LLVM frontend

Updated to Clang/LLVM version 21.


C frontend

* The analyzer-intrinsic function __astree_eof is now deprecated 
  and no longer used by the C library of the tool.
  This allows EOF to be a constant expression during preprocessing.

* Improved precision on rounding and removed duplicate alarms 
  for floating-point constant expressions in specific cases, 
  such as in initializers for objects with static or thread duration.
  
* Array (type) declarations are now rejected if the size of
  the array element type is not a multiple of its alignment.

* The mapping of preprocessed code to original source code 
  has been fixed for the case that the preprocessor option 
  keep-comments is enabled and the source code contains 
  comments with Windows-style CRLF line endings.
  
* Fixed frontend errors about incomplete types when using 
  the directive __ASTREE_import.


Stub libraries, ABIs, OS and compiler configurations

* The new ABI option flush_single_precision_to_zero (default is no)
  improves support for targets that flush subnormals to zero 
  on single-precision floating-point arithmetic operations.

* Added support for parsing code that contains
  CompCert’s __builtin_ais_annot.
  
* Configurable type sizes in the ABI settings are now limited
  to realistic values. For example, sizeof_int=5 cannot be specified
  in the GUI and is rejected when specified in DAX.

* The following restrictions on ABI settings are now enforced:

  * in mode astree-cxx or rulechecker,
    intmax_t is now required to have the same size 
    as the largest configured integer type
    
  * in mode astree-cxx,
    integer types of same size need to have the same alignment

  * in mode astree-cxx,
    floating-point types of same size need to have the same alignment

* Updated the memset implementation in the C stub library to avoid false alarms
  when running the analysis with the ABI setting char_sign=signed
  and the analyzer option warn-on-explicit-integer-cast-ranges=yes.

* Improved the C library stubs for malloc and calloc such that
  Astrée can now determine that no memory allocation is performed 
  in the error case (which returns a null pointer).

* Corrected the C library stub for realloc such that 
  dynamic memory allocation and the potential memory freeing is only performed
  in the success case (which returns a non-null pointer).

* Improved compatibility of built-in C library headers with respect
  to declarations of errno_t.

* constant_out_of_range alarms are no longer triggered by expressions
  provided by the following macros in the standard library stubs:

  * SIZE_MIN_MIN       * PTRDIFF_MIN_MIN     * WCHAR_MIN_MIN
  * CHAR16_MIN_MIN     * INTPTR_MIN_MIN      * WINT_MIN_MIN
  * CHAR32_MIN_MIN     * INTMAX_MIN_MIN      * SIG_ATOMIC_MIN_MIN

* When extracting ABI settings for GNU compilers, char signedness is now
  more accurately detected by the compilation database importer.

* ABI files for PowerPC targets now include the types defined in the standard 
  header files stddef.h, stdint.h, wchar.h, and signal.h.

* In the ABI files for x86, AMD64, ARM5, ARM6, and SPARC, 
  the option bitfield_sign has been changed to "signed",
  which is the default of mainstream compilers for these targets.

* The TriCore ABI now includes the new option
  flush_single_precision_to_zero=maybe.

* The abstract stub implementation of std::vector<..>::erase 
  no longer requires the first iterator argument to be dereferenceable
  when the range is empty.


Improved QSK performance

Superfluous tool runs for qk_check* tests have been removed
to speed up QSK execution.


New test cases in the Astrée QSK

* qk_abi_flush_single_precision_to_zero
* qk_check_csa_call_null_function_pointer
* qk_check_csa_null_dereference
* qk_check_csa_call_uninitialized_function_pointer
* qk_check_csa_call_uninitialized_object_pointer
* qk_check_csa_division_by_zero
* qk_check_csa_double_free
* qk_check_csa_null_reference_param
* qk_check_csa_stack_address_escape
* qk_check_csa_uninitialized_array_subscript
* qk_check_csa_uninitialized_assign
* qk_check_csa_uninitialized_binop_operand
* qk_check_csa_uninitialized_branch_condition
* qk_check_csa_uninitialized_object
* qk_check_csa_uninitialized_return
* qk_check_partition_merge_conflict
* qk_option_enable_program_slicing
* qk_option_partition_boolean_interpolation
* qk_option_partition_boolean_barycenter
* qk_check_pointer_arithmetic_function
* qk_check_pointer_arithmetic_incomplete
* qk_check_pointer_arithmetic_void
* qk_rule_cert_exp_8
* qk_rule_m2023_cpp_4_1_3
* qk_intrinsic_offsetof

The obsolete test cases
qk_intrinsic_eof,
qk_directive_smash_variables, and
qk_option_dynamic_smash_variables_threshold
have been removed from the Astrée QSK.


Astrée QSK test case extended to C++

* qk_directive_partition_merge_closest
* qk_option_exclude_complement_overflow
* qk_check_array_index_range
* qk_check_float_division_by_zero
* qk_check_int_division_by_zero
* qk_check_int_modulo_by_zero
* qk_check_int_undefined_modulo
* qk_check_invalid_function_pointer
* qk_check_invalid_pointer_arithmetics
* qk_check_left_shift_negative_first_argument
* qk_check_misaligned_dereference
* qk_check_offset_overflow
* qk_check_overflow_upon_dereference
* qk_check_undefined_extern
* qk_check_undefined_extern_pure_virtual
* qk_check_undefined_shift_width
* qk_check_uninitialized_variable_use
* qk_intrinsic_exit
* qk_intrinsic_malloc
* qk_intrinsic_memcpy


New test cases in the RuleChecker QSK

* qk_abi_flush_single_precision_to_zero
* qk_check_assert_invalid
* qk_check_assert_false
* qk_check_assert_with_constant
* qk_check_bad_header_filename
* qk_check_initializer_excess_string
* qk_check_macro_unparenthesized
* qk_check_malloc_size_struct
* qk_check_pointer_arithmetic_function
* qk_check_pointer_arithmetic_incomplete
* qk_check_pragma_operator_usage
* qk_check_precedence_math
* qk_check_precedence_pp_math
* qk_check_precedence_pp_remainder
* qk_check_precedence_remainder
* qk_check_string_size_explicit
* qk_check_termination_signal
* qk_check_unnamed_constant
* qk_directive_attributes
* qk_directive_attributes_source
* qk_rule_cert_dcl_6
* qk_rule_cert_dcl_23
* qk_rule_cert_exp_0
* qk_rule_cert_exp_3
* qk_rule_cert_exp_7
* qk_rule_cert_exp_8
* qk_rule_cert_fio_1
* qk_rule_cert_fio_21
* qk_rule_cert_msc_22
* qk_rule_cert_msc_23
* qk_rule_cert_pos_44
* qk_rule_cert_pre_2
* qk_rule_cert_pre_4
* qk_rule_cert_sig_0
* qk_rule_m2023_cpp_8_0_1
* qk_rule_m2023_cpp_19_6_1
* qk_rule_m2023_cpp_22_3_1

The obsolete test case qk_intrinsic_eof
has been removed from the RuleChecker QSK.


Customer-specific QSKs

* Each QSK package for a customer-specific rule set
 (X.A, X.B, X.E, X.F, and X.G) now contains an additional document 
  with the compliance matrix for said set, located at

    reports/a3c_compliance_<ruleset>.html

* The package for rule set X.B no longer includes the tests
  qk_check_pointer_arithmetic_function
  and qk_check_pointer_arithmetic_incomplete


------------------------------------------------------------------------
Last updated on 28 April 2026 by alex@absint.com. Copyright 2026 AbsInt.
------------------------------------------------------------------------

An HTML version of these release notes is available at
absint.com/releasenotes/astree/26.04

A video summary is available at
youtube.com/watch?v=iqTdNtoJjBU