CompCert — это компилятор языка программирования Си (ANSI C с незначительными ограничениями) для платформ PowerPC, ARM и IA32, предназначенный для сборки программ с повышенными требованиями надежности и дополняющий формальные методы проверки (статический анализ, проверка на модели и т.п.) на уровне исходного кода.
Некоторые изменения:
- поддержка типов long long и unsigned long long;
- предварительная поддержка отладочной информации;
- агрессивная стратегия исключения дублирующегося кода;
- уменьшено потребление памяти при компиляции;
- исправлены некоторые ошибки.
Исходные коды компилятора распространяются на условиях лицензии «INRIA Non-Commercial License Agreement».
>>> Подробности
