The CompCert C verified compiler: Documentation and user’s manual - Archive ouverte HAL Access content directly
Reports Year : 2021

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

(1, 2)
1
2

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.
Fichier principal
Vignette du fichier
manual.pdf (449.81 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-01091802 , version 1 (06-12-2014)
hal-01091802 , version 2 (22-12-2015)
hal-01091802 , version 3 (22-12-2015)
hal-01091802 , version 4 (09-12-2016)
hal-01091802 , version 5 (05-11-2017)
hal-01091802 , version 6 (09-11-2018)
hal-01091802 , version 7 (19-11-2019)
hal-01091802 , version 8 (09-12-2020)
hal-01091802 , version 9 (18-12-2021)
hal-01091802 , version 10 (06-12-2022)

Licence

Attribution - NonCommercial - ShareAlike - CC BY 4.0

Identifiers

  • HAL Id : hal-01091802 , version 9

Cite

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

Share

Gmail Facebook Twitter LinkedIn More