diff options
| -rw-r--r-- | Changelog | 10 |
1 files changed, 6 insertions, 4 deletions
@@ -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). |