Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Не путать с Framasoft .
Фрама-С
Логотип Frama-C, full.png
Разработчики)Commissariat à l'Énergie Atomique ( CEA-List ) и Inria
Репозиторий
Отредактируйте это в Викиданных
Написано вOCaml
Операционная системаMicrosoft Windows , FreeBSD , OpenBSD , Linux , Mac OS X
Доступно ванглийский
ТипФормальная проверка , Статический анализ кода
Лицензияв основном LGPL , некоторые части под лицензиями BSD
Веб-сайтframa-c .com

Frama-C [1] обозначает рамки для модульного анализа программ C . Frama-C представляет собой набор совместимых анализаторов программ для программ C . Frama-C был разработан Французским комиссариатом по атомной энергии и альтернативным источникам энергии ( CEA-List ) [2] и Inria . Он также получил финансирование от Инициативы по базовой инфраструктуре . Frama-C, как статический анализатор , проверяет программы, не выполняя их. Несмотря на название, программа не имеет отношения к французскому проекту Framasoft .

Архитектура [ править ]

Frama-C имеет модульную архитектуру плагинов [3], сравнимую с Eclipse (программное обеспечение) или GIMP .

Frama-C использует CIL ( промежуточный язык C ) для создания абстрактного синтаксического дерева . В абстрактное синтаксическое дерево опоры аннотации , написанные на ANSI / ISO C спецификации языка (ACSL).

Несколько модулей могут управлять абстрактным синтаксическим деревом для добавления аннотаций ANSI / ISO C Specification Language (ACSL). Среди часто используемых [ расплывчатых ] плагинов:

  • Анализ значений  - вычисляет значение или набор возможных значений для каждой переменной в программе. Этот плагин использует абстрактные методы интерпретации , и многие другие плагины используют его результаты.
  • Джесси  - проверяет свойства дедуктивным способом. Джесси полагается на серверную часть Why [4] или Why3, чтобы обеспечить отправку обязательств по доказательству автоматическим средствам доказательства теорем, таким как Z3, Simplify, Alt-Ergo, или интерактивным средствам доказательства теорем, таким как Coq или Why. Используя Jessie, можно доказать , что реализация системы пузырьковой сортировки или игрушечной системы электронного голосования удовлетворяет их соответствующим спецификациям. Он использует модель памяти разделения, вдохновленную логикой разделения .
  • WP (слабое предварительное условие)  - аналогично Джесси , проверяет свойства дедуктивным способом. В отличие от Джесси, он фокусируется на параметризации в отношении модели памяти. WP разработан для взаимодействия с другими плагинами Frama-C, такими как плагин анализа значений, в отличие от Jessie, который компилирует программу C непосредственно в язык Why. WP может дополнительно использовать платформу Why3 для вызова многих других автоматических и интерактивных программ проверки.
  • Анализ воздействия  - подчеркивает влияние модификации исходного кода C.
  • Нарезка  - позволяет нарезать программу . Это позволяет сгенерировать новую программу C меньшего размера, которая сохраняет некоторые заданные свойства. [5]
  • Запасной код  - удаляет бесполезный код из программы C.

Другие плагины:

  • Dominators  - вычисляет доминаторы и постдоминаторы утверждений.
  • Из анализа  - вычисляет функциональные зависимости.

Особенности [ править ]

Frama-C может использоваться для следующих целей:

  • Чтобы понять код C, который вы не писали. В частности, Frama-C позволяет наблюдать набор значений, разбивать программу на более короткие программы и перемещаться по программе.
  • Доказать формальные свойства кода. Использование спецификаций, написанных на языке спецификаций ANSI / ISO C, позволяет гарантировать свойства кода для любого возможного поведения. Frama-C обрабатывает числа с плавающей запятой. [6]
  • Обеспечить соблюдение стандартов кодирования или соглашений о коде в исходном коде C с помощью настраиваемых плагинов [7]
  • Для защиты кода C от некоторых недостатков безопасности [8]

См. Также [ править ]

  • СПАРК (язык программирования)

Ссылки [ править ]

  1. ^ "Frama-C" . frama-c.com . Проверено 5 ноября 2016 .
  2. ^ СПИСОК CEA. «CEA LIST, Умные цифровые системы» . Проверено 5 ноября 2016 .
  3. ^ Паскаль Куок; и другие. (Август 2009 г.). «Отчет об опыте использования OCaml для структуры статического анализа промышленной прочности». Материалы 14-й Международной конференции ACM SIGPLAN по функциональному программированию . 44 (9): 281–286. DOI : 10.1145 / 1631687.1596591 .
  4. ^ "Почему домашняя страница" .
  5. ^ Бенджамин Монате; Жюльен Синьолес (2008). «Нарезка для защиты кода». Надежные вычисления - проблемы и приложения . Конспект лекций по информатике. 4968/2008. DOI : 10.1007 / 978-3-540-68979-9_10 . ISBN 978-3-540-68978-2.
  6. ^ Сильви Болдо; Тхи Мин Туен Нгуен (2010). "Аппаратно-независимые доказательства числовых программ" (PDF) . Материалы НМФ 2010 .
  7. ^ Дэвид Дельмас; Стефан Дюпра; Виктория Моя Ламиэль; Жюльен Синьолес. «Taster, подключаемый модуль Frama-C для обеспечения соблюдения стандартов кодирования» (PDF) . Встроенное программное обеспечение и системы реального времени 2010, Тулуза, Франция .
  8. ↑ Джонатан-Кристофер Демей; Эрик Тотель; Фредерик Тронель (2009). «Автоматическое программное обеспечение для обнаружения атак, не связанных с контрольными данными». Последние достижения в обнаружении вторжений . Конспект лекций по информатике. 5758/2009. С. 348–349. DOI : 10.1007 / 978-3-642-04342-0_19 . ISBN 978-3-642-04341-3.

Внешние ссылки [ править ]

  • Официальный веб-сайт
  • Список обсуждения Frama-C
  • Система отслеживания ошибок Frama-C