CompCert

The verified C compiler.

Overview

The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM, x86 and RISC-V processors.

The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code.

For more information on CompCert (supported platforms, supported C features, installation instructions, using the compiler, etc), please refer to the Web site and especially the user's manual.

Verimag-Kalray version

This is a special version with additions from Verimag and Kalray :

• A backend for the KVX processor: see README_Kalray.md for details.
• Some general-purpose optimization phases (e.g. profiling).
  • see PROFILING.md for details on the profiling system

The people responsible for this version are

• Sylvain Boulmé (Grenoble-INP, Verimag)
• David Monniaux (CNRS, Verimag)
• Cyril Six (Kalray)

Papers, docs, etc on this CompCert version

• a 5-minutes video by C. Six, presenting the postpass scheduling and the KVX backend.
• Certified and Efficient Instruction Scheduling, an OOPSLA'20 paper, by Six, Boulmé and Monniaux.
• the documentation of the KVX backend Coq sources

License

CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes. A commercial version of CompCert, without this restriction and with professional support, can be purchased from AbsInt. See the file LICENSE for more information.

Copyright

The CompCert verified compiler is Copyright Institut National de Recherche en Informatique et en Automatique (INRIA) and AbsInt Angewandte Informatik GmbH.

The additions are Copyright Grenoble-INP, CNRS and Kalray.

Contact

General discussions on CompCert take place on the compcert-users@inria.fr mailing list.

For inquiries on the commercial version of CompCert, please contact info@absint.com

For inquiries on the Verimag-specific additions, contact the researchers.