Skip to content

Commit

Permalink
Second update for release 3.10
Browse files Browse the repository at this point in the history
  • Loading branch information
xavierleroy committed Nov 19, 2021
1 parent 2198a28 commit fd2a2a8
Showing 1 changed file with 6 additions and 4 deletions.
10 changes: 6 additions & 4 deletions Changelog
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand All @@ -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).
Expand Down

0 comments on commit fd2a2a8

Please sign in to comment.