The CompCert C verified compiler: Documentation and user’s manual - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2023

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

Résumé

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 (407.56 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et 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)
hal-01091802 , version 11 (05-12-2023)

Licence

Paternité - Pas d'utilisation commerciale - Partage selon les Conditions Initiales

Identifiants

  • HAL Id : hal-01091802 , version 11

Citer

Xavier Leroy. The CompCert C verified compiler: Documentation and user’s manual. [Intern report] Inria. 2023, pp.1-79. ⟨hal-01091802v11⟩
1240 Consultations
3957 Téléchargements

Partager

Gmail Facebook X LinkedIn More