github AbsInt/CompCert v3.1
CompCert 3.1

latest releases: v3.14, v3.13.1, v3.13...
6 years ago

Release 3.1, 2017-08-18

Major improvements

  • New port targeting the RISC-V architecture, in 32- and 64-bit modes.

  • Improved support for PowerPC 64 processors: use 64-bit registers and
    instructions for 64-bit integer arithmetic. Pointers remain 32 bits
    and the 32-bit ABI is still used.

Code generation and optimization

  • Optimize leaf functions in the PowerPC back-end.
    (Avoid reloading the return address from the stack.)
  • Avoid generating useless conditional branches for empty if/else statements.
  • Earlier elimination of redundant &*expr and *&expr addressings.
  • Improve utilization of addressing modes for volatile loads and stores.

Usability

  • Add options -finline / -fno-inline to control function inlining.
  • Removed the compilation of '.cm' files written in Cminor concrete syntax.
  • More precise warnings about missing function returns.
  • clightgen: add option "-normalize" to avoid memory loads deep inside
    expressions.

Bug fixing

  • Issue #179: clightgen produces wrong output for "switch" statements.
  • Issue #196: excessive proof times in .v files produced by clightgen.
  • Do not generate code for functions with "inline" specifier that are
    neither static nor extern, as per ISO C99.
  • Some line number information was missing for some goto labels and
    switch cases.
  • Issue #P16: illegal PowerPC asm generated for unsigned division after
    constant propagation.
  • Issue #P18: ARM addressing overflows caused by 1- underestimation of
    code size, causing mismanagement of constant pool, and 2- large stack
    frames where return address and back link are at offsets >= 4Kb.
  • Pass -no-pie flag to the x86 linker when -pie is the default.

Coq and Caml development

  • Support Coq 8.6.1.
  • Improve compatibility with Coq working version.
  • Always generate .merlin and _CoqProject files.

Don't miss a new CompCert release

NewReleases is sending notifications on new releases.