如何在Ubuntu 14.04上爲Frama-c安裝影響分析插件？

Question

我安裝郵資-C在Ubuntu 14.04，使用下列命令：

sudo apt-get install frama-c 

然而，當我使用下面的命令打開郵資-C的GUI：

frama-c-gui 

我無法找到左側窗口中的「Impact Analysis」插件。

此圖顯示了我的郵資-C的當前可用的插件：

我也提到了Frama-c web page卻找不到任何聯繫我下載或安裝的影響分析插件。

如何在Ubuntu 14.04上啓用和使用Impact Analysis？

Answer 1

從Neon-20140301開始，Impact插件已經與Frama-C一起安裝，並且您無需執行任何特殊操作即可啓用它，只需選擇一個語句並找到正確的上下文菜單即可將其激活。

從你提到的郵資-C網頁（以粗體顯示的相關部分高亮）：

影響分析，可通過在郵資-C++圖形用戶界面在每個語句一個上下文菜單。

在你的屏幕截圖的左側窗口包含文件樹（上部，用文件名和全局變量/函數），併爲這些插件插件板的名單，這注冊了自己的GUI面板。請注意，並非所有插件都有相關的面板;例如，影響是一個只能通過上下文菜單才能使用的插件。

仔細觀察Frama-C網站上的Impact插件頁面，您會注意到所顯示的屏幕截圖不包括截圖中的GUI部分，而是其左側部分已經是Cil代碼（省略您的截圖）：

要獲得的截圖所示的彈出式菜單中，你需要有一個聲明強調的，不只是一個表達。請注意，在屏幕截圖中，整個p = T;語句突出顯示。否則，上下文菜單將不會顯示「影響分析」項目。

在Frama-C GUI中選擇語句的簡單方法是在分號後單擊。如果它是一個賦值語句，如上面的截圖所示，您也可以單擊等號來選擇語句。但是，如果直接點擊p或T，則只會選擇與這些變量相對應的表達式。因爲Impact是基於語句而不是表達式的，所以在這種情況下它不會顯示其上下文菜單。順便說一句，如果您想檢查您的Frama-C安裝中是否有給定的插件，您可以簡單地運行frama-c -plugins以獲取已安裝插件的列表，或者打開「分析」面板GUI（菜單分析/分析），每個插件包含一個條目。

編輯：與VM的測試後，我意識到的Ubuntu 14.04（忠實的）具有郵資-C氟（自2013年）在其包裝，這是一個很老的版本，也有衝擊插件，但由於某種原因，它當時並未包含在Debian軟件包中（這就是爲什麼你不能使用它）。 Frama-C正在迅速發展，所以使用這樣一箇舊版本會導致幾個問題。我真的建議嘗試通過OPAM安裝它。