| CompCert | |
|---|---|
| Type | Kompiler |
| Forfatter | Xavier Leroy , INRIA |
| Skrevet i | Caml _ _ |
| Første udgave | 3. april 2008 |
| Hardware platform | Cross-platform software |
| nyeste version | |
| Licens | gratis til ikke-kommerciel brug [1] ; kommercielle licenser fra AbsInt |
| Internet side | compcert.inria.fr |
CompCert er et projekt til at skabe officielt verificerede compilere. Projektet udviklede CompCert C- kompileren til C -sproget (ISO C90 / ANSI C-standarder med nogle mindre begrænsninger og separate udvidelser inspireret af efterfølgende standarder), og Coq -verifikationssystemet blev fuldstændig skrevet og demonstreret . Hovedudvikleren er Xavier Leroy . Denne compiler har en maskinkontrol af, at den genererede kode opfører sig på samme måde som kildekoden. Compileren giver dig mulighed for at generere maskinkode til PowerPC- , ARM- og x86 - processorarkitekturerne .
Fordi compilere er meget kompleks software, lider de ofte af mange fejl [3] . For eksempel kan de ikke generere kode, der matcher kildekoden. Disse fejl kan føre til meget alvorlige konsekvenser i kritiske områder. Derfor er målet med CompCert at skabe en formelt verificeret compiler med matematiske garantier.
Kode genereret af CompCert er cirka dobbelt så hurtig som GCC genereret uden optimering og lidt langsommere end genereret med højere optimeringsniveauer. [fire]