CompCert release 16.10
- 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.
- Added implementation for
__builtin_ctzll for ARM and PowerPC.
- CompCert now is able to read command line arguments from response files passed
@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
in the reference interpreter.