The CompCert ‍C verified compiler

Documentation and user’s manual

Version 3.12


Xavier Leroy, Collège de France and Inria, November ‍25, 2022

Copyright 2022 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:


This document was translated from LATEX by HEVEA.