CompCert changelog
- Support for C11
_Generic
selection
- Improved if-conversion optimization pass
- Support for mergeable string and literal sections
__builtin_nop
for all architectures
- Improved messages and warnings
- Formally verified handling of bitfields in structs and unions
- Support for producing Csyntax abstract syntax
- Support for non-integer bitfields
- Support for 32-bit PowerPC VLE with the NXP-GCC toolchain
- Improved ABI compatibility
- Improved diagnostics
- Additional and improved built-ins
- New built-in functions
- Improved diagnostics
- Support for
_Static_assert
- New architecture AArch64
- Improved error messages
- Improved DWARF support
- If-conversion optimization
- Improved built-in functions
- New diagnostics
- Improved attribute handling
- Improved scoping
- Improved DWARF handling
- Better handling of
_Alignof
/_Alignas
- Valex check for symbol placement
- New diagnostics
- New builtin for integration with ał
- JSON export of ARM assembly
- Valex for ARM
- New backend for hybrid 64-/32-bit PPC
- New compiler optimizations
- Qualification Support Kit for Valex
- Full support for C11 anonymous compound types
- Checks for unused variables and parameters
- Improved support for K&R, ARM and PowerPC
- Compatibility with coq v8.5pl2
- New options for GCC compatibility
- More built-in functions
- Various fixes
- Valex tool
- DWARF2 support
- New language features