The CompCert C verified compiler
Documentation and user’s manual
Xavier Leroy, Collège de France and Inria, November 16, 2020
Copyright 2020 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
- 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.
This document was translated from LATEX by