About / Advertise
Kompilatorn Compcert producerar maskinkod som exakt följer vad standarden ISO C 99 föreskriver. Detta är bevisat, vilket enligt leverantören Absint är unikt. Det betyder att kompilatorn inte innehåller några buggar.Kompilatorer visar sig då och då innehålla buggar som uppträder under kuriösa omständigheter. Men det här kommer enligt Absint aldrig att kunna hända om du använder Compcert eftersom Absint har genomfört formella bevis av att kompilatorn är korrekt.
Det här betyder att du kan verifiera att ditt program är korrekt via resonemang kring C-källkoden, och därefter har rätt att dra slutsatsen att verifieringen är giltig även i den genererade maskinkoden.
Tekniken som används för att utföra bevisen härstammar från forskning på franska institutet Inria som gett Absint licens att använda kompilatorn. Från Inria härstammar även Xavier Leroy, som leder projektet och är Absints teknikchef.
Priset du betalar för garantin är cirka 20 procent sämre prestanda, i alla fall om du jämför med kompilatorn GCC, med alla optimeringsflaggor aktiverade. Det är å andra sidan kanske inte en rättvis jämförelse, eftersom optimeringsflaggor är något man gärna undviker när man skriver kritisk programvara, eftersom de har en tendens att introducera subtila programfel.
I jämförelse med GCC utan optimering är tvärtom Compcert som är överlägsen: den genererar dubbelt så snabba program, enligt Absints mätningar. Resultatet gäller enligt Absint för ”typisk programvara för inbyggda system”.
Ett annat pris du betalar är att beviset inte gäller hela ISO C 99, exempelvis inte instruktionerna setjmp och longjmp. Däremot stöds hela den delmängd av C som kallas MISRA-C 2004, vilket, återigen, är vad utvecklare av kritisk programvara snarare är intresserade av.
Compcert är gratis att använda för forskare.
