From 2c47585b90858a6782b6e9a88efdb43368708429 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 29 Apr 2021 09:34:49 +0200 Subject: Update Changelog --- Changelog | 53 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) (limited to 'Changelog') diff --git a/Changelog b/Changelog index f86691a6..bda21a96 100644 --- a/Changelog +++ b/Changelog @@ -1,3 +1,56 @@ +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) + +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`). +- 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. + +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. + + Release 3.8, 2020-11-16 ======================= -- cgit From 19e1039a26b01297e19590340d7acb25a49b0560 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 8 May 2021 09:13:44 +0200 Subject: Update Changelog --- Changelog | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'Changelog') diff --git a/Changelog b/Changelog index bda21a96..2e14d2ca 100644 --- a/Changelog +++ b/Changelog @@ -2,6 +2,8 @@ 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 @@ -16,7 +18,7 @@ Usability: 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`). + 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, @@ -37,6 +39,9 @@ Bug fixing: 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` @@ -50,6 +55,11 @@ Coq development: - 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). + Release 3.8, 2020-11-16 ======================= -- cgit From 63ba4b55d198fb6a783256d6759887b31ca3d031 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 9 May 2021 18:10:08 +0200 Subject: Update Changelog for release 3.9 --- Changelog | 3 +++ 1 file changed, 3 insertions(+) (limited to 'Changelog') diff --git a/Changelog b/Changelog index 2e14d2ca..aa57a554 100644 --- a/Changelog +++ b/Changelog @@ -1,3 +1,6 @@ +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 -- cgit