News
How Static Analysis Supports DO-178C Verification
Developing software for airborne systems requires strong verification evidence, especially for higher-criticality applications. DO-178C defines objectives for airborne software development and verification, while DO-333 provides guidance for using formal methods as part of that process. Static analysis tools such as Astrée, aiT, StackAnalyzer, and RuleChecker can support several of these verification activities and help reduce the amount of manual effort required during certification. Where Static Analysis Helps Testing is essential, but some properties are difficult to demonstrate through testing alone. For example, proving that all relevant program paths and hardware conditions have been exercised can require significant effort. Sound static analysis based on Abstract Interpretation takes a different approach. Instead of relying on individual test executions, it analyzes an approximation of all possible program behaviors while keeping the result on the safe side. DO-333 recognizes Abstract Interpretation as a formal method, and AbsInt maps its analysis tools to several DO-178C/DO-333 verification objectives. The tools address different areas of verification: Astrée detects potential runtime errors such as overflows, invalid pointers, uninitialized variables, array access errors, and data-flow issues. aiT determines safe upper bounds for Worst-Case Execution Time (WCET). StackAnalyzer determines safe upper bounds for maximum stack usage. RuleChecker checks compliance with coding guidelines such as MISRA and other supported standards. Together, these tools can provide verification evidence for runtime behavior, timing, memory usage, control/data flow, and coding-standard compliance. Where the ROI Comes From The ROI is mainly found in two areas. First, static analysis can reduce verification effort. Determining WCET or stack usage through measurement may require extensive target testing and confidence that the worst-case program and hardware conditions were actually observed. Sound static analysis provides safe upper bounds by design, reducing dependence on exhaustive testing. Second, there is tool qualification effort. When verification tools are used to reduce or replace manual verification activities, qualification requirements may apply under DO-178C/DO-330. AbsInt provides Qualification Support Kits for aiT, Astrée, and StackAnalyzer to support this process and reduce the amount of qualification material a development team must create themselves. Bringing Verification Earlier into Development Static analysis is most valuable when it is used throughout development rather than only at the end of the certification process. Running these analyses early can help identify runtime errors, timing violations, stack problems, and coding-standard issues before they become expensive integration or certification problems. For teams working toward DO-178C compliance, static analysis therefore provides more than defect detection. It can become part of the verification strategy itself helping improve confidence in the software while reducing verification and qualification effort. Want to learn how these tools fit into a practical DO-178C workflow? Join us at our upcoming in-person event to explore how static analysis can support safety-critical software development and verification.
Learn more
Installing and Using AbsInt Astrée with Visual Studio Code
AbsInt Astrée can be integrated with Visual Studio Code using the A3C extension, allowing developers to run Astrée analysis and review detected alarms directly within the editor. Install and Configure A3C Open Visual Studio Code and press Ctrl + Shift + X. Search for the A3C / Astrée extension and install it. Configure the Astrée installation path if prompted. Open your C/C++ project folder in VS Code. Once configured, A3C connects VS Code with Astrée and can automatically start an analysis when a source file is opened. Running the Analysis For Single Translation Unit analysis, go to: Manage → Settings → Workspace → Extensions → A3C for C/C++ LSP Client Change the view from Full Project to Single Translation Unit. Now, when you open a source file, Astrée automatically starts the analysis. Opening another source file triggers a new analysis for that file. Detected alarms appear directly in the editor as red squiggly indicators, with additional information available in the Problems and Output panels. A single-click analyzes a file temporarily, while a double-click keeps the results available, allowing alarms from multiple files to be reviewed together. You may also see a .dax file at the top level of an Astrée project: Project/├── project.dax└── src/ ├── main.c ├── module1.c └── module2.c The .dax file is not source code. It contains the Astrée project/analysis configuration and defines how Astrée should analyze the source code. This is why it is typically kept at the project level rather than inside the source directory. See It in Action The complete workflow is also demonstrated at approximately the 26-minute mark of our webinar: Integrating AbsInt Static Analysis Tool with the KEIL Studio and using VS code
Learn more
VS Code and the Modern Embedded Workflow
Visual Studio Code has become a preferred development environment for many embedded software teams thanks to its flexibility, lightweight design, and extensive extension ecosystem. However, as embedded projects grow in complexity, writing code is only part of the challenge. Teams must also ensure software quality, compliance, test coverage, and verification while still meeting aggressive release schedules. The challenge is that many of these activities are still performed later in the development lifecycle, where defects become significantly more expensive to resolve. Industry studies have shown that software defects discovered during integration or system testing can cost up to 10x more to fix than those identified during development. For this reason, many organizations are shifting verification activities earlier in the software lifecycle to reduce project risk, improve quality, and avoid costly rework. Rather than forcing developers to abandon their preferred development environment, a modern VS Code-based workflow allows quality and verification activities to be integrated directly into day-to-day development. Developers can use Keil MDK to build and debug Arm Cortex-M applications while continuing to work within a familiar VS Code environment. Powered by Arm Compiler and the CMSIS ecosystem, Keil MDK provides optimized code generation, comprehensive device support, and advanced debugging capabilities specifically designed for Arm-based systems. This enables teams to accelerate development while building on a trusted toolchain widely used across safety, industrial, automotive, and IoT applications. Coding standards compliance is often another source of engineering effort, particularly for projects operating under safety, security, or regulatory requirements. QA MISRA helps identify coding standard violations as code is written, allowing issues to be corrected before formal reviews begin. Organizations that introduce coding standards verification earlier in development often report reduced review effort, improved code consistency, and fewer compliance related surprises during audits and certification activities. With the QA·MISRA extension integrated directly into VS Code, developers can identify violations and receive feedback within the editor, helping them address issues before they become larger development or compliance challenges. Static analysis provides another opportunity to identify defects before they become schedule impacting problems. AbsInt Astrée analysis tools help detect runtime anomalies, stack usage concerns, and software defects before code reaches target hardware. Finding issues during development rather than during integration testing can substantially reduce debugging effort while improving software reliability and reducing verification risk. Similar to QA MISRA, Astrée integrates with VS Code and highlights analysis results directly within the development environment, enabling engineers to identify and resolve issues earlier in the software lifecycle. Verification through testing remains equally important. QA Systems Cantata enables automated unit and integration testing for C and C++ applications, helping teams continuously verify functionality throughout development. Studies have shown that automated testing can reduce manual test execution effort by 30–50% while improving repeatability, coverage, and traceability. For organizations operating in regulated industries, automated testing also helps generate evidence required for standards such as ISO 26262, IEC 61508, IEC 62304, and DO-178C. With Cantata's VS Code integration, developers can generate test cases, execute tests, and review code coverage directly within their development environment, helping teams build quality into the software lifecycle from the start. Modern development workflows increasingly rely on CI/CD pipelines to improve efficiency, consistency, and software quality. VS Code integrates seamlessly with source control and automation platforms, making it easier to manage branches, reviews, builds, testing, and deployments. When combined with tools such as Keil MDK, QA·MISRA, AbsInt, and Cantata, teams can automate quality checks, compliance verification, static analysis, compilation, and testing throughout the development lifecycle. This unified workflow improves traceability, strengthens collaboration between development and quality teams, and helps identify issues earlier, reducing the risk of costly late-stage defects while providing greater confidence that software meets quality, security, and compliance requirements before release. Together, VS Code, Keil MDK, QA MISRA, AbsInt, and Cantata support multiple stages of the embedded software V-model from implementation and debugging through compliance, static analysis, testing, and verification. The result is not simply better tooling, but a more predictable development process, fewer escaped defects, reduced rework, and higher confidence in software quality before release. Interested in learning how these tools can fit into your development workflow? Reach out to Hrutik Champaneri at hrutik.champaneri@joraltechnologies.com to discuss your project requirements, compliance goals, or embedded software development challenges. Explore our VS Code Ecosystem page to discover tools for embedded development, static analysis, MISRA compliance, automated testing, and CI/CD integration, all within a modern VS Code workflow.
Learn more
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
EMBEDDED IS EVERYWHERE
PRODUCTS
Manufacturers
Resource center