CompCert Release 16.10

General improvements
* CompCert is now compatible with coq v8.5pl2.

* The installer now offers a GUI to compile the runtime libraries
  for the provided target configurations.

* Improved support for K&R functions.

* Improved robustness of the frontend.
  More cases of invalid inputs are now treated with proper error messages.

* CompCert now produces colored diagnostic output.

* DW_AT_subrange_type is set for array sub ranges.

* Added support for empty variables (empty structs, arrays of size 0).

* Error messages are now numbered.

New features
* Added implementation for __builtin_ctz, __builtin_ctzl,
  and __builtin_ctzll for ARM and PowerPC.

* CompCert now is able to read command line arguments from response files
  passed via @file. The options read are inserted in place of the original
  @file option.
  If the file does not exist, or cannot be read, then the option will be
  treated literally, and not removed.
  Options in the file are separated by whitespaces. A whitespace character
  may be included in an option by enclosing the entire option in single
  or double quotes. Any character, including a backslash, may be used
  if escaped with a backslash.
  The file may itself contain additional @file options; any such options
  will be processed recursively.

* New command line options for more control of diagnostic output of CompCert.
  It is now possible to activate or suppress certain warnings,
  or additionally mark them as errors.

* CompCert now supports usage of anonymous composite types
  and allows accessing the named parts of the composite.

* Fixed internal error that prevents compilation of __builtin_clzll for ia32.

* Fixed known issue concerning block scope variables with external linkage.

* Fixed the return value of the emulated printf in the reference interpreter.

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