CompCert
| CompCert | |
|---|---|
| Тип | компилятор и source-available software[вд] |
| Написана на | OCaml и Rocq |
| Последняя версия |
|
| Репозиторий | github.com/AbsInt/CompCe… |
| Лицензия | source available license[вд][2] |
| Сайт | compcert.org/comp… (англ.) |
CompCert — проект по созданию официально верифицированных компиляторов. В рамках проекта разработан компилятор CompCert C для
Ксавье Леруа. У этого компилятора есть машинная проверка того, что сгенерированный код ведёт себя так же, как и исходный код. Компилятор позволяет генерировать машинный код для архитектур процессора PowerPC, ARM и x86
.
Код, сгенерированный CompCert, примерно вдвое быстрее, чем сгенерированный GCC без оптимизации и немного медленнее, чем сгенерированный с более высокими уровнями оптимизации[3]
См. также
Примечания
- ↑ Release Compcert 3.15 — 2024.
- ↑ https://github.com/AbsInt/CompCert/blob/master/LICENSE
- ↑ CompCert - The CompCert C compiler. Дата обращения: 12 декабря 2016. Архивировано 3 декабря 2015 года.