HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

The CompCert C verified compiler: Documentation and user’s manual

Xavier Leroy 1, 2
1 Chaire Sciences du logiciel
2 CAMBIUM - Langages de programmation : systèmes de types, concurrence, preuve de programme
Inria de Paris, CdF (institution) - Collège de France
Abstract : 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.
Document type :
Reports
Complete list of metadata
https://hal.inria.fr/hal-01091802
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Saturday, December 18, 2021 - 7:19:05 PM
Last modification on : Friday, February 4, 2022 - 3:10:20 AM

File

Vignette du document
manual.pdf
Files produced by the author(s)

Licence

Distributed under a Creative Commons Attribution - NonCommercial - ShareAlike 4.0 International License

Identifiers

  • HAL Id : hal-01091802, version 9

Collections

CDF | PSL | LARA | INRIA | INRIA2

Citation

Xavier Leroy. The CompCert C verified compiler: Documentation and user’s manual. [Intern report] Inria. 2021, pp.1-79. ⟨hal-01091802v9⟩

Export

BibTeX TEI DC DCterms EndNote Datacite

Share

Metrics

Record views

849

Files downloads

2505

 

Contact                    Legal Notice                    Personal Data