Вышел Frama-C - набор инструментов для анализа исходного кода на языке Си

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

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

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

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

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


Сообщает Opennet.ru



Опубликовал admin
5 Июн, Четверг 2008г.



Программирование для чайников.