Release 3.9, 2021-05-10
New features
- New port: AArch64 (ARM 64 bits, "Apple silicon") under macOS.
- Support bitfields of types other than
int
, provided they are no larger than 32 bits (#387) - Support
__builtin_unreachable
and__builtin_expect
(#394) (but these builtins are not used for optimization yet)
Optimizations
- Improved branch tunneling: optimized conditional branches can introduce further opportunities for tunneling, which are now taken into account.
Usability
- Pragmas within functions are now ignored (with a warning) instead of being lifted just before the function like in earlier versions.
- configure script: add
-mandir
option (#382)
Compiler internals
- Finer control of variable initialization in sections. Now we can put variables initialized with symbol addresses that need relocation in specific sections (e.g.
const_data
on macOS). - Support re-normalization of function parameters at function entry, as required by the AArch64/ELF ABI.
- PowerPC 64 bits: remove
Pfcfi
,Pfcfiu
,Pfctiu
pseudo-instructions, expanding the corresponding int<->FP conversions during the selection pass instead.
Bug fixing
- PowerPC 64 bits: incorrect
ld
andstd
instructions were generated and rejected by the assembler. - PowerPC: some variadic functions had the wrong position for their first variadic parameter.
- RISC-V: fix calling convention in the case of floating-point arguments that are passed in integer registers.
- AArch64: the default function alignment was incorrect, causing a warning from the LLVM assembler.
- Pick the correct archiver to build
.a
library archives (#380). - x86 32 bits: make sure functions returning structs and unions return the correct pointer in register EAX (#377).
- PowerPC, ARM, AArch64: updated the registers destroyed by asm pseudo-instructions and built-in functions.
- Remove spurious error on initialization of a local struct containing a flexible array member.
- Fixed bug in emulation of assignment to a volatile bit-field (#395).
The clightgen tool
- Move the
$
notation for Clight identifiers to scopeclight_scope
and submoduleClightNotations
, to avoid clashes with Ltac2's use of$
(#392).
Coq development
- Compatibility with Coq 8.12.2, 8.13.0, 8.13.1, 8.13.2.
- Compatibility with Menhir 20210419 and up.
- Oldest Coq version supported is now 8.9.0.
- Use the
lia
tactic instead ofomega
. - Updated the Flocq library to version 3.4.0.
Licensing and distribution
- Dual-licensed source files are now distributed under the LGPL version 2.1 (plus the Inria non-commercial license) instead of the GPL version 2 (plus the Inria non-commercial license).