如何在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安装它。