diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-18 11:16:51 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-18 11:16:51 +0200 |
commit | 576d65e2570d114c2e25ac2e25de29d3889af06f (patch) | |
tree | 6c1fe955f78c1335635d3b890b1e5ff5f0cb3b6b | |
parent | ab6d5e98b4d967cc7834ad457b36bbf4c141f2ee (diff) | |
download | compcert-576d65e2570d114c2e25ac2e25de29d3889af06f.tar.gz compcert-576d65e2570d114c2e25ac2e25de29d3889af06f.zip |
Update Changelog in preparation for release 3.1
-rw-r--r-- | Changelog | 10 |
1 files changed, 8 insertions, 2 deletions
@@ -1,3 +1,6 @@ +Release 3.1, 2017-08-18 +======================= + Major improvements: - New port targeting the RISC-V architecture, in 32- and 64-bit modes. @@ -12,6 +15,7 @@ Code generation and optimization: (Avoid reloading the return address from the stack.) - Avoid generating useless conditional branches for empty if/else statements. - Earlier elimination of redundant `&*expr` and `*&expr` addressings. +- Improve utilization of addressing modes for volatile loads and stores. Usability: @@ -31,12 +35,14 @@ Bug fixing: switch cases. - Issue #P16: illegal PowerPC asm generated for unsigned division after constant propagation. -- Issue #P18: ARM PC-relative addressing of constant pool overflows - owing to underestimation of code size. +- Issue #P18: ARM addressing overflows caused by 1- underestimation of + code size, causing mismanagement of constant pool, and 2- large stack + frames where return address and back link are at offsets >= 4Kb. - Pass -no-pie flag to the x86 linker when -pie is the default. Coq and Caml development: +- Support Coq 8.6.1. - Improve compatibility with Coq working version. - Always generate .merlin and _CoqProject files. |