CompCert 2.6

Release 2.6, 2015-12-21

Usability:

• Generation of full DWARF v2 debugging information in "-g" mode,
  including function-local variables. This is fully supported
  for the PowerPC target with GNU tools or Diab tools. Support
  for IA32 and ARM is nearly there.
• Production of detailed explanations for syntax errors during parsing.
  (Exploiting recent work by F. Pottier on the Menhir parser generator.)
• PowerPC port: added many new builtin functions.

Code generation and optimization:

• Support for PowerPC 64-bits (pointers are still 32-bit wide)
  and Freescale's E5500 variant.
• More prudent alias analysis for operations over pointers that are
  formally undefined, such as bit masking.
• New pass: Debugvar, to associate debug information to local variables.

Coq development:

• Richer representation of arguments and results to builtin operations.
• As a consequence, annotation builtins no longer need special handling.
• Added EF_debug builtins to transport debugging information throughout
  the compiler back-end.
• Upgraded the Flocq library to version 2.5.0.

Bug fixing:

• Issue #71: incorrect initialization of an array of wchar_t
• Corrected the handling of bit-fields of type _Bool and width > 1
• Removed copy optimization when returning a struct from a function.
• Full parsing of unprototyped (K&R-style) function definitions.
  (Before, the parsing was incomplete and would reject some definitions.)

Miscellaneous:

• The cchecklink tool (for a posteriori validation of assembly
  and linking) was removed. It is replaced by the Valex tool,
  available from AbsInt.
• Added a command-line option -conf to select
  a different compcert.ini configuration file.
• Removed the command-line options fstruct-passing=
  and -fstruct-return=, more confusing than useful.
• Added a command-line option -fstruct-passing that activates
  ABI-conformant by-value passing of structs and unions as
  function arguments or results. If this option is not set,
  passing a struct/union as function argument is now rejected.
• The -fstruct-return command-line option is deprecated and
  becomes a synonymous for -fstruct-passing.
• The return type of __builtin_clz() is int, as documented,
  and not unsigned int, as previously implemented.

CompCert 2.5

Release 2.5, 2015-06-12

Language features:

• Extended inline assembly in the style of GCC. (See section 6.5
  of the user's manual.) The implementation is not as complete
  as that of GCC or Clang. In particular, the only constraints
  supported over operands are "r" (register), "m" (memory), and
  "i" (integer immediate).

Code generation and optimization:

• Revised translation of '||' and '&&' to Clight so as to
  produce well-typed Clight code.
• More prudent value analysis of uninitialized declarations of
  "const" global variables.
• Revised handling of "common" global declarations, fixes an issue
  with uninitialized declarations of "const" global variables.

Improvements in confidence:

• Formalized the typing rules for CompCert C in Coq and verified
  a type-checker, which is used to produce the type annotations
  in CompCert C ASTs, rather than trusting the types produced by
  the Elab pass.
• Coq proof of correctness for the Unusedglob pass (elimination
  of unreferenced static global definitions). The Coq AST for
  compilation units now records which globals are static.
• More careful semantics of comparisons between a non-null pointer
  and the null pointer. The comparison is undefined if the non-null
  pointer is out of bounds.

Usability:

• Generation of DWARF v2 debugging information in "-g" mode.
  The information describes C types, global variables, functions,
  but not yet function-local variables. This is currently available
  only for the PowerPC/Diab target.
• Added command-line options to turn individual optimizations on or off,
  and a "-O0" option to turn them all off.
• Revised handling of arguments to __builtin_annot so that no code
  is generated for an argument that is a global variable or a local
  variable whose address is taken.
• In string and character literals, treat illegal escape sequences
  (e.g. "%" or "\0") as an error instead of a warning.
• Warn if floating-point literals overflow or underflow when converted
  to FP numbers.
• In "-g -S" mode, annotate the generated .s file with comments
  containing the C source code.
• Recognize and accept more of GCC's alternate keywords, e.g. signed,
  __volatile, etc.
• cchecklink: added option "-files-from" to read .sdump file names
  from a file or from standard input.

ABI conformance:

• Improved ABI conformance for passing values of struct or union types
  as function arguments or results. Full conformance is achieved on
  IA32/ELF, IA32/MacOSX, PowerPC/EABI, PowerPC/Linux, and ARM/EABI.
• Support the "va_arg" macro from <stdarg.h> in the case of arguments
  of struct or union types.

Coq development:

• In the CompCert C and Clight ASTs, struct and union types are now
  represented by name instead of by structure. A separate environment
  maps these names to struct/union definitions. This avoids
  bad algorithmic complexity of operations over structural types.
• Introduce symbol environments (type Senv.t) as a restricted view on
  global environments (type Genv.t).
• Upgraded the Flocq library to version 2.4.0.

Bug fixing:

• Issue #4: exponential behaviors with deeply-nested struct types.
• Issue #6: mismatch on the definition of wchar_t
• Issue #10: definition of composite type missing from the environment.
• Issue #13: improved handling of wide string literals
• Issue #15: variable-argument functions are not eligible for inlining.
• Issue #19: support empty "switch" statements
• Issue #20: ABI incompatibility wrt struct passing on IA32.
• Issue #28: missing type decay in __builtin_memcpy_aligned applied to arrays.
• Issue #42: emit error if "static" definition follows non-"static" declaration.
• Issue #44: OSX assembler does not recognize ".global" directive.
• Protect against redefinition of the __i64_xxx helper library functions.
• Revised handling of nonstandard attributes in C type compatibility check.
• Emit an error on "preprocessing numbers" that are invalid numerical literals.
• Added missing check for static redefinition following a non-static
  declaration.
• Added missing check for redefinition of a typedef as an ordinary
  identifier within the same scope.

Miscellaneous:

• When preprocessing with gcc or clang, use "-std=c99" mode to force
  C99 conformance.
• Use a Makefile instead of ocamlbuild to compile the OCaml code.