CompCert

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[2]) 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, RISC-V, x86 et x86-64.

CompCert

Informations
Développé par Xavier Leroy, INRIA
Fichier exécutable ccomp
Première version
Dernière version 3.11 ()[1]
Dépôt https://github.com/AbsInt/CompCert
Écrit en OCaml, Coq
Environnement Multiplate-forme
Type Compilateur
Licence INRIA Non-Commercial License Agreement
Site web compcert.org/compcert-C.html

Motivation

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

Performances

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[4].

Notes et références
  1. « https://github.com/AbsInt/CompCert/releases/tag/v3.11 »
  2. « The CompCert ‍C language », sur compcert.org (consulté le )
  3. Xuejun Yang, Yang Chen, Eric Eide, John Regehr, « Finding and Understanding Bugs in C Compilers », University of Utah, School of Computing
  4. « CompCert — Performance of the generated code », sur INRIA

Voir aussi
  • Portail de l’informatique
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.