CompCert release 17.04

New features

  • Full support for C11 anonymous compound types.
  • Support for the attribute noinline to prevent functions from inlining.
  • Checks for unused variables and parameters. Support for the attribute unused to suppress the warning.

New options

  • -w
    disables all warnings
  • -fmax-errors
    limits the number of errors that are reported before the compilation is aborted
  • -f(no-)diagnostics-show-option
    controls whether the [-Woption] is printed in the diagnostic message for mappable warnings/errors
  • -fdiagnostics-format
    allows to switch between the three different format versions ccomp, vi and msvc
  • -g<level>
    replaces the old option -gdepth

General improvements

  • New warning for inline assembler in files compiled with -sdump.
  • Support for question mark and asterisk wildcards under Windows.
  • Implementation of the offsetof macro via a builtin function that is evaluated to the offset at compile time.
  • Improved handling of attributes, now distinguishing attributes that apply to types from those that apply to names.
  • Improved precision for warnings related to function returns.
  • New warning for unknown attributes.


Fixed wrong argument check for dcbtls and ibctls.

Other fixes and changes

  • Fixed issue with non-working debug information for compilation of multiple C files.
  • Fixed wrong prefix for deactivating warnings.
  • Fixed bug in generation of the DW_AT_comp_dir tag for Windows paths that require quoting.
  • Removed the compilation of .cm files written in Cminor concrete syntax.