| CompCert | |
|---|---|
| Тип | Компилятор |
| Автор | Ксавье Лерой, INRIA |
| Написана на | Caml, Coq |
| Первый выпуск | 3 Апреля 2008 г. |
| Аппаратная платформа | Кроссплатформенное программное обеспечение |
| Последняя версия | 2.7.1 (Июнь 2016) |
| Лицензия | бесплатно для некоммерческого использования[1]; коммерческие лицензии от AbsInt |
| Сайт | compcert.inria.fr |
CompCert — проект по создания официально верифицированных компиляторов. В рамках проекта разработан компилятор CompCert C для языка С (стандартов ISO C90 / ANSI C с некоторыми незначительными ограничениями и отдельными расширениями, вдохновленные последующими стандартами), а также полностью написана и продемонстрирована система верификации Coq. Основной разработчик — Ксавье Лерой. У этого компилятора есть машинная проверка того, что что сгенерированный код ведет себя так же, как и исходный код. Компилятор позволяет генерировать машинный код для архитектур процессора PowerPC, ARM и x86.
Поскольку компиляторы являются очень сложным программным обеспечением, они часто страдают от большого количества багов[2]. Например, они не могут генерировать код, соответствующий исходному коду. Эти баги могут привести к очень серьезным последствиям в критических областях. Таким образом, цель CompCert в создании формально верифицированного компилятора с математическими гарантиями.
Код, сгенерированный CompCert, примерно вдвое быстрее, чем сгенерированный GCC без оптимизации и немного медленнее, чем сгенерированный с более высокими уровнями оптимизации.[3]
Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".
Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.
Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .