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.

Valex

  • 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.

Fixes

  • 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.