New features
- New builtin for tool coupling with a³ which allows inserting AIS annotations in the original source code.
- JSON export of abstract ARM assembly.
- New builtins for the PowerPC 32-/64-bit hybrid mode:
__builtin_mulhd (PowerPC instruction mulhd)__builtin_mulhdu (PowerPC instruction mulhdu)__builtin_read64_reversed (PowerPC instruction ldbrx)__builtin_write64_reversed (PowerPC instruction stdbrx)
- The
-t option of dcc for the Diab-based backend is now supported
and passed on to the assembler, preprocessor and linker.
Valex
Valex for ARM is now available, including the corresponding Qualification Support Kit.
Diagnostics
- Improved and unified error diagnostics.
- New diagnostics for:
- duplicated cases inside of switch statements
- usage of void as type for parameters
- empty typedefs and using
_Noreturn in typedefs
- incomplete array element types
- empty declarations in K&R functions
- assigning a volatile struct to a struct
- casts involving composite types as required by ISO standard
- static or extern variables defined inside a for statement
- comparing a pointer to complete and incomplete type
- Improved handling and diagnostics for the
auto storage class.
- Improved error messages for:
- exhausted ELF code during instruction comparison
- subtraction of arithmetic type and pointer
- Improved check for incomplete types in pointer subtraction.
- Added check for enums that have the same tag as composites.
- Empty enum declarations after nonempty enum definitions are accepted.
Other improvements
- 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.
Fixes
- New check for constant expression and redeclarations of static variables and functions.
- 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
for loop.
- For addressing modes
symbol + ofs in the 64-bit x86 backend, the range of ofs is limited to 24 bits.
- For
sizeof and _Alignof on expressions designating bit-fields, an error is triggered.
- Fixed initialization of anonymous bit-fields in structs.