aboutsummaryrefslogtreecommitdiffstats
path: root/Changelog
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2021-11-19 10:30:11 +0100
committerXavier Leroy <xavier.leroy@college-de-france.fr>2021-11-19 10:30:11 +0100
commitfd2a2a8c8c2417b259e25a061c7fcfb6ee6f1848 (patch)
treed592bb7d827cedf9e61ee80319206ebe82f17c35 /Changelog
parent2198a280b1150a61be1e514f044da03e69a66af9 (diff)
downloadcompcert-kvx-fd2a2a8c8c2417b259e25a061c7fcfb6ee6f1848.tar.gz
compcert-kvx-fd2a2a8c8c2417b259e25a061c7fcfb6ee6f1848.zip
Second update for release 3.10
Diffstat (limited to 'Changelog')
-rw-r--r--Changelog10
1 files changed, 6 insertions, 4 deletions
diff --git a/Changelog b/Changelog
index f10285c7..94d85535 100644
--- a/Changelog
+++ b/Changelog
@@ -30,9 +30,10 @@ ISO C conformance:
Bug fixing:
- x86 64 bits: overflow in offset of `leaq` instructions (#407).
- AArch64, ARM, PowerPC, RISC-V: wrong expansion of `__builtin_memcpy_aligned`
- in some cases involving arguments that are stack addresses (#410, #412)
+ in cases involving arguments that are stack addresses (#410, #412)
- PowerPC 64 bits: wrong selection of 64-bit rotate-and-mask
- instructions (`rldic`, `rldicl`, `rldicr`).
+ instructions (`rldic`, `rldicl`, `rldicr`), resulting in assertion
+ failures later in the compiler.
- RISC-V: update the Asm semantics to reflect the fact that
register X1 is destroyed by some builtins.
@@ -42,13 +43,14 @@ Compiler internals:
improves performance.
- Add the ability to give formal semantics to numerical builtins
with small integer return types.
-- PowerPC port: share code for memory accesses between Asmgen and Asmexpand
+- PowerPC: share code for memory accesses between Asmgen and Asmexpand
- Declare `__compcert_i64*` helper runtime functions during the C2C
pass, so that they are not visible during source elaboration.
The clightgen tool:
- Add support for producing Csyntax abstract syntax instead of Clight
- abstract syntax (option `-csyntax` to `clightgen`) (#404, #413).
+ abstract syntax (option `-csyntax` to `clightgen`)
+ (contributed by Bart Jacobs; #404, #413).
Coq development:
- Added support for Coq 8.14 (#415).