CompCert release 22.04
- Bit fields in structs and unions that were previously implemented through
an unverified source-to-source translation are now handled in the formally-verified part of CompCert.
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.
- Added support for producing Csyntax abstract syntax instead of Clight abstract syntax
- Built-in functions for testing floating-point values are now available for all backends:
- Several built-in functions are now expanded in the formally verified part.
- For PowerPC and PowerPC VLE:
- For PowerPC:
- Improved assembler instruction selection for instructions
with immediates for PowerPC VLE.
- Improved diagnostics for struct arguments used when
-fstruct-passing is not given.
- Improved specification of the semantics of the built-ins
__builtin_fmin for x86.
- Enable selection optimization for single floating point values
for PowerPC VLE
- Stricter checking of multi-character constants
L'ab' are now rejected,
just like by GCC and Clang.
__SIZEOF_INT128__ to indicate that 128-bit integers
are not supported for 64-bit x86 targets.