AbsInt/CompCert v3.16 on GitHub

Code generation and optimization

Extend neededness analysis to 64-bit integer operations, enabling more useless integer computations to be removed.
Extend common subexpression elimination (CSE) and dead code elimination to calls to known pure built-in functions and to known pure arithmetic helper functions.
Generation of position-independent code (PIC) for AArch64, RISC-V and x86-64 (option -fpic) (#551)
Generation of position-independent executables (PIE) for AArch64, RISC-V and x86-64 (option -fpie) (#551)
RISC-V: use PC-relative addressing instead of absolute addressing where possible (#550)
PowerPC and x86/ELF: put jump tables in .rodata section instead of .text section (#508)

Reject identifiers consisting of a single $ sign. This can cause errors with some assemblers, and is not ISO C.
Remove syntactic support for [*] array declarators, which was introduced in 3.15 (#539). They are usable only with variable-length arrays, which CompCert doesn't support.
Check that [static <size>] declarators occur only in function prototypes and only in outermost position, as prescribed by ISO C.
Fix corner case of designated initializers involving union with anonymous members.
Fix wrong lexing of #pragma directives that immediately follow a // single-line comment. (Affects only non-preprocessed .i input files; preprocessed .c files are not affected.)

Added warning dollar-in-identifier-extension for identifiers that contain $ signs. (This is not ISO C, just a popular extension.)
Revised handling of unknown warnings: -W<unknown warning> is now a warning instead of an error; -Wno-<unknown warning> is silently ignored (#554).
Added warning unknown-warning-option, so that warnings about unknown warnings can be ignored (-Wno-unknown-warning-option) or turned into an error (-Werror=unknown-warning-option) (#554).
Recognize option -shared and pass it to the linker.
Recognize options -pie and -no-pie and pass them to the linker.
Recognize options -MD and -MMD and pass them to the preprocessor.
On BSD platforms, use cc instead of gcc as the default preprocessor and linker.
On BSD platforms, add -z nobtcfi linker option. (This turns IBT/BTI off on OpenBSD, until it is properly supported by CompCert.)