The subset of C supported by CompCert

CompCert supports all of ISO C 99, with the following exceptions:

• Variable-length arrays are not supported.
• longjmp and setjmp are not guaranteed to work.
• By default, switch statements must be structured as in MISRA-C. Support for unstructured switches, as in Duff’s Device, can be activated via the command-line option -funstructured-switch.

With that, CompCert supports the full MISRA-C 2004 subset of C, plus many features that are excluded by MISRA (such as recursive functions and dynamic heap memory allocation).

Additionally, a number of ISO C 2011 features are supported:

• The _Alignof operator and the _Alignas attribute.
• Anonymous structures and unions.
• _Static_assert statements and _Generic expressions.
• Unicode string literals and character constants.

Furthermore, CompCert supports some extensions to ISO C taken from the GNU and Diab compilers:

• Pragmas and attributes to control the alignment and section placement of global variables.
• Attributes to control struct packing, function inlining, etc.
• Built-in functions to provide access to certain processor-specific instructions.
• Inline assembly code with GNU-style arguments.

Free trial

Request your free trial package today, complete with training and support via WebEx and email.