- New builtin for tool coupling with ał which allows inserting AIS annotations in the original source code.
- Added JSON export of abstract ARM assembly.
- The dcc-based backend now supports the
-t option to be passed on to the assembler, preprocessor and linker.
Valex for ARM is now available, including the corresponding Qualification Support Kit.
- Improved strength reduction of unsigned comparisons
x ==u 0,
x !=u 0, etc.
- New inline heuristic
finline-functions-called-once that considers all static functions
called once for inlining into their caller even if they are not marked inline. If a call to a given
function is integrated, then the function is not output as assembler code in its own right.
- Unified emitting of constant literals in RISC-V, PowerPC and x86 backends.
- Improved error message for exhausted ELF code during instruction comparison.
- Improved and unified error diagnostics.
- More conservative value analysis of dubious comparisons such as
(uintptr_t) &global == 0x1234
which are undefined behavior in CompCert.
- Fixed scoping of variables declared within the first clause of a
- In the
symbol + ofs addressing modes of the x86_64 backend,
limit the range of
ofs in 64 bits.