CompCert release 22.04

New features

• 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 (option -csyntax to clightgen)
• Built-in functions for testing floating-point values are now available for all backends:
  • __builtin_isinf
  • __builtin_isinff
  • __builtin_isnan
  • __builtin_isnanf
  • __builtin_isfinite
  • __builtin_isfinitef

Improvements

• Several built-in functions are now expanded in the formally verified part.
  • For PowerPC and PowerPC VLE:
    • __builtin_mulhw
    • __builtin_mulhwu
    • __builtin_isel
    • __builtin_uisel
    • __builtin_bsel
  • For PowerPC:
    • __builtin_mulhd
    • __builtin_mulhdu
    • __builtin_isel64
    • __builtin_uisel64
• 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_fmax and __builtin_fmin for x86.
• Enable selection optimization for single floating point values for PowerPC VLE
• Stricter checking of multi-character constants 'abc'. Multi-wide-character constants L'ab' are now rejected, just like by GCC and Clang.
• Undefine __SIZEOF_INT128__ to indicate that 128-bit integers are not supported for 64-bit x86 targets.