@xavierleroy xavierleroy released this Feb 12, 2017 · 457 commits to master since this release

Assets 2

Release 3.0, 2017-02-10

Major improvements:

  • Added support for 64-bit target platforms, including pointers that are 64-bit wide, and the ability to use 64-bit integer registers and arithmetic operations. This support does not replace but comes in addition to CompCert's original support for 32-bit target platforms, with 32-bit pointers and emulation of 64-bit integer arithmetic using pairs of 32-bit integers. In terms of C data models, CompCert used to be restricted to the ILP32LL64 model; now it also supports I32LP64 and IL32LLP64.
  • The x86 port of CompCert was extended to produce x86-64 bit code in addition to the original x86-32 bit (IA32) code. (This is the first instantiation of the new support for 64-bit targets described above.) Support for x86-64 is currently available for Linux and MacOS X. (Run the configure script with x86_64-linux or x86_64-macosx.) This is an early port: several ABI incompatibilities remain.

Language features:

  • Support for anonymous structures and unions as members of structures or unions. (ISO C11, section, para 13 and 19.)
  • New built-in functions for ARM and PowerPC: __builtin_ctz, __builtin_ctzl, __builtin_ctzll (count trailing zeros, 32 and 64 bits).


  • Added options -Wxxx and -Wno-xxx (for various values of "xxx") to control which warnings are emitted.
  • Added options -Werror=xxx and -Wno-error=xxx (for various values of "xxx") to control which warnings are treated as errors.
  • Support response files where additional command-line arguments can be passed (syntax: @file).
  • Improved wording of warning and error messages.
  • Improved handling of attributes, distinguishing attributes that apply to types from attributes that apply to names. For example, in __attribute((aligned(8),section("foo"))) int * p; the "aligned" attribute is attached to type int, while the "section" attribute is attached to name p.

Code generation:

  • Support for ARM target processors in big-endian mode.
  • Optimize 64-bit integer division by constants.

Bug fixing:

  • Issue #155: on ARM, assembly errors caused by large jump tables for "switch" statements and overflow in accessing constant pools.
  • Issue #151: large inductive definition causes a fatal error in 32-bit versions of Coq.
  • Issue #143: handle %lf printf() format in the reference interpreter
  • Issue #138: struct declarations in K&R function parameters were ignored.
  • Issues #110, #111, #113, #114, #115, #119, #120, #121, #122, #123, #124, #125, #126, #127, #128, #129, #130, #133, #138, #144: various cases of internal errors and failed assertions that should have been proper errors instead.
  • For __builtin_memcpy_aligned, size and alignment arguments of 64-bit integer type were causing a fatal error on a 32-bit target.
  • ARM and x86 ports: wrong register allocation for some calls to function pointers.