The CompCert formally-verified C compiler
free
has well-defined semantics on blocks of size 0 (#509).sub
instruction was generated for Pallocframe
.memcpy
if option -fno-fpu
is given.-fstruct-return
, deprecated since release 2.6.intuition
tactic (#496 and more).git submodule init && git submodule update
to download it._Noreturn
on function definitions (but not declarations) was ignored sometimes.__builtin_va_end
was discarded, is now evaluated for its side effects.va_list
structure can get out of scope.wchar_t
exactly like the ABI says. On most platforms, CompCert was defining wchar_t
as signed int
, but it must be unsigned int
for AArch64-ELF and unsigned long
for PowerPC-EABI._Noreturn
on function definitions (but not declarations) was ignored sometimes.__builtin_va_end
was discarded, is now evaluated for its side effects.va_list
structure can get out of scope.wchar_t
exactly like the ABI says. On most platforms, CompCert was defining wchar_t
as signed int
, but it must be unsigned int
for AArch64-ELF and unsigned long
for PowerPC-EABI.switch
statements such as Duff's device. This is achieved via an optional, unverified code rewrite, activated by option -funstructured-switch
. (#459)u8"été"
or u32'❎'
.-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)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.-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..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)Tag_ABI_VFP
attribute (#461)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.||
, &&
expressions to make sure the generated Clight code is well typed and is not rejected later by ccomp
(#458).-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.goto
labels (#371) (by Pierre Nigron)Declare Scope
statements where appropriate, and re-enable the undeclared-scope
warning._Generic
expressions from ISO C11.int
but not with other integer types.T (*)()
and prototyped, zero-argument function pointer types T (*)(void)
in type casts (#431).T f() { ... }
, i.e. unprototyped but with no parameters. (Before, the warning would trigger only if parameters were declared.)__builtin_fmin
and __builtin_fmax
so that their NaN behavior is the one documented in the manual.\r\n
for end-of-lines (#434).# 0
line directive generated by some C preprocessors (#398).__SIZEOF_INT128__
macro that is predefined by some C preprocessors (#419).##
instead of #
to delimit comments (#399).'abc'
.
Multi-wide-character constants L'ab'
are now rejected, like GCC and Clang do.leaq
instructions (#407).__builtin_memcpy_aligned
in cases involving arguments that are stack addresses (#410, #412)rldic
, rldicl
, rldicr
), resulting in assertion failures later in the compiler.__compcert_i64*
helper runtime functions during the C2C pass, so that they are not visible during source elaboration.clightgen
tool-csyntax
to clightgen
) (contributed by Bart Jacobs; #404, #413).Global Set Asymmetric Patterns
by more local settings (#408).int
, provided they are no larger than 32 bits (#387)__builtin_unreachable
and __builtin_expect
(#394) (but these builtins are not used for optimization yet)-mandir
option (#382)const_data
on macOS).Pfcfi
, Pfcfiu
, Pfctiu
pseudo-instructions, expanding the corresponding int<->FP conversions during the selection pass instead.ld
and std
instructions were generated and rejected by the assembler..a
library archives (#380).$
notation for Clight identifiers to scope clight_scope
and submodule ClightNotations
, to avoid clashes with Ltac2's use of $
(#392).lia
tactic instead of omega
._Static_assert
from ISO C11.__builtin_constant_p
from GCC and Clang.x86_64-cygwin
).__builtin_sqrt
, __builtin_fabsf
, and all variants of __builtin_clz
and __builtin_ctz
.__builtin_fmin
and __builtin_fmax
for AArch64.++
and --
applied to pointers to incomplete types.-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.-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.-use-external-Flocq
and -use-external-MenhirLib
to the configure
script).compcert.config
summary of configuration choices in the same directory as the Coq development.extern
then implemented inline
remain extern
wchar_t
, not int
free(NULL)
float
arguments passed on stack are passed in 64-bit formatisel
instructionec_readonly
condition over external calls
(permissions can be dropped on read-only locations)if
/else
statements and a ? b : c
conditional expressions are compiled to branchless conditional move instructions, when supported by the target processor-Obranchless
, to favor the generation of branchless instruction sequences, even if probably slower than branches.__builtin_fsqrt
and __builtin_bswap*
have semantics.__builtin_sel(a,b,c)
. Similar to a ? b : c
but b
and c
are always evaluated, and a branchless conditional move instruction is produced if possible.double
and unsigned int
.__builtin_bswap64
is now available for all platforms._Complex
and _Imaginary
.void
parameters.__COMPCERT_MAJOR__
, __COMPCERT_MINOR__
, and __COMPCERT_VERSION__
with CompCert's version number. (#284)$(DESTDIR)
to the installation target. (#169)%eax
if int and %rax
if long).int * x, sz = sizeof(x);
). (#267)float
arguments to __builtin_annot
and __builtin_ais_annot
were uselessly promoted to type double
.switch
statements. (#285)-dprepro
, -dall
. (#298)-dclight
. (#314)