| CompCert | |
|---|---|
| Sorts | Kompilator |
| Författare | Xavier Leroy , INRIA |
| Skrivet i | Caml _ _ |
| Första upplagan | 3 april 2008 |
| Hårdvaruplattform | Programvara för flera plattformar |
| senaste versionen | |
| Licens | gratis för icke-kommersiellt bruk [1] ; kommersiella licenser från AbsInt |
| Hemsida | compcert.inria.fr |
CompCert är ett projekt för att skapa officiellt verifierade kompilatorer. Projektet utvecklade CompCert C- kompilatorn för C- språket (ISO C90 / ANSI C-standarder med några mindre begränsningar och separata tillägg inspirerade av efterföljande standarder), och Coq -verifieringssystemet var helt skrivet och demonstrerat . Huvudutvecklaren är Xavier Leroy . Denna kompilator har en maskinkontroll att den genererade koden beter sig på samma sätt som källkoden. Kompilatorn låter dig generera maskinkod för PowerPC- , ARM- och x86- processorarkitekturerna .
Eftersom kompilatorer är mycket komplex programvara, lider de ofta av många buggar [3] . De kan till exempel inte generera kod som matchar källkoden. Dessa buggar kan leda till mycket allvarliga konsekvenser i kritiska områden. Därför är målet med CompCert att skapa en formellt verifierad kompilator med matematiska garantier.
Koden som genereras av CompCert är ungefär dubbelt så snabb som GCC genererad utan optimering och något långsammare än genererad med högre optimeringsnivåer. [fyra]