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 .