CompCert
| Oryginalni autorzy | Ksawerego Leroya |
|---|---|
| Deweloperzy | AbsInt |
| Pierwsze wydanie | 2005 |
| Wersja stabilna | 3.12 / 25 listopada 2022 r |
| Magazyn | |
| Typ | Kompilator |
| Licencja | bezpłatnie do użytku niekomercyjnego |
| Strona internetowa |
|
CompCert to formalnie zweryfikowany kompilator optymalizacyjny dla dużego podzbioru języka programowania C99 (znanego jako Clight), który obecnie jest przeznaczony dla architektur PowerPC , ARM , RISC-V , x86 i x86-64 . Projekt ten, prowadzony przez Xaviera Leroya , rozpoczął się oficjalnie w 2005 roku, finansowany przez francuskie instytuty ANR i INRIA . Kompilator jest określony, zaprogramowany i sprawdzony w Coq . Ma służyć do programowania systemów wbudowanych wymagających niezawodności . Wydajność wygenerowanego kodu jest często zbliżona do wydajności GCC (wersja 3) na poziomie optymalizacji -O1 i zawsze lepsza niż GCC bez optymalizacji.
Od 2015 roku AbsInt oferuje licencje komercyjne, zapewnia wsparcie i utrzymanie oraz przyczynia się do rozwoju narzędzia. CompCert jest udostępniany na licencji niekomercyjnej, a zatem nie jest wolnym oprogramowaniem , chociaż niektóre z jego plików źródłowych są objęte podwójną licencją z GNU Lesser General Public License w wersji 2.1 lub nowszej lub są dostępne na warunkach innych licencji.
Za rozwój CompCert, pierwszego praktycznie użytecznego kompilatora optymalizacyjnego przeznaczonego dla wielu komercyjnych architektur, który ma kompletny, mechanicznie sprawdzony dowód jego poprawności, Xavier Leroy i zespół programistów CompCert otrzymali nagrodę ACM Software System Award 2021 .
- ^ „Wydanie 3.12” . 25 listopada 2022 . Źródło 8 grudnia 2022 r .
- ^ a b „Licencja CompCert” .
- ^ Uwagi do wersji 3.0
- ^ Witryna CompCert
- ^ Wydajność CompCert
- ^ „CompCert - Partnerzy” . compcert.inria.fr . Źródło 2019-03-21 .