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.