如何在 Ubuntu 14.04 上安装 Frama-c 的影响分析插件？

Question

我在 Ubuntu 14.04 上安装了 Frama-c，使用以下命令：

sudo apt-get install frama-c

但是，当我使用以下命令打开 frama-c 的 GUI 时：

frama-c-gui

我在左侧窗口中找不到“影响分析”插件。

此图显示了我的 Frama-c 目前可用的插件：

我也参考了Frama-c web page，但找不到任何链接供我下载或安装影响分析插件。

如何在 Ubuntu 14.04 上启用和使用影响分析？

Answer 1

Impact 插件自 Neon-20140301 版本起已与 Frama-C 一起安装，您无需执行任何特殊操作即可启用它，只需选择一个语句并找到正确的上下文菜单即可激活它。

来自您提到的 Frama-C 网页（以粗体突出显示相关部分）：

影响分析可通过 Frama-C 图形用户界面中的每个语句的上下文菜单进行。

屏幕截图中的左侧窗口包含文件树（上部，带有文件名和全局变量/函数）和插件面板列表，注册了自己的 GUI 面板的插件。请注意，并非所有插件都有关联的面板；例如，Impact 是一个只能通过上下文菜单使用的插件。

仔细查看 Frama-C 网站的 Impact 插件页面，您会注意到显示的屏幕截图中没有包含 GUI 的部分，而是其左侧部分已经是 Cil 代码（在您的屏幕截图中省略）：

要获得屏幕截图中指示的弹出菜单，您需要突出显示一个语句，而不仅仅是一个表达式。请注意，在屏幕截图中，整个 p = T; 语句被突出显示。否则，上下文菜单不会显示“影响分析”项。

在 Frama-C GUI 中选择语句的一种简单方法是在分号之后单击 。如果是赋值语句，如上图，也可以点击等号选择语句。但是，如果您直接单击p 或T，您将只选择与这些变量对应的表达式。由于 Impact 是基于语句而不是表达式，因此在这种情况下它不会显示其上下文菜单。

顺便说一句，如果您想检查某个给定的插件是否在您的 Frama-C 安装中可用，您可以简单地运行 frama-c -plugins 以获取已安装插件的列表，或者在GUI（菜单分析/分析），每个插件包含一个条目。

编辑：在使用 VM 进行测试后，我意识到 Ubuntu 14.04 (Trusty) 的软件包中包含 Frama-C Fluorine（从 2013 年开始），这是一个非常旧的版本，确实具有影响插件，但由于某种原因，当时它并未包含在 Debian 软件包中（这就是您无法使用它的原因）。 Frama-C 正在迅速发展，因此使用这样的旧版本会导致几个问题。我真的建议尝试通过 OPAM 安装它。