Release 3.8, 2020-11-16
New features
- Support
_Static_assert
from ISO C11. - Support
__builtin_constant_p
from GCC and Clang. - New port: x86 64 bits Windows with the Cygwin 64 environment. (configure with target
x86_64-cygwin
). - The following built-in functions are now available for all ports:
__builtin_sqrt
,__builtin_fabsf
, and all variants of__builtin_clz
and__builtin_ctz
. - Added
__builtin_fmin
and__builtin_fmax
for AArch64.
Removed features
- The x86 32 bits port is no longer supported under macOS.
Compiler internals
- Simpler translation of CompCert C casts used for their effects but not for their values.
- Known builtins whose results are unused are eliminated earlier.
- Improved error reporting for
++
and--
applied to pointers to incomplete types. - Improved error reporting for redefinitions and implicit definitions of built-in functions.
- Added formal semantics for some PowerPC built-ins.
The clightgen tool
- New
-canonical-idents
mode, selected by default, to change the way C identifiers are encoded as CompCert idents (positive numbers). In-canonical-idents
mode, a fixed one-to-one encoding is used so that the same identifier occurring in different compilation units encodes to the same number. - The
-short-idents
flag restores the previous encoding where C identifiers are consecutively numbered in order of appearance, causing the same identifier to have different numbers in different compilation units. - Removed the automatic translation of annotation builtins to Coq logical assertions, which was never used and possibly confusing.
Coq and OCaml development
- Compatibility with Coq 8.12.1, 8.12.0, 8.11.2, 8.11.1.
- Can use already-installed Flocq and MenhirLib libraries instead of their local copies (options
-use-external-Flocq
and-use-external-MenhirLib
to theconfigure
script). - Automatically build to OCaml bytecode on platforms where OCaml native-code compilation is not available.
- Install the
compcert.config
summary of configuration choices in the same directory as the Coq development. - Updated the list of dual-licensed source files.