CompCert release 17.10

New features

  • New command line option -finline to control inlining.
  • New backend for hybrid 64-bit–32-bit PowerPC code.

Valex

  • Qualification Support Kit for ISO 26262, DO-178B/C, and other safety standards.
  • Support for hybrid PowerPC port.
  • Inline assembler can now be skipped via the new configuration inline-asm.
  • More uniform printing of error messages.

Improvements

  • Now avoiding generation of useless conditional branches for empty if/else statements.
  • Removed reloading of the LR register in leaf functions for the PowerPC backend.
  • Early optimization of redundant *& and &* addressings.
  • Built-in arguments extended with a pointer addition operator. This enables more addressing modes to be encoded as built-in arguments, and to be used in conjunction with volatile memory accesses.
  • Reduced operator strength for 64-bit PowerPC instructions.
  • Unique error codes added for more error messages.
  • ARM in Thumb mode: simpler instruction sequence for branch through jump table.
  • Now using temporary files for objects if CompCert is used to compile and link.

Fixes

  • More strict check for modifiable lvalues.
  • No code is generated for non-static “inline definitions”.
  • Fixed crash for redefined composite with different tag.
  • Fixed assertion failure in register allocation for overflow in undefined address calculation.
  • Fix for illegal PowerPC asm generated for unsigned division after constant propagation.
  • Fixed issue with illegal assembly generated for function calls in large code blocks that use more than four floating-point arguments.
  • Overflow in ARM assembly addressing caused by large stack frames where return address and back link are at offsets ≥ 4kB.
  • Made sure that sizeof(long double) = sizeof(double) in all contexts to improve consistency in case the option -flongdouble is used.

Other

Prefixed the CompCert arithmetic helper functions with __compcert.