Release CompCert 3.10 · AbsInt/CompCert

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.

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).

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.

x86 64 bits: overflow in offset of leaq instructions (#407).
AArch64, ARM, PowerPC, RISC-V: wrong expansion of __builtin_memcpy_aligned 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), 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.

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: 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.

Add support for producing Csyntax abstract syntax instead of Clight abstract syntax (option -csyntax to clightgen) (contributed by Bart Jacobs; #404, #413).