AbsInt/CompCert v3.14

CompCert 3.14

on GitHub

ISO C conformance

• free has well-defined semantics on blocks of size 0 (#509).

Code generation and optimization

• More simplifications of comparison operations and selection operations during the CSE pass.
• Replace selection operations with moves if both branches are equal.
• ARM 32 bits: several minor improvements to the generated code (#503 and more).

Bug fixes

• x86 under Windows: the wrong sub instruction was generated for Pallocframe.
• ARM: fix PC displacement overflow involving floating-point constants.
• ARM: fix error on printing of "s17" register.
• RISC-V: do not use 64-bit FP registers for memcpy if option -fno-fpu is given.

Usability

• Added generation of CFI debugging directives for AArch64 and RISC-V.
• Removed the command-line option -fstruct-return, deprecated since release 2.6.

Formal semantics

• The big-step semantics for Clight now supports the two models for function arguments (either as stack-allocated variables or as register-like temporaries).

Coq development

• Support Coq 8.17, 8.18, and 8.19.
• Revised most uses of the intuition tactic (#496 and more).
• Address most other deprecation warnings from Coq 8.18 and 8.19.
• Updated local copy of MenhirLib to version 20231231.
• Updated local copy of Flocq to version 4.1.4.

Distribution

• The small test suite was moved to a separate Git repository. Use git submodule init && git submodule update to download it.