我使用以下命令在 Ubuntu 14.04 上安装了 Frama-c:
sudo apt-get install frama-c
但是,当我使用以下命令打开 frama-c 的 GUI 时:
frama-c-gui
我在左侧窗口中找不到“影响分析”插件。
我还参考了Frama-c 网页,但找不到任何链接供我下载或安装影响分析插件。
如何在 Ubuntu 14.04 上启用和使用影响分析?
我使用以下命令在 Ubuntu 14.04 上安装了 Frama-c:
sudo apt-get install frama-c
但是,当我使用以下命令打开 frama-c 的 GUI 时:
frama-c-gui
我在左侧窗口中找不到“影响分析”插件。
我还参考了Frama-c 网页,但找不到任何链接供我下载或安装影响分析插件。
如何在 Ubuntu 14.04 上启用和使用影响分析?
从 Neon-20140301 版本开始,Impact 插件已经与 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 年开始),这是一个非常旧的版本,确实有 Impact 插件,但由于某种原因它是当时未包含在 Debian 软件包中(这就是您无法使用它的原因)。Frama-C 正在迅速发展,因此使用这样的旧版本会导致几个问题。我真的建议尝试通过 OPAM 安装它。