Ubuntu 14.04でFrama-c用のImpact Analysisプラグインをインストールするには？

Question

私は、次のコマンドを使用して、Ubuntuの14.04でFRAMA-Cをインストール：

sudo apt-get install frama-c 

しかし、私は次のコマンドを使用してFRAMA-CのGUIを開くとき：

frama-c-gui 

を私は見つけることができません左側のウィンドウに "Impact Analysis"プラグインがあります。

この図は私のFRAMA-Cの現在利用可能なプラグインを示しています

私もFrama-c web page呼ばなく、プラグインをインパクト分析をダウンロードまたはインストールするには、私のためにすべてのリンクを見つけることができません。

Ubuntu 14.04でImpact Analysisを有効にして使用するにはどうすればよいですか？

Answer 1

Impactプラグインは、バージョンNeon-20140301以降、Frama-Cと一緒にインストールされています。有効にするために特別な操作を行う必要はありません。あなたが言及したFRAMA-CのWebページから

は（太字関連部分にハイライト表示）：

影響分析は、FRAMA-Cグラフィカル・ユーザー・インターフェース内の各ステートメントでコンテクストメニューから利用できます。

は

あなたのスクリーンショットの左側のウィンドウには、それらのプラグイン用のプラグインパネルのリスト、（ファイル名およびグローバル変数/関数で、上部）filetreeが含まれています独自のGUIパネルを登録しました。すべてのプラグインにパネルが関連付けられているわけではありません。たとえば、Impactは、コンテキストメニューを使用してのみ使用できるプラグインです。

Frama-CウェブサイトのImpactプラグインページを詳しく見ると、表示されたスクリーンショットにはスクリーンショットのGUIの一部が含まれていないことがわかりますが、その左側の部分は既にCilですコード（スクリーンショットでは省略）：

スクリーンショットに示されたポップアップメニューを取得するには、声明は単なる表現ではなく、強調表示されている必要があります。スクリーンショットでは、p = T;ステートメント全体が強調表示されています。そうしないと、コンテキストメニューに「影響分析」項目が表示されません。

Frama-C GUIで文を選択する簡単な方法は、の後にセミコロンのをクリックすることです。上記のスクリーンショットのように代入文であれば、等号をクリックして文を選択することもできます。ただし、pまたはTを直接クリックすると、それらの変数に対応する式だけが選択されます。 Impactは式ではなくステートメントに基づいているため、このような場合はコンテキストメニューが表示されません。

ちなみに、Frama-Cインストールで特定のプラグインが利用可能かどうかを確認するには、frama-c -pluginsを実行して、インストールされているプラ​​グインの一覧を取得するか、プラグインごとに1つのエントリが含まれているGUI（メニューの[分析/分析]）。

編集：VMでのテストの後、私はUbuntuの14.04（トラスティ）がインパクトプラグインを持っていなかった非常に古いバージョンでそのパッケージで（2013年から）FRAMA-Cフッ素を、持っていることに気づき、何らかの理由で、Debianパッケージには含まれていませんでした（そのため、使用できません）。 Frama-Cは急速に進化しているので、古いバージョンを使用するといくつかの問題が発生します。 OPAM経由でインストールすることをお勧めします。