Jump to content

КомпСерт

КомпСерт
Оригинальный автор(ы) Ксавье Лерой
Разработчик(и) Абсент
Первоначальный выпуск 2005 г .; 19 лет назад ( 2005 )
Стабильная версия
3.12 / 25 ноября 2022 г.; 4 июля 2023 г. [1] [2]
Репозиторий
Тип Компилятор
Лицензия бесплатно для некоммерческого использования [3]
Веб-сайт концерт .org /compcert-C .html Отредактируйте это в Викиданных

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 .

  1. ^ «Релиз 3.12» . 25 ноября 2022 г. Проверено 8 декабря 2022 г.
  2. ^ «Релиз 3.13» . 4 июля 2023 г. Проверено 2 ноября 2023 г.
  3. ^ Jump up to: а б «Лицензия КомпСерт» .
  4. ^ Примечания к выпуску v3.0
  5. ^ Веб-сайт CompCert
  6. ^ Производительность CompCert
  7. ^ «КомпСерт – Партнеры» . compcert.inria.fr . Проверено 21 марта 2019 г.
[ редактировать ]


Arc.Ask3.Ru: конец переведенного документа.
Arc.Ask3.Ru
Номер скриншота №: 5db3f8b64b7de452c981d7b6fd3a0751__1710688080
URL1:https://arc.ask3.ru/arc/aa/5d/51/5db3f8b64b7de452c981d7b6fd3a0751.html
Заголовок, (Title) документа по адресу, URL1:
CompCert - Wikipedia
Данный printscreen веб страницы (снимок веб страницы, скриншот веб страницы), визуально-программная копия документа расположенного по адресу URL1 и сохраненная в файл, имеет: квалифицированную, усовершенствованную (подтверждены: метки времени, валидность сертификата), открепленную ЭЦП (приложена к данному файлу), что может быть использовано для подтверждения содержания и факта существования документа в этот момент времени. Права на данный скриншот принадлежат администрации Ask3.ru, использование в качестве доказательства только с письменного разрешения правообладателя скриншота. Администрация Ask3.ru не несет ответственности за информацию размещенную на данном скриншоте. Права на прочие зарегистрированные элементы любого права, изображенные на снимках принадлежат их владельцам. Качество перевода предоставляется как есть. Любые претензии, иски не могут быть предъявлены. Если вы не согласны с любым пунктом перечисленным выше, вы не можете использовать данный сайт и информация размещенную на нем (сайте/странице), немедленно покиньте данный сайт. В случае нарушения любого пункта перечисленного выше, штраф 55! (Пятьдесят пять факториал, Денежную единицу (имеющую самостоятельную стоимость) можете выбрать самостоятельно, выплаичвается товарами в течение 7 дней с момента нарушения.)