| CompCert | |
|---|---|
| Tip de | Compilator |
| Autor | Xavier Leroy , INRIA |
| Scris in | Caml _ _ |
| Prima editie | 3 aprilie 2008 |
| Platformă hardware | Software multiplatformă |
| ultima versiune | |
| Licență | gratuit pentru uz necomercial [1] ; licențe comerciale de la AbsInt |
| Site-ul web | compcert.inria.fr |
CompCert este un proiect de creare a compilatoarelor verificate oficial. Proiectul a dezvoltat compilatorul CompCert C pentru limbajul C (standarde ISO C90 / ANSI C cu unele restricții minore și extensii separate inspirate de standardele ulterioare), iar sistemul de verificare Coq a fost complet scris și demonstrat . Dezvoltatorul principal este Xavier Leroy . Acest compilator are o mașină care verifică dacă codul generat se comportă la fel ca și codul sursă. Compilatorul vă permite să generați cod de mașină pentru arhitecturile de procesor PowerPC , ARM și x86 .
Deoarece compilatoarele sunt software foarte complexe, acestea suferă adesea de o mulțime de erori [3] . De exemplu, nu pot genera cod care să se potrivească cu codul sursă. Aceste erori pot duce la consecințe foarte grave în zonele critice. Astfel, scopul CompCert este de a crea un compilator verificat formal, cu garanții matematice.
Codul generat de CompCert este de aproximativ două ori mai rapid decât GCC generat fără optimizare și puțin mai lent decât generat cu niveluri de optimizare mai ridicate. [patru]