Release 26.04 CompCert

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.