From db8a63f28efbdc3bcbe170320bef4102be3b13da Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 21 Nov 2022 11:32:00 +0100 Subject: [PATCH] Updates for release 3.12 --- Changelog | 53 +++++++++++++++++++++++++++++++++++++++++++++++++- VERSION | 2 +- doc/index.html | 2 +- 3 files changed, 54 insertions(+), 3 deletions(-) diff --git a/Changelog b/Changelog index c7d8d2f4e5..02a3dde1f4 100644 --- a/Changelog +++ b/Changelog @@ -1,6 +1,57 @@ +Release 3.12, 2022-11-25 +======================== + +New features: +- Support unstructured `switch` statements such as Duff's device. + This is achieved via an optional, unverified code rewrite, + activated by option `-funstructured-switch`. (#459) +- Support C11 Unicode string literals and character constants, + such as `u8"été"` or `u32'❎'`. + +Usability: +- Support the `-std=c99`, `-std=c11` and `-std=c18` option. + These options are passed to the preprocessor, helping it select the + correct version of the standard header files. It also controls + CompCert's warning for uses of C11 features. (#456) +- The source character set of CompCert is now officially Unicode + with UTF-8 encoding, A new warning `invalid-utf8` is triggered if byte + sequences that are not valid UTF-8 are found outside of comments. + Other source character sets and stricter validation can be supported + via the `-finput-charset` option, see next. +- If the GNU preprocessor is used, the source character set can be + selected with the `-finput-charset=` option. In particular, + `-finput-charset=utf8` checks that the source file is correctly + UTF-8 encoded, and `-finput-charset=ascii` that it contains no + Unicode characters at all. +- Support mergeable sections for string literals and for numerical constants. +- AArch64, ARM, RISC-V and x86 ELF targets: use `.data.rel.ro` section + for `const` data whose initializers contain relocatable addresses. + This is required by the LLVM linker and simplifies the work of the GNU linker. +- `configure` script: add option `-sharedir` to specify where to put + the `compcert.ini` configuration file (#450, #460) +- ARM 32 bits: emit appropriate `Tag_ABI_VFP` attribute (#461) + +Optimizations: +- Recognize more `if`-`else` statements that can be if-converted into + a conditional move. In particular, debug statements generated in + `-g` mode no longer prevent this conversion. + +Bug fixes: +- Revised simplification of nested conditional, `||`, `&&` expressions + to make sure the generated Clight code is well typed and is not rejected + later by `ccomp` (#458). +- In `-g` mode, when running under Windows, the `ccomp` executable could + fail on an uncaught exception while inserting lines of the source C file + as comments in the generated assembly file. +- Reintroduced DWARF debug information for bit fields in structs + (it was missing since 3.10). + Coq development: -- RTLgen: use the state and error monad for reserving goto labels (#371) +- RTLgen: use the state and error monad for reserving `goto` labels (#371) (by Pierre Nigron) +- Add `Declare Scope` statements where appropriate, and re-enable the + `undeclared-scope` warning. + Release 3.11, 2022-06-27 ======================== diff --git a/VERSION b/VERSION index c31ce8861e..a3233349b7 100644 --- a/VERSION +++ b/VERSION @@ -1,4 +1,4 @@ -version=3.11 +version=3.12 buildnr= tag= branch= diff --git a/doc/index.html b/doc/index.html index 10b30c3e9d..c3049344c8 100644 --- a/doc/index.html +++ b/doc/index.html @@ -25,7 +25,7 @@

The CompCert verified compiler

Commented Coq development

-

Version 3.11, 2022-06-27

+

Version 3.12, 2022-11-25

Introduction