CompCert changelog
- More precise value analysis
- Improved
if-conversion heuristic
- Improved common subexpression elimination optimization
- New options
- Various improvements for ARM and PowerPC
- New Valex configuration
- Improved function prologue and epilogue code
- CFI directives for AArch64 and RISC-V
- Various improvements for ARM
- Improved common subexpression elimination for conditional operators
- Improved constant propagation
- Removed limit on the number of spilling rounds
- Support for Duff’s Device
- Support for Unicode character constants and string literals
- Improved instruction selection and register allocation for ARM/Thumb
- Support for C11
_Generic selection
- Improved if-conversion optimization
- Mergeable string and literal sections
- 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
- Extended inline assembly
- 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 a3
- 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
