Как установить плагин Impact Analysis для Frama-c в Ubuntu 14.04?

Question

Я установил Frama-c на Ubuntu 14.04, используя следующие команды:

sudo apt-get install frama-c

Однако, когда я открываю графический интерфейс frama-c, используя следующую команду:

frama-c-gui

Я не могу найти плагин "Анализ воздействия" в левом окне.

На этом рисунке показан в настоящее время доступный плагин моего Frama-c:

Я также ссылался на веб-страницу Frama-c, но не могу найти никаких ссылок для загрузки или установки подключаемого модуля Impact Analysis.

Как я могу включить и использовать Impact Analysis в Ubuntu 14.04?

Answer 1

Плагин Impact уже установлен с Frama-C начиная с версии Neon-20140301, и вам не нужно делать ничего особенного, чтобы включить его, просто выберите оператор и найдите правильное контекстное меню для его активации.

С упомянутой вами веб-страницы Frama-C (выделена жирным шрифтом соответствующая часть):

Анализ воздействия доступен через контекстное меню каждого оператора в графическом пользовательском интерфейсе Frama-C.

Левое окно на вашем скриншоте содержит дерево файлов (верхняя часть, с именами файлов и глобальными переменными / функциями) и список панелей плагинов для тех плагинов, которые зарегистрировали свои собственные панели графического интерфейса. Обратите внимание, что не все плагины имеют связанные панели; Например, Impact - это плагин, который доступен только через контекстные меню.

Присмотревшись к странице плагина Impact на веб-сайте Frama-C, вы заметите, что показанный снимок экрана не включает часть графического интерфейса в скриншоте, но вместо этого его левая часть уже является кодом Cil (опущено в ваш скриншот):

Чтобы получить всплывающее меню, указанное на скриншоте, необходимо выделить оператор, а не просто выражение. Обратите внимание, что на скриншоте вся p = T; Заявление выделено. В противном случае в контекстном меню не будет отображен пункт "Анализ воздействия".

Простой способ выбрать оператор в графическом интерфейсе Frama-C - щелкнуть после точки с запятой. Если это оператор присваивания, как на скриншоте выше, вы также можете нажать на знак равенства, чтобы выбрать оператор. Однако, если вы нажмете на p или же T непосредственно, вы будете выбирать только выражение, соответствующее этим переменным. Поскольку Impact основан на выражениях, а не на выражениях, в таких случаях он не будет отображать свое контекстное меню.

Кстати, если вы хотите проверить, доступен ли данный плагин в вашей установке Frama-C, вы можете просто запустить frama-c -plugins чтобы получить список установленных плагинов или открыть панель "Анализы" в графическом интерфейсе (меню "Анализ / Анализ"), которая содержит одну запись для каждого плагина.

Редактировать: после тестирования на виртуальной машине я понял, что Ubuntu 14.04 (Trusty) имеет Frama-C Fluorine (с 2013 года) в своих пакетах, что является очень старой версией, в которой был подключаемый модуль Impact, но по какой-то причине это было в данный момент не входит в пакет Debian (поэтому вы не можете его использовать). Frama-C быстро развивается, поэтому использование такой старой версии приведет к нескольким проблемам. Я действительно рекомендую попробовать установить его через OPAM.