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 bitfield declarations and formal semantics for bitfield accesses. 
  The translation of bitfield 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.


------------------------------------------------------------------------------
Last updated on 27 April 2022 by alex@absint.com. Copyright 2022 AbsInt.
------------------------------------------------------------------------------
An HTML version of these release notes is available at
absint.com/releasenotes/compcert/22.04