The CompCert C verified compiler
Documentation and user’s manual
Xavier Leroy, INRIA Paris, February 10, 2017
Copyright 2017 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