CompCert

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
CompCert C
Développeurs Xavier Leroy, INRIA
Première version
Dernière version 2.5 ()
Écrit en Caml, Coq
Environnements Multiplate-forme
Type Compilateur
Site web http://compcert.inria.fr

CompCert est un projet dont l'objectif est la réalisation de compilateurs certifiés formellement. Essentiellement, ce projet développe un compilateur, CompCert C, pour le langage C (ISO C90 / ANSI C avec quelques limitations mineures et plusieurs extensions inspirées des normes ultérieures) entièrement écrit et prouvé avec le logiciel Coq. Le développeur principal est Xavier Leroy. 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 et x86.

Motivation[modifier | modifier le code]

Les compilateurs étant des logiciels très complexes, ils souffrent souvent de très nombreux bugs[1]. Par exemple, ils peuvent ne pas générer du code correspondant au code source. Ces bugs peuvent mener à des conséquences très graves dans des domaines critiques. Par conséquent, l'objectif de CompCert est de créer un compilateur formellement vérifié avec des assurances mathématiques.

Performances[modifier | modifier le code]

Le code généré par CompCert est environ deux fois plus rapide que celui généré par GCC sans optimisation et légèrement plus lent que celui généré avec des niveaux d'optimisation supérieurs[2].

Notes et références[modifier | modifier le code]

Voir aussi[modifier | modifier le code]