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
orx86_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 6.7.2.1, 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).
Usability:
- Added options
-W
xxx 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 typeint
, while the "section" attribute is attached to namep
.
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.