The OpenNET Project / Index page

[ новости /+++ | форум | wiki | теги | ]

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

04.06.2008 00:20

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

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

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

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

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

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

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


  1. Главная ссылка к новости (http://lwn.net/Articles/284650...)
  2. What is Frama-C
Автор новости: zyx
Тип: К сведению
Короткая ссылка: https://opennet.ru/16282-gcc
Ключевые слова: gcc, compile, debug, code
Поддержать дальнейшую публикацию новостей на OpenNET.


Обсуждение (9) Ajax | 1 уровень | Линейный | +/- | Раскрыть всё | RSS
  • 1.1, Aleksey (??), 09:03, 04/06/2008 [ответить]  
  • +/
    А для C++ что-то подобное есть?
     
     
  • 2.3, Аноним (3), 18:36, 04/06/2008 [^] [^^] [^^^] [ответить]  
  • +/
    Плюсы отчекать никакого ИИ не хватит. C(ompile and pray!)++
     
  • 2.7, pavlinux (ok), 01:43, 05/06/2008 [^] [^^] [^^^] [ответить]  
  • +/
    ./configure --enable-cxx
     

  • 1.2, Аноним (-), 10:08, 04/06/2008 [ответить]  
  • +/
    The following environments have been tested to be able to run Frama-C:
    Ubuntu Linux on x86 and AMD64
    Windows XP x86
    MacOS X Tiger and Leopard on PowerPC and Intel
     
  • 1.4, pavlinux (ok), 19:02, 04/06/2008 [ответить]  
  • +/
    Этот OCalm это какая-то попа...
     
     
  • 2.5, vitek (??), 23:39, 04/06/2008 [^] [^^] [^^^] [ответить]  
  • +/
    да ладно...
    вот пробую..
    и не знал.
     
     
  • 3.6, pavlinux (ok), 23:44, 04/06/2008 [^] [^^] [^^^] [ответить]  
  • +/
    >да ладно...
    >вот пробую..
    >и не знал.

    Как настроить до рабочего вида OCalm расскажешь?

     
     
  • 4.8, Аноним (3), 18:04, 05/06/2008 [^] [^^] [^^^] [ответить]  
  • +/
    >Как настроить до рабочего вида OCalm расскажешь?

    OCalm ? Сам не знаю, Ocaml - make install clean и всё!

     
     
  • 5.9, pavlinux (ok), 18:20, 05/06/2008 [^] [^^] [^^^] [ответить]  
  • +/
    >>Как настроить до рабочего вида OCalm расскажешь?
    >
    >OCalm ? Сам не знаю, Ocaml - make install clean и всё!
    >

    Ну очепятка...

    В общем поставил... часа 3 трахался с библиотеками, особенно c lablgtk...

    Теперь пытаюсь выяснить, какой от неё толк.


     
     Добавить комментарий
    Имя:
    E-Mail:
    Текст:
    При перепечатке указание ссылки на opennet.ru обязательно



    Спонсоры:
    Inferno Solutions
    Hosting by Hoster.ru
    Хостинг:

    Закладки на сайте
    Проследить за страницей
    Created 1996-2021 by Maxim Chirkov
    Добавить, Поддержать, Вебмастеру