 | В этой статье слишком много ссылок на первоисточники . ( Февраль 2018 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения ) |
![[икона]](/wiki/File:Wiki_letter_w_cropped.svg){kind=small} | Этот раздел нуждается в расширении . Вы можете помочь, добавив к нему . ( Февраль 2018 г. ) |
| Стабильный выпуск | 3.8 / 16 ноября 2020 г . |
|---|---|
| Репозиторий |  |
| Тип | Компилятор |
| Лицензия | бесплатно для некоммерческого использования [1] |
| Веб-сайт | https://compcert.org/ |
CompCert - это официально проверенный оптимизирующий компилятор для большого подмножества языка программирования C99 (известного как Clight), который в настоящее время ориентирован на архитектуры PowerPC , ARM , RISC-V , x86 и x86-64 [2] . [3] Этот проект, возглавляемый Ксавье Леруа , официально стартовал в 2005 году при финансовой поддержке французских институтов ANR и INRIA . Компилятор указан, запрограммирован и испытан на Coq . Он предназначен для использования для программирования встраиваемых систем, требующих надежности.. Производительность его сгенерированного кода часто близка к производительности GCC (версия 3) на уровне оптимизации -O1 и всегда лучше, чем у GCC без оптимизаций. [4]
С 2015 года AbsInt предлагает коммерческие лицензии, [5] обеспечивает поддержку и обслуживание, а также способствует развитию инструмента. CompCert выпускается по некоммерческой лицензии и, следовательно, не является бесплатным программным обеспечением , хотя некоторые из его исходных файлов имеют двойную лицензию с Стандартной общественной лицензией GNU версии 2 или более поздней версии или доступны на условиях других лицензий. [1]
Ссылки [ править ]
- ^ a b «Лицензия CompCert» .
- ^ Примечания к выпуску v3.0
- ^ Веб-сайт CompCert
- ^ Производительность CompCert
- ^ "CompCert - Партнеры" . compcert.inria.fr . Проверено 21 марта 2019 .
Внешние ссылки [ править ]
- Формальная проверка реалистичного компилятора
- Официальный веб-сайт
- CompCert на GitHub
