CompCert

Cet article est une ébauche concernant l’informatique.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

CompCert

Informations

Développé par	Xavier Leroy, Sandrine Blazy, INRIA
Fichier exécutable	ccomp
Première version	3 avril 2008
Dépôt	https://github.com/AbsInt/CompCert
Écrit en	OCaml, Rocq
Environnement	Multiplate-forme
Type	Compilateur
Licence	INRIA Non-Commercial License Agreement
Site web	compcert.org/compcert-C.html

modifier - modifier le code - voir Wikidata (aide)

CompCert est un projet dont l'objectif est la réalisation de compilateurs certifiés formellement. Ce projet développe essentiellement un compilateur, CompCert C, pour le langage C (ISO C99 avec quelques limitations mineures et plusieurs extensions inspirées de la norme ISO C2011^[1]) entièrement écrit et prouvé avec le logiciel Rocq. Le développeur principal est Xavier Leroy. Sandrine Blazy, Zaynah Dargaye, Jacques-Henri Jourdan, Michael Schmidt, Bernhard Schommer, et Jean-Baptiste Tristan participent activement en tant que développeurs à ce projet. Ce compilateur possède une preuve vérifiée par machine que le code généré se comporte de la même manière que le code source. Il permet de générer du code machine pour les architectures de processeur PowerPC, ARM, RISC-V, x86 et x86-64.