Frama-C - открытый, интегрированный набор инструментов для анализа исходного кода на языке Си доступен для загрузки под лицензией GNU LGPL v2.

Frama-C написан на языке OCaml и является ответвлением библиотеки CIL.

Набор включает ACSL (ANSI/ISO C Specification Language) - специальный язык, позволяющий подробно описывать спецификации функций C, например указать диапазон допустимых входных значений функции и диапазон нормальных выходных значений.

Этот инструментарий помогает производить такие действия:

• Осуществлять формальную валидацию кода;
• Искать потенциальные ошибки исполнения;
• Произвести аудит или рецензирование кода;
• Проводить реверс-инжиниринг кода для улучшения понимания структуры;
• Генерировать формальную документацию;

Frama-C включает такие полезные инструменты:

• Парсер, систему проверки типов и линкер уровня исходного кода для программы на языке С, опционально, аннотированной формулами ACSL.
• Набор плагинов статистического анализа:
  • Плагин обнаружения ошибок исполнения, базирующийся на интерпретации;
  • Плагин поиска зависимостей;
  • Интерактивный плагин анализа возможных значений переменной;
  • Плагин вычисления Use/Defs;
  • Плагин среза программы (автоматически вырезает работающее подмножество кода программы, которое соответствует некоторому критерию);
  • Калькулятор слабейшего предусловия, базирующийся на логике Флойда-Хоара (Floyd-Hoare);