Skip to content

CompCert 3.9
Compare
Choose a tag to compare
@xavierleroy xavierleroy released this 10 May 08:14
· 212 commits to master since this release
v3.9
7b3bc19

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 and std 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 scope clight_scope and submodule ClightNotations, 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 of omega.
  • 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).
Assets 2