| CompCert | |
|---|---|
| Tipo de | Compilador |
| Autor | Xavier Leroy , INRIA |
| Escrito en | cam _ _ |
| Primera edición | 3 de abril de 2008 |
| plataforma de hardware | Software multiplataforma |
| ultima versión |
|
| Licencia | gratis para uso no comercial [1] ; licencias comerciales de AbsInt |
| Sitio web | compcert.inria.fr |
CompCert es un proyecto para crear compiladores verificados oficialmente. El proyecto desarrolló el compilador CompCert C para el lenguaje C (estándares ISO C90/ANSI C con algunas restricciones menores y extensiones separadas inspiradas en estándares posteriores), y el sistema de verificación Coq se escribió y demostró por completo . El principal desarrollador es Xavier Leroy . Este compilador tiene una máquina para comprobar que el código generado se comporta igual que el código fuente. El compilador le permite generar código de máquina para las arquitecturas de procesador PowerPC , ARM y x86 .
Debido a que los compiladores son un software muy complejo, a menudo sufren muchos errores [3] . Por ejemplo, no pueden generar código que coincida con el código fuente. Estos errores pueden tener consecuencias muy graves en áreas críticas. Por lo tanto, el objetivo de CompCert es crear un compilador formalmente verificado con garantías matemáticas.
El código generado por CompCert es aproximadamente el doble de rápido que el generado por GCC sin optimización y un poco más lento que el generado con niveles de optimización más altos. [cuatro]