News
CompCert: Advancing Confidence in Safety-Critical Software Development
In the modern age where everything is run by software, the reliability of software toolchains plays a crucial role in safety critical industries such as aerospace, automotive and industrial applications. Traditional compilers are, although highly capable, can occasionally introduce miscompilation issues that may impact system behaviour in unexpected ways. This brings us to CompCert, which is the world's first commercially available formally verified optimizing C compiler, and is being qualified for its use in highly critical avionics applications at Airbus. Unlike conventional compilers that primarily rely on extensive testing, CompCert uses mathematical proofs to demonstrate semantic preservation, ensuring generated executable code behaves consistently with the original source code. By reducing the risks associated with compiler errors and while still maintaining optimization capabilities, this approach can help improve confidence and efficiency in software development workflows, reducing the time in verification in safety critical applications. As safety requirements continue to evolve, technologies like CompCert, which are backed by mathematical proof rather than testing alone, represent an important step toward building more reliable embedded systems. If you would like to evaluate CompCert or need any further information, please feel free to reach out to Robert Campbell at Robert.Campbell@joraltechnologies.com Qualifying CompCert for Safety-Critical Avionics Software - Click here to review the full article. Visit the CompCert Product Page
Learn more
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
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
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
Release 25.10 of AbsInt Tools for Safety-Critical Software Development
All Products =============== - The AbsInt Linux tools require now RHEL 9 or compatible and ship a Dockerfile creating a compatible Rocky Linux 9 container to facilitate deployment in containerized environments. aiT, TimingProfiler, StackAnalyzer, TimeWeaver ================================================== - NEW: aiT for TI TMS320F28386D/4D/8D - NEW: aiT for ATSAME51J18/19/20A - NEW: aiT for TMS570LC4357 rev B - Improved Project/Workspace Diff-Viewer, Sections View, and Symbols View - Enhanced analysis setup capabilities enable users to create new analysis projects more efficiently Astrée, RuleChecker ====================== - NEW: Delta analysis displays summary of differences between project revisions by tables and charts, and classifies alarms as new/old. - NEW: Astrée supports sound analysis of bounded recursions - Enhanced safety manual by DO-356A and ISO 21434 verification goal coverage - Enhanced VS-Code plugin (LSP server) by "single translation unit" mode, enabling faster rule checking - Improved rule coverage of CERT C/C++ and CWE CompCert ============ - NEW: CompCert for TriCore (1.6.x) - Improved optimizations for arithmetic runtime library functions - Generation of position-independent executables (PIE) and position-independent code (PIC) for AArch64, RISC-V and x86-64 Plugins ========= - AbsInt toolbox for TargetLink supports "diff" mode as default alarm comment mode. A complete list of all new features and improvements can be found here. You may watch a demonstration of selected new features on the AbsInt YouTube Channel.
Learn more
The first and only formally verified C compiler for safety-critical TriCore applications
CompCert for TriCore is a formally verified optimizing C compiler. Its intended use is compiling safety-critical software and meeting the highest levels of assurance. Can you trust your compiler? Compilers are complicated pieces of software that implement delicate algorithms. Bugs in compilers do occur and can cause incorrect executable code to be silently generated from a correct source program. In other words, a buggy compiler can insert bugs in the programs that it compiles. Time and again, studies have shown that many popular production compilers suffer from miscompilation issues. As early as in 1995, the authors of the Nullstone C conformance test suite reported [integer-division] defects in twelve of twenty commercially available compilers that were evaluated. A decade later, E. Eide and J. Regehr showed similar sloppiness in C compilers, this time concerning volatile memory accesses: We tested thirteen production-quality C compilers and, for each, found situations in which the compiler generated incorrect code for accessing volatile variables. This result is disturbing because it implies that embedded software and operating systems — both typically coded in C, both being bases for many mission-critical and safety-critical applications, and both relying on the correct translation of volatiles — may be being miscompiled. More recently, Regehr, Yang et al. generalized their testing of C compilers and, again, found many instances of miscompilation: We created a tool that generates random C programs, and then spent two and a half years using it to find compiler bugs. So far, we have reported more than 325 previously unknown bugs to compiler developers. Moreover, every compiler that we tested has been found to crash and also to silently generate wrong code when presented with valid inputs. What sets CompCert apart? CompCert is the only production compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues. The code it produces is proved to behave exactly as specified by the semantics of the source C program. Your benefits CompCert is a natural complement to any verification techniques that you apply at the source-code level — be it model checking, program proof, or static analyzers such as Astrée or RuleChecker. Only with CompCert can you guarantee that all the safety properties verified on the source code also hold for the generated machine code. CompCert supports verified separate compilation, enabling large-scale verification of complex software created by many different teams each working on C modules of their own. When using a conventional compiler to compile safety-critical applications, you typically have to disable compiler optimizations and run into resource problems as a result. With CompCert, you can significantly improve your applications’ performance, as you no longer have to switch off optimizations for safety reasons. Formally verified optimizations CompCert implements the following optimizations, all of them formally verified: Register allocation using graph coloring and iterated register coalescing Instruction selection with strength reduction Constant propagation for integer and floating-point types Common subexpression elimination Dead code elimination Redundant code elimination Function inlining Tail call elimination If-conversion Loop optimizations are currently not performed, but can be implemented on request. Compilation with execution time in mind On average, code generated by CompCert is: twice as fast as code generated by GCC without optimizations, only 10% slower than GCC code at optimization level 1, some 20% slower than GCC code at optimization level 3. Due to the lack of aggressive loop optimizations, performance is lower for code that involves many matrix computations. Ease-of-use and interoperability From command-line options to error messages to the handling of built-in functions, many CompCert features are very deliberately implemented to feel familiar and intuitive to GCC and LLVM users. Another express goal is to generate object code that respects the Application Binary Interface (ABI) of the target platform, and thus can be linked with object code and libraries compiled by other C compilers. In this, CompCert succeeds to a great extent, with some exceptions that are thoroughly documented. CompCert for TriCore is supported by the entire chain of AbsInt tools for safety-critical and mission-critical TriCore applications: Astrée for sound static analysis of your C code RuleChecker for proving compliance with MISRA, CERT, CWE, and other standards ValueAnalyzer for uncovering illegal accesses from within third-party object code StackAnalyzer for static analysis of the worst-case stack usage aiT for safe and precise static WCET analysis TimeWeaver for hybrid WCET analysis TimingProfiler for WCET estimates at early stages of software development © 2025 AbsInt. Published by JORAL Technologies.
Learn more
25.10 Release of AbsInt Tools for Safety-Critical Software Development
All tools =========== - The AbsInt Linux tools require now RHEL 9 or compatible and ship a Dockerfile creating a compatible Rocky Linux 9 container to facilitate deployment in containerized environments aiT, TimingProfiler, StackAnalyzer, TimeWeaver ================================================== - NEW: aiT for TI TMS320F28386D/4D/8D - NEW: aiT for ATSAME51J18/19/20A - NEW: aiT for TMS570LC4357 rev B - Improved Project/Workspace Diff-Viewer, Sections View and Symbols View - Enhanced analysis setup capabilities enable users to create new analysis projects more efficiently Astrée, RuleChecker ====================== - NEW: Delta analysis displays summary of differences between project revisions by tables and charts, and classifies alarms as new/old. - NEW: Astrée supports sound analysis of bounded recursions - Enhanced safety manual by DO-356A and ISO 21434 verification goal coverage - Enhanced VS-Code plugin (LSP server) by "single translation unit" mode, enabling faster rule checking - Improved rule coverage of CERT C/C++ and CWE CompCert ============ - NEW: CompCert for TriCore (1.6.x) - Improved optimizations for arithmetic runtime library functions - Generation of position-independent executables (PIE) and position-independent code (PIC) for AArch64, RISC-V and x86-64. Plugins ========= - AbsInt toolbox for TargetLink supports "diff" mode as default alarm comment mode
Learn more
PRODUCTS
Manufacturers
Resource center