News
ARCHITECTURE OF TRUST: STRENGTHENING SECURITY IN MODERN CORTEX-M SYSTEMS
As embedded devices continue to expand into connected and safety-critical applications, security has become a fundamental design requirement rather than an optional feature. From industrial controllers and medical devices to automotive and IoT systems, developers must address increasingly sophisticated threats while maintaining performance and reliability. Modern Arm Cortex-M processors have evolved significantly to meet these challenges. While earlier Cortex-M architectures provided strong performance and low-power operation, newer generations introduce hardware enforced security features designed to protect software, data, and system resources from both accidental faults and malicious attacks. One of the most significant advancements is TrustZone for Arm Cortex-M, which enables the separation of applications into Secure and Non-Secure environments. By isolating sensitive assets such as cryptographic keys, authentication services, and security-critical firmware, TrustZone helps reduce the attack surface and limits the impact of compromised software components. Recent Cortex-M architectures further strengthen security through features such as Stack Limit Registers, PAN (Privileged Access Never), PXN (Privileged Execute Never), Pointer Authentication and Branch Target Identification (PACBTI), enhanced Memory Protection Unit (MPU) capabilities, and secure gateway mechanisms. Together, these technologies help mitigate common attack vectors including stack overflows, code injection, privilege escalation, control-flow hijacking, and cross-domain attacks. These hardware assisted protections are particularly valuable as embedded systems become increasingly connected and exposed to external threats. Security mechanisms that were once implemented primarily in software can now be enforced directly by the processor, improving both robustness and system resilience. As cybersecurity requirements continue to evolve, modern Cortex-M security features provide developers with practical tools to implement a defense in depth strategy. By combining hardware isolation, memory protection, privilege controls, and control-flow integrity mechanisms, organizations can build more secure and trustworthy embedded systems for the next generation of connected devices. To learn more about the security features discussed in this article, watch the full webinar here.
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
Safe and Efficient AUTOSAR Development with ISO 26262 Verification
AUTOSAR defines how software is structured. QA Systems tools prove that the software is safe. AUTOSAR provides a standardised software architecture that underpins much of today’s automotive ECU development. While it delivers structural consistency and standardised interfaces, functional safety certification is determined by how the underlying C/C++ software is verified and not by architecture alone. When combined with rigorous static and dynamic verification, it enables OEMs and Tier 1 suppliers to achieve ISO 26262-compliant, ASIL-aligned software verification across powertrain, chassis, ADAS, and software-defined vehicle platforms. Why AUTOSAR Alone Is Not Enough for ISO 26262 ISO 26262 compliance is achieved through rigorous software verification, regardless of whether a project uses Classic or Adaptive AUTOSAR. This includes: Mandatory coding-standard compliance Unit and integration testing Structural coverage, including MC/DC at higher ASILs Full traceability and audit-ready evidence This is where QA-MISRA and Cantata integrate directly into AUTOSAR workflows, providing the static and dynamic verification evidence required to support ISO 26262 safety cases. Where AUTOSAR Is Used in Safety-Critical Automotive Systems Classic AUTOSAR Domains: Powertrain ECUs (torque control, fuel injection, emissions) Braking, steering and chassis systems (ABS, ESC, EPB, steer-by-wire) Adaptive AUTOSAR Domains: ADAS and automated driving controllers (AEB, ACC, LKA) Software-defined vehicle platforms, OTA, V2X, EV energy management Modern vehicles often combine Classic ECUs for actuation with Adaptive controllers for perception and planning, creating end-to-end safety-critical chains from sensor to actuator. Using QA-MISRA in an AUTOSAR Workflow QA-MISRA provides static analysis and coding-standard enforcement aligned with ISO 26262 Part 6 for AUTOSAR software implementation. It analyses: MISRA C MISRA C++ AUTOSAR C++14 This ensures that BSW drivers, RTE glue code, and SWCs avoid undefined behaviour, data races, memory errors, and unsafe constructs. Typical QA-MISRA AUTOSAR Flow Generated and handwritten C/C++ is analysed in CI pipelines Project-specific rule profiles are derived from ASIL targets and HARA The QA-MISRA Tool Qualification Support Kit (QSK) provides ISO 26262 tool-confidence evidence Benefits: Reduced manual code reviews Early detection of integration regressions Consistent enforcement across multi-supplier AUTOSAR projects Using Cantata to Verify AUTOSAR Components Cantata provides ISO 26262-aligned dynamic unit and integration testing and is independently certified for use up to ASIL D. Typical Cantata Applications in AUTOSAR Unit testing of safety-critical SWCs (e.g. brake pressure control, steering assist, torque arbitration) Using RTE and BSW stubs to achieve: statement coverage branch coverage MC/DC coverage Integration testing of end-to-end safety chains (e.g. sensor fusion → motion control → brake/steering actuation) on target hardware Cantata’s TÜV certification and ISO 26262 qualification kits provide regulators with confidence that test results can be relied upon in the safety case. Bringing It All Together for Safety-Critical Projects A pragmatic and certifiable approach for safety-critical automotive development is: AUTOSAR → architectural backbone QA-MISRA → static verification & defect prevention Cantata → dynamic verification, coverage & regression AUTOSAR defines the structure. QA-MISRA and Cantata provide the verification evidence that the C/C++ implementation is robust, compliant, and tested to ASIL-appropriate coverage levels. AUTOSAR Classic vs Adaptive: How QA Systems Maps Across Both QA Systems tools operate horizontally across both Classic and Adaptive AUTOSAR. They do not replace AUTOSAR services, they verify the software that implements them. AUTOSAR Classic: Control-Centric ECUs Used for powertrain, chassis, airbags, EPS, and body ECUs. QA-MISRA enforces MISRA/AUTOSAR coding rules and provides ISO 26262 tool-qualification evidence Cantata performs unit and integration testing of SWCs and BSW using RTE/MCAL stubs, certified up to ASIL D AUTOSAR Adaptive: Service-Oriented Platforms Used for ADAS, central compute, connectivity, OTA, and domain controllers. QA-MISRA enforces safe C++ coding across complex Adaptive services Cantata validates safety-relevant shared libraries and services using structural coverage, regression testing, and fault-response validation Cross-Cutting ISO 26262 and Tool Qualification Classic and Adaptive AUTOSAR share the same ISO 26262 tool-qualification requirements. Cantata: TÜV-certified (ISO 26262 TCL 1, up to ASIL D) QA-MISRA: ISO 26262 Tool Qualification Support Kit Together they provide the complete tool-confidence argument required by OEMs and Tier 1 suppliers. Practical Mapping Summary Classic domain: powertrain, chassis, airbags, EPS → verify low-level C code with QA-MISRA + Cantata, apply MC/DC where required Adaptive domain: ADAS, central compute, connectivity, OTA → verify C/C++ services with QA-MISRA for defect prevention and Cantata for regression & safety-mechanism testing. © 2026 QA Systems. Published by JORAL Technologies.
Learn more
Embedded Debugging Tools: How Atlas Hardware Models with Arm DS IDE
If you’ve ever tried to validate embedded behavior in a virtual environment, you know the pain: you can observe what the system does, but the moment you need to interact with it—drive a pin high, simulate a button press, flick an LED on and off—you’re suddenly deep in custom tooling, rewrites, and one-off scripts.
That’s exactly where I started in a recent customer engagement bringing up their system in Corellium Atlas.
CoreModel is the set of interfaces which we use to virtualize peripherals. We already provide a coremodel-gpio example that could monitor GPIO pins. Great for visibility. Not enough for real testing. I needed true bidirectional GPIO control—the kind that lets you build realistic scenarios, poke the SoC like real hardware would, and keep iterating without restarting your app.
I used Kiro’s spec-driven development flow to go from a rough idea to production-quality C code fast.
What You’ll Learn in This Guide
How to build interactive digital twin sensors using Corellium Atlas
How to control GPIO inputs and outputs in a virtual environment
How to use AWS Kiro’s agentic AI to generate C code from specs
How to automate embedded system testing with CLI commands
How to simulate real hardware behavior without physical devices
Why bidirectional control is essential for firmware validation
How to speed up development with spec-driven design workflows
Here’s what that journey looked like—and why it changed the way I build low-level tooling.
Why GPIO Monitoring Isn’t Enough for Digital Twins
CoreModel is a C API library for remote peripheral interaction in Corellium virtual machines. It’s powerful, lean, and designed for serious systems work. But the GPIO example was limited to read-only behavior.
For my use case, that wasn’t just inconvenient—it was a blocker.
I needed to:
Drive GPIO pins at specific voltage levels (0–5V)
Monitor pins for real-time voltage changes
Switch modes on the fly during runtime
Control multiple pins at once
Test interactively using a CLI (not rebuild-run-repeat)
I wanted to create a real board’s behavior—LEDs, buttons, bidirectional handshakes—inside a Corellium Atlas i.MX93.
That meant writing a new example that fit CoreModel’s patterns, used its select-based event loop correctly, and handling errors accordingly.
Using Agentic AI to Accelerate Development with AWS Kiro
Traditional path:
Start coding
Hit unknowns
Redesign mid-flight
Refactor
Repeat until it works
I needed to accelerate the development of the working solution to quickly hit a timeline for when it would be implemented. I couldn’t sift through every single line of code just figure out how to connect the pieces of the API together.
Instead, I used Kiro’s spec feature.
Specs allowed me to move quickly through the problem in order:
What needs to exist
How it should work
What tasks get us there
Then code
Step-by-Step: Creating Spec-Driven GPIO Controls
That structured approach enabled me to be able to focus on delivery of a working solution faster than reading documentation and reviewing my code line by line.
Step 1: Requirements from the Spec
I had Kiro write a requirements spec that included:
5 clear user stories (output control, input monitoring, runtime commands, docs, error handling)
17 measurable acceptance criteria (so “done” was unambiguous)
Firm boundaries on scope (to produce a working MVP)
Kiro made these into clean, testable requirements. The biggest win wasn’t documentation—it was momentum. With these specific requirements, implementation became an easier direct task.
Step 2: Designs to take action on
With requirements done, Kiro guided a design doc that mapped cleanly to CoreModel’s structure:
Components: argument parser, GPIO manager, command handler, main loop integration
Data model: a simple gpio_config_t to track pin modes and voltage
API plan: using established CoreModel calls like coremodel_gpio_set() and coremodel_attach_gpio()
Error strategy: fail fast, clean up always, no leaks, no undefined behavior
The doc included ASCII diagrams and function signatures, so when coding began, Kiro could easily follow the blueprint it created.
Step 3: Automatic task breakdown
Then Kiro generated an implementation plan:
8 major tasks → 18 subtasksEach tied back to requirements.
With the tasks created, it was easy to follow the logic that Kiro used to build the code for the solution. It was clear what Kiro was working on and building on top of.
Real-Time CLI Testing and Event Handling
Once the tasks existed, the coding phase was the easiest part of the process.
1) Parsing mixed GPIO specs
The CLI had to support hybrid input/output configs like:
./coremodel-gpio-rw 10.10.0.3:1900 gpio1 0 1=3300 2 3=1800
Meaning:
pins 0 and 2 → inputs (monitoring)
pins 1 and 3 → outputs at 3.3V and 1.8V
Kiro helped me implement robust parsing with strict validation and clear user errors without having to worry about cumbersome argument handling.
2) Integrating stdin into CoreModel’s event loop
CoreModel uses select() for its event loop. I needed to extend it without breaking established flow.
The custom loop:
calls coremodel_preparefds()
adds stdin to the read set
handles both model events and interactive commands
supports clean shutdown from signals or quit
This was a subtle integration point—and the spec made it predictable.
3) Interactive runtime commands
The CLI supports:
set
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
EMBEDDED IS EVERYWHERE
PRODUCTS
Manufacturers
Resource center