CompCert

Cet article est une ébauche concernant l’informatique.

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
Dernière version 3.17 ()[1]Voir et modifier les données sur Wikidata
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.htmlVoir et modifier les données sur Wikidata

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[2]) 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.

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

Récompenses

CompCert a été récompensé par l'Association for computing machinery avec le Prix ACM Software System en 2021 notamment[5].

Notes et références

  1. ↑ « CompCert 3.17 », (consulté le )
  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
  5. ↑ « CompCert récompensé par l’ACM pour ses garanties d’absence de bugs », sur CNRS, (consulté le )

Voir aussi

Content Disclaimer

Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.

  1. The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
  2. There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
  3. It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
  4. Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
  5. Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.