First update for release 3.10

3 files changed, 57 insertions, 2 deletions

diff --git a/Changelog b/Changelog
index d3a4cc4b..f10285c7 100644
--- a/Changelog
+++ b/Changelog
@@ -1,5 +1,60 @@
+Release 3.10, 2021-11-19
+========================
+
+Major improvement:
+- Bit fields in structs and unions are now handled in the
+  formally-verified part of CompCert. (Before, they were being
+  implemented through an unverified source-to-source translation.)
+  The CompCert C and Clight languages provide abstract syntax for
+  bit-field declarations and formal semantics for bit-field accesses.
+  The translation of bit-field accesses to bit manipulations is
+  performed in the Cshmgen pass and proved correct.
+
+Usability:
+- The layout of bit-fields in memory now follows the ELF ABI
+  algorithm, improving ABI compatibility for the CompCert target
+  platforms that use ELF.
+- Handle the `# 0` line directive generated by some C preprocessors (#398).
+- Un-define the `__SIZEOF_INT128__` macro that is predefined by some C
+  preprocessors (#419).
+- macOS assembler: use `##` instead of `#` to delimit comments (#399).
+
+ISO C conformance:
+- Stricter checking of multi-character constants `'abc'`.
+  Multi-wide-character constants `L'ab'` are now rejected,
+  like GCC and Clang do.
+- Ignore (but still warn about) unnamed plain members of structs
+  and unions (#411).
+- Ignore unnamed bit fields when initializing unions.
+
+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)
+- PowerPC 64 bits: wrong selection of 64-bit rotate-and-mask
+  instructions (`rldic`, `rldicl`, `rldicr`).
+- RISC-V: update the Asm semantics to reflect the fact that
+  register X1 is destroyed by some builtins.
+
+Compiler internals:
+- The "PTree" data structure (binary tries) was reimplemented, using
+  a canonical representation that guarantees extensionality and
+  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
+- 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).
+
 Coq development:
+- Added support for Coq 8.14 (#415).
+- Added support for OCaml 4.13.
 - Updated the Flocq library to version 3.4.2.
+- Replaced `Global Set Asymmetric Patterns` by more local settings (#408).
 
 
 Release 3.9, 2021-05-10
diff --git a/VERSION b/VERSION
index 51212887..5f95604a 100644
--- a/VERSION
+++ b/VERSION
@@ -1,4 +1,4 @@
-version=3.9
+version=3.10
 buildnr=
 tag=
 branch=
diff --git a/doc/index.html b/doc/index.html
index c3912cb2..857457cb 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -25,7 +25,7 @@ a:active {color : Red; text-decoration : underline; }
 
 <H1 align="center">The CompCert verified compiler</H1>
 <H2 align="center">Commented Coq development</H2>
-<H3 align="center">Version 3.9, 2021-05-10</H3>
+<H3 align="center">Version 3.10, 2021-11-19</H3>
 
 <H2>Introduction</H2>