CompCert
| CompCert | |
|---|---|
| Тип | Компилятор |
| Автор | Ксавье Лерой, INRIA |
| Написана на | Caml, Coq |
| Первый выпуск | 3 Апреля 2008 г. |
| Аппаратная платформа | Кроссплатформенное программное обеспечение |
| Лицензия | бесплатно для некоммерческого использования[1]; коммерческие лицензии от AbsInt |
| Ссылки | |
| Сайт | compcert.inria.fr |
CompCert — проект по созданию официально верифицированных компиляторов. В рамках проекта разработан компилятор CompCert C для языка С (стандартов ISO C90 / ANSI C с некоторыми незначительными ограничениями и отдельными расширениями, вдохновленные последующими стандартами), а также полностью написана и продемонстрирована система верификации Coq. Основной разработчик — Ксавье Лерой. У этого компилятора есть машинная проверка того, что сгенерированный код ведет себя так же, как и исходный код. Компилятор позволяет генерировать машинный код для архитектур процессора PowerPC, ARM и x86.
Мотивация[править]
Поскольку компиляторы являются очень сложным программным обеспечением, они часто страдают от большого количества багов[2]. Например, они не могут генерировать код, соответствующий исходному коду. Эти баги могут привести к очень серьезным последствиям в критических областях. Таким образом, цель CompCert в создании формально верифицированного компилятора с математическими гарантиями.
Реализация[править]
Код, сгенерированный CompCert, примерно вдвое быстрее, чем сгенерированный GCC без оптимизации и немного медленнее, чем сгенерированный с более высокими уровнями оптимизации.[3]
См. также[править]
Примечания[править]
- ↑ Архивированная копия. Дата обращения: 12 декабря 2016. Архивировано 13 августа 2011 года.
- ↑ Архивированная копия. Дата обращения: 12 декабря 2016. Архивировано 6 июля 2017 года.
- ↑ CompCert - The CompCert C compiler. Дата обращения: 12 декабря 2016. Архивировано 3 декабря 2015 года.