КомпСерт
Оригинальный автор(ы) | Ксавье Лерой |
---|---|
Разработчик(и) | Абсент |
Первоначальный выпуск | 2005 г |
Стабильная версия | |
Репозиторий | |
Тип | Компилятор |
Лицензия | бесплатно для некоммерческого использования [3] |
Веб-сайт | концерт |
Этот раздел нуждается в расширении . Вы можете помочь, добавив к нему . ( февраль 2018 г. ) |
CompCert — это официально проверенный оптимизирующий компилятор для большого подмножества языка программирования C99 (известного как Clight), который в настоящее время предназначен для PowerPC , ARM , RISC-V , x86 и x86-64. [4] архитектуры. [5] Этот проект, возглавляемый Ксавье Леруа , официально стартовал в 2005 году и финансировался французскими институтами ANR и INRIA . Компилятор указан, запрограммирован и проверен в Coq . Он предназначен для использования для программирования встроенных систем, требующих надежности . Производительность сгенерированного кода часто близка к производительности GCC (версия 3) на уровне оптимизации -O1 и всегда лучше, чем у GCC без оптимизации. [6]
С 2015 года AbsInt предлагает коммерческие лицензии, [7] обеспечивает поддержку и обслуживание, а также способствует развитию инструмента. CompCert выпускается под некоммерческой лицензией и, следовательно, не является свободным программным обеспечением , хотя некоторые из его исходных файлов имеют лицензию двойную GNU Lesser General Public License версии 2.1 или более поздней или доступны на условиях других лицензий. [3]
За разработку CompCert, первого практически полезного оптимизирующего компилятора, ориентированного на несколько коммерческих архитектур, имеющего полное, механически проверенное доказательство его правильности, Ксавье Лерой и команда разработчиков CompCert получили премию ACM Software System Award 2021 .
Ссылки
[ редактировать ]- ^ «Релиз 3.12» . 25 ноября 2022 г. Проверено 8 декабря 2022 г.
- ^ «Релиз 3.13» . 4 июля 2023 г. Проверено 2 ноября 2023 г.
- ^ Jump up to: а б «Лицензия КомпСерт» .
- ^ Примечания к выпуску v3.0
- ^ Веб-сайт CompCert
- ^ Производительность CompCert
- ^ «КомпСерт – Партнеры» . compcert.inria.fr . Проверено 21 марта 2019 г.
Внешние ссылки
[ редактировать ]- Официальный сайт
- CompCert на GitHub
- Формальная проверка реалистичного компилятора
- Премия за программную систему — ACM Awards