News
New features New function attribute alias for ELF targets, allowing to add weak aliases, i.e. alternate names for functions. New command line options to select data types implementing size_t and ptrdiff_t. Support for the Zicond RISC-V extension. New built-in functions RISC-V: __builtin_czero_eqz, __builtin_czero_nez AArch64: __builtin_mulhd, __builtin_mulhdu TriCore: __builtin_cadd, __builtin_csub General improvements Formally verified expansion of __builtin_mull. Faster compilation for programs containing composites with many members. More prudent handling of static names for string literals. Improved register selection for compressed instruction set. Improved diagnostics for duplicated case statements. Improved debug information for global variables. Backend-specific improvements Improved instruction selection for 64-bit arithmetic for 32-bit backends. Improved conditional move for ARM, RISC-V, and TriCore. Improved value analysis for TriCore. Improved branch relaxation for PowerPC. Improved Valex support for intermixed ARM/Thumb code. Hard-coded ISA selection for RISC-V has been removed from .ini files. Fixes The expansion of offsets for volatile load and store instructions has been reworked.
Learn more
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
Release 26.04 aiT, TimeWeaver, TimingProfiler, StackAnalyzer, ValueAnalyzer, EnergyAnalyzer
a³ 26.04 release notes An HTML version of these notes is available at absint.com/releasenotes/a3/26.04 A video summary is available at youtube.com/watch?v=rQmJIzzgohE New targets * TimeWeaver is now available for RISC-V. * aiT for TriCore now supports AURIX TC48x. * All tools for ARM and x86 now support the AdaCore GNAT Pro compiler for C, C++, and Ada. * All tools for AURIX now support the formally verified CompCert compiler. zlib-ng integration zlib-compressed input files are now read much faster. Documentation Improved description of the handling of denormalized floating point values for ARM and V850. GUI improvements * When searching graphs for addresses of memory reads/writes, precise hits are now ranked higher. * Improved display of additional information in Diff Viewer. * Minor visual tweaks to the Windows installer. Annotations * New functors: exists() Checks for existence of symbols, instructions, routines and loops. Can be used to guard the application of specific annotations, as an alternative to the "try" directive. Example: if (exists(symbol("CPUZ6"))) { area "MODE" contains data: 4; } The above will annotate the memory contents of the variable MODE if a symbol by the name of CPUZ6 exists. cast() Casts addresses to a specific type. Example: area (cast("Record", 0x400)."IntComp") contains data: 4; The above will tell the decoder to treat the object at address 0x400 as being of type "Record" and to annotate the memory contents of the structure field IntComp. * Improved resolving of complex area definitions. * Improved handling of assertion annotations. * Improved evaluation of expressions. Decoding * Improved handling of additional HEX files. * Improved resolving of virtual-function calls for classes with multiple inheritance. DWARF * Improved demangling of EDG template names. * Improved export of type information. All available typedefs found are exported now. * Improved handling of global type information and of duplicate routine symbols. * Improved extraction of type information and of data structures with many member variables or functions. TimingProfiler pipeline analysis * Write accesses to cached memory no longer burst-write a single cache line, but are performed as single write-throughs. * Improved handling of imprecise accesses to cached and uncached memory regions. Value analysis * Improved handling of infeasibility annotations. * Improved precision of the type domain. * Improved feasibility check for virtual function calls. ARM * Improved automatic switch table decoding for THUMB. * Improved pipeline analysis for Cortex-R by optimizing guard splits in local worst case. * Support for the AdaCore GNAT Pro compiler for C, C++, and Ada. PowerPC Support for denormalized floating-point values by accounting for possible normalization delays for e300, MPC7448(s), MPC755(s), and PPC750. RISC-V Support for the Zicond ISA extension. TriCore Support for the formally verified CompCert compiler. x86 * Support for moves to and from xmm registers (added by SSE). * Support for the AdaCore GNAT Pro compiler for C, C++, and Ada. TimeWeaver * A trace snippet that cannot be mapped to the control-flow graph now triggers a warning rather than an info message. * Improved handling of Lauterbach ASCII trace events. * Improved timestamp handling for Infineon MCDS DAS/TAB traces. TraceVisualizer * Improved extraction of multi-core traces. * Improved handling of unresolved computed control-flow transitions. Reporting Routines that take zero cycles but lie on the WCET path are now included in the XML report. Qualification Support Kits * New QSKs: * aiT for TMS320F2812 * aiT for TC387 * TimeWeaver for RISC-V * New compiler-specific QSKs: * StackAnalyzer for ARM with GCC 12.1.1 * StackAnalyzer for ARM AArch64 with GCC 9.4.0 * StackAnalyzer for C28x with TI 16.9.3.lts * aiT for ARM with GHS 2024.1.4 (ARM and THUMB) * Improved handling of license files that have both a generic and a specific derivate of the same architecture enabled. ------------------------------------------------------------------------ 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/a3/26.04 A video summary is available at youtube.com/watch?v=rQmJIzzgohE
Learn more
New Arm Product Updates Available
New Arm Product Updates Available The following products have been updated: Product Code Product Version ACOMP616 Arm Compiler for Embedded FuSa 6.16LTS r6p16-03rel0 This release adds download packages for Arm Certified C Library 6.16.A. It does not include any changes to the Arm Compiler for Embedded FuSa 6.16.3 toolchain, Arm Certified C++ Library 6.16LTS, or Arm Certified C Library 6.6.B download packages. Arm Compiler for Embedded FuSa 6.16.3 was released on 16 January 2026. It is a qualified release suitable for use for projects with functional safety or long-term maintenance requirements. For more information, see the Release Notes available via developer.arm.com/documentation.
Learn more
Cantata Now Available as a VS Code Extension
Hello Engineering Team, My name is Hrutik from the JORAL Engineering Team. QA Systems Cantata, a trusted solution for unit testing and code coverage, is now expanding its accessibility with a new Visual Studio Code extension. Known for helping teams automate testing, run efficient test execution, and generate clear diagnostic reports, Cantata helps development teams detect issues early and improve software quality with confidence. Just a quick note to let you know that Cantata is now available as an extension pack for Visual Studio Code. With this latest update, developers can now use Cantata directly within VS Code while still benefiting from the full functionality traditionally available in the Cantata IDE. This integration makes it easier for teams already working in VS Code to adopt Cantata without changing their workflow, improving efficiency and accessibility. To get started: Open Visual Studio Code Go to the Extensions tab Search for “Cantata” You should see a set of Cantata-related extensions—install the ones you need If you’d like to see how Cantata works within VS Code, I’ve included a short demo video for reference: 🎥 Cantata Visual Studio Code Extension Demohttps://www.youtube.com/watch?v=HClll6OWOWg&list=PL-3AenM-IauNUzUAE5SxDm1fboHdHobXr Feel free to reach out if you have any questions or would like a walkthrough. Hrutik Champaneri Field Application Engineer Email: hrutik.champaneri@joraltechnologies.com https://www.linkedin.com/in/hrutikchampaneri/ https://joraltechnologies.com/
Learn more
CompCert Qualification Achieved for Avionics Software
AbsInt is proud to announce that at the beginning of 2026 the CompCert compiler has officially been qualified for the Multi-Function Computer New Generation (MFC_NG) of ATR 42/72 aircrafts. For the first time, certification credits from compiler usage can be claimed for critical avionics software in compliance with DO-178C, DO-333, and DO-330. Successful qualification of CompCert for the Multi-Function Computer New Generation (MFC_NG) of ATR 42/72 aircrafts Claiming certification credits from a compiler allows applicants to eliminate, reduce, or automate specific objectives defined by DO-178C. The use of CompCert supports the objective of verifying property preservation between source and object code — even in the presence of compiler optimizations. As a result, test effort can be reduced. For example, formal verification performed at the source-code level can replace certain object-code testing activities otherwise required to demonstrate that the executable code complies with low-level requirements and maintains robustness. The AbsInt Qualification Support Kit further reduces certification effort and cost. It represents a major advancement in the qualification of compilers for avionics software at the highest assurance levels under DO-178C. CompCert is the first commercially available optimizing compiler to be formally verified. The machine code it generates is mathematically proven to conform exactly to the formal semantics of the source C program. CompCert supports multiple target architectures, including PowerPC, ARM, TriCore, RISC-V, and x86. In recognition of its groundbreaking formal proof, CompCert received the ACM Software System Award in 2021. It has been successfully deployed in commercial projects for many years and has also been qualified in safety-critical industry applications certified under IEC 60880. By adopting CompCert, organizations can achieve significant gains in application performance and development efficiency while reducing the risk of malfunctions due to miscompilation. If you have any questions, please do not hesitate to contact us.
Learn more
Canata 26.01 AI-Assisted Test Generation for Cantata
We hope you have had a good start to the new year! As promised, we are delighted to announce the release of Cantata 26.01, featuring the innovative AI-Assisted Test Generation and a new Visual Studio Code Extension Cantata 26.01 now available AI-Assisted Test Generation for Cantata Cantata 26.01 introduces the Cantata Test Automation Skill: a new integration that brings AI-assisted test generation into your Cantata workflow. By combining Cantata's proven testing framework with the capabilities of Claude Code (Anthropic's agentic coding tool), this skill enables developers to generate unit tests for C/C++ source code using natural language commands. Visual Studio Code Extension The new VS Code extension in Cantata 26.01 allows the creation of Cantata test scripts directly within the IDE, featuring a fresh new user interface and extensive configurability. To create a new test script, developers start by opening the test script configuration view. Within this interface, they can select the source files to be tested, define the script name, and configure other basic settings from the main configuration tab. Additional tabs provide more detailed controls, such as options for stubs and wrappers, while advanced customization is available through the extension settings for even greater control over the test script. Check out our demo videos on the new features Cantata AI-Assist Cantata VS Code Extensions Further technical details can be found here: Technical Note - Integration with Claude CodeCantata 26.01 Release Notes
Learn more
New Targets - StackAnalyzer for ARM 32-bit/LLVM/Clang-based compiler - StackAnalyzer for ARM 64-bit/LLVM/Clang-based compiler - StackAnalyzer for Infineon TriCore-AURIX/CompCert compiler - TimingProfiler by now support exactly the same targets as StackAnalyzer - TimeWeaver for Infineon TriCore-AURIX/CompCert compiler - aiT for Infineon TriCore-AURIX CPUs New QSKs - QSK for TimeWeaver for ARM 32-bit - QSK for StackAnalyzer for C28x - QSK for StackAnalyzer for MIPS
Learn more
Functional Safety in Automotive: ISO 26262 Testing Best Practices
Functional safety is a non-negotiable requirement in modern automotive software development. ISO 26262 provides the regulatory framework to ensure reliability and effective risk management across vehicle electronic and electrical (E/E) systems. To meet these demands, certified tools from QA Systems, Cantata and QA-MISRA, form the backbone of robust ISO 26262 testing strategies, enabling rigorous verification, automation, and full traceability for projects targeting Automotive Safety Integrity Levels (ASIL) up to D, the highest integrity tier for critical systems such as autonomous braking and airbag deployment. ISO 26262 Testing Principles ISO 26262 defines a structured, lifecycle-driven verification process that begins with hazard classification and ASIL determination and continues through: requirements definition and bidirectional traceability unit and integration testing fault injection and robustness testing structural and code coverage analysis For example, in Level 4 Autonomous Emergency Braking (AEB) systems, the lifecycle starts with item definition and Hazard Analysis and Risk Assessment (HARA), followed by measurable safety requirements mapped directly to verification activities. This disciplined approach has been critical in preventing failures such as unintended acceleration, incidents that historically led to major recalls and industry-wide safety reforms. QA Systems: Enabling ISO 26262 Compliance Cantata SGS-TÜV independently certified for use up to ASIL D, Cantata automates: unit and integration test generation branch and MC/DC structural coverage requirements-based testing fault-injection and robustness validation Cantata directly supports the confirmation review phase of ISO 26262, where independent assessors validate the effectiveness of implemented safety measures. QA-MISRA QA-MISRA complements Cantata by providing: automated static code analysis enforcement of MISRA C/C++ coding standards tool qualification kits for compliance reporting early detection of unsafe language constructs and resource usage Together, Cantata and QA-MISRA deliver a certified workflow that supports ISO 26262 requirements across all ASIL levels. Real-World Testing Examples Emergency Braking Systems (AEB): Automotive OEMs use Cantata to simulate sensor faults, actuator failures, and unexpected vehicle maneuvers, verifying that embedded software consistently responds within defined safety limits. QA-MISRA ensures the underlying ADAS codebase complies with MISRA rules to prevent undefined behavior before deployment. Electronic Throttle Control: In one documented case, ISO 26262 verification activities uncovered shortcomings in functional safety implementation, prompting revised software architectures and significantly strengthened validation processes. ISO 26262 Testing Best Practice To build a defensible functional safety case, automotive organisations should: establish bidirectional traceability between requirements, tests, and results adopt automation for regression, fault injection, and interface testing maintain comprehensive documentation using certified tools (Cantata and QA-MISRA) to streamline independent confirmation reviews integrate simulation methodologies (MIL, SIL, HIL) to validate fault behaviour and edge cases continuously update safety plans and audits to reflect new risks, technologies, and regulatory updates By combining these best practices with QA Systems’ proven toolsets, automotive teams can confidently meet ISO 26262 requirements, safeguard public trust, and protect road users against the evolving risks of embedded vehicle systems. Mapping QA Systems Tools to Unit, Integration, and System Testing QA Systems tools align precisely with the classic software testing pyramid: unit, integration, and system testing. Unit Testing Cantata is purpose-built for automated unit testing of embedded C and C++ software. It enables verification of individual functions or modules in isolation using: white-box testing techniques branch and MC/DC code coverage full requirements traceability Key capabilities include automatic test case generation, stubbing, and mocking, ensuring dependencies are controlled and each test focuses strictly on the logic under test, fully aligned with ISO 26262 expectations. Integration Testing Cantata extends seamlessly into integration testing by allowing multiple modules, subsystems, and APIs to be verified together. It supports: call interception and wrapping controlled fault injection interaction and interface validation This ensures that not only do individual components behave correctly in isolation, but that data flows, error handling, and interfaces remain robust, as required for ISO 26262 item integration. System Testing While Cantata focuses primarily on unit and integration levels, its outputs form the foundation of system-level qualification evidence. For full system validation: Cantata provides low-level dynamic test and coverage evidence QA-MISRA supplies coding-standard compliance evidence Both tools contribute traceable, auditable artefacts required for final system certification Together, they ensure that system-level safety is built on verified, standards-compliant software from the earliest phases of development. Summary Table Test Level Main QA-Systems Tool Capability Highlight Unit Testing Cantata Isolate modules, auto-generate tests, and coverage analysis Integration Testing Cantata Combine modules, wrap/call intercept, interface testing System Testing Cantata & QA-MISRA Evidence & compliance for system qualification Together, Cantata and QA-MISRA provide end-to-end ISO 26262 verification, from precise code-level correctness to system-level safety assurance with certification-ready evidence. © 2025 QA Systems. Published by JORAL Technologies.
Learn more
EMBEDDED IS EVERYWHERE
PRODUCTS
Manufacturers
Resource center