CompCert Release 17.10

New features
● New command line option -finline to control inlining.
● New backend for hybrid 64-bit/32-bit PowerPC code.

● 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.

● 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 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.

● 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.

Prefixed the CompCert arithmetic helper functions with "__compcert".

Last modified on 18 October 2017 by Copyright 2017 AbsInt.
An HTML version of these release notes is available at