Copyright 2025 Xavier Leroy. This text is distributed under the terms of the Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.

This manual is also available in PDF format.

This document is the user’s manual for the CompCert C verified compiler. It is organized as follows:

• Chapter 1 gives an overview of the CompCert C compiler and of the formal verification of compilers.
• Chapter 2 explains how to install CompCert C.
• Chapter 3 explains how to use the CompCert C compiler.
• Chapter 4 explains how to use the CompCert C reference interpreter.
• Chapter 5 describes the subset of the ISO C99 language that is implemented by CompCert.
• Chapter 6 describes the supported language extensions: pragmas, attributes, built-in functions, inline assembly.

• CompCert C: a trustworthy compiler
  • Can you trust your compiler?
  • Formal verification of compilers
  • Structure of the CompCert C compiler
  • CompCert C in practice
• Installation instructions
  • Obtaining CompCert C
  • Prerequisites
  • Installation
• Using the CompCert C compiler
  • Overview
  • Options
• Using the CompCert C interpreter
  • Overview
  • Limitations
  • Options
  • Examples of use
• The CompCert C language
  • §5 Environment
  • §6 Language
  • §7 Library
• Language extensions
  • Pragmas
  • Attributes
  • Built-in functions
  • Embedded program annotations for a³
  • General program annotations
  • Extended inline assembly
• References

This document was translated from L^AT_EX by H^EV^EA.