| CompCert | |
|---|---|
| Typ | Kompilátor |
| Autor | Xavier Leroy , INRIA |
| Zapsáno v | Caml _ _ |
| První vydání | 3. dubna 2008 |
| Hardwarová platforma | Multiplatformní software |
| Nejnovější verze |
|
| Licence | zdarma pro nekomerční použití [1] ; komerční licence od AbsInt |
| webová stránka | compcert.inria.fr |
CompCert je projekt na vytvoření oficiálně ověřených kompilátorů. V rámci projektu byl vyvinut kompilátor CompCert C pro jazyk C (normy ISO C90 / ANSI C s některými drobnými omezeními a samostatnými rozšířeními inspirovanými následujícími normami) a byl kompletně napsán a předveden ověřovací systém Coq . Hlavním vývojářem je Xavier Leroy . Tento kompilátor má strojovou kontrolu, zda se vygenerovaný kód chová stejně jako zdrojový kód. Kompilátor umožňuje generovat strojový kód pro architektury procesorů PowerPC , ARM a x86 .
Protože kompilátory jsou velmi složitý software, často trpí spoustou chyb [3] . Nemohou například generovat kód, který by odpovídal zdrojovému kódu. Tyto chyby mohou vést k velmi vážným následkům v kritických oblastech. Cílem CompCert je tedy vytvořit formálně ověřený překladač s matematickými zárukami.
Kód generovaný CompCertem je asi dvakrát rychlejší než GCC generovaný bez optimalizace a o něco pomalejší než generovaný s vyššími úrovněmi optimalizace. [čtyři]