如何在 Ubuntu 14.04 上安装 Frama-c 的影响分析插件？
How to install Impact Analysis Plug-in for Frama-c on Ubuntu 14.04?
我在 Ubuntu 14.04 上安装了 Frama-c，使用以下命令：
sudo apt-get install frama-c
但是，当我使用以下命令打开 frama-c 的 GUI 时：
frama-c-gui
我在左侧 window 找不到 "Impact Analysis" 插件。
下图是我的Frama-c目前可用的插件：
我也提到了 Frama-c web page 但找不到任何链接供我下载或安装影响分析插件。
如何在 Ubuntu 14.04 上启用和使用影响分析？
自 Neon-20140301 版本以来，Impact 插件已随 Frama-C 安装，您无需执行任何特殊操作即可启用它，只需 select 一条语句并找到正确的上下文菜单激活它。
来自您提到的 Frama-C 网页（以粗体突出显示相关部分）：
Impact analysis is available through a contextual menu at each statement in the Frama-C graphical user interface.
屏幕截图的左侧 window 包含 filetree（上半部分，包含文件名和全局 variables/functions）和一个列表插件面板的数量，对于那些注册了自己的 GUI 面板的插件。请注意，并非所有插件都有关联的面板；例如，Impact 是一个只能通过上下文菜单使用的插件。
仔细观察Frama-C网站上的Impact插件页面，您会发现显示的屏幕截图中不包括您屏幕截图中的GUI部分，而是左侧部分已经是Cil 代码（在您的屏幕截图中省略）：
要获得屏幕截图中指示的弹出菜单，您需要突出显示 语句，而不仅仅是一个表达式。请注意，在屏幕截图中，整个 p = T; 语句被突出显示。否则，上下文菜单将不会显示 "Impact analysis" 项。
在 Frama-C GUI 中 select 语句的一种简单方法是单击 在 分号之后。如果是赋值语句，如上图，也可以点击等号select语句。但是，如果您直接单击 p 或 T，您将只 select 对应于这些变量的表达式。因为 Impact 基于语句而不是表达式，所以在这种情况下它不会显示其上下文菜单。
顺便说一句，如果您想检查给定的插件是否在您的 Frama-C 安装中可用，您可以简单地 运行 frama-c -plugins 来获取已安装插件的列表ins，或打开 GUI 中的分析面板（菜单 Analyses/Analyses），每个插件包含一个条目。
编辑：在用虚拟机测试后，我意识到 Ubuntu 14.04 (Trusty) 的包中有 Frama-C Fluorine (from 2013)，这是一个非常旧的版本，确实有 Impact 插件，但出于某种原因它当时没有包含在 Debian 软件包中（这就是你不能使用它的原因）。 Frama-C 正在迅速发展，因此使用这样一个旧版本会导致几个问题。我真的建议尝试通过 OPAM 安装它。
我在 Ubuntu 14.04 上安装了 Frama-c，使用以下命令：
sudo apt-get install frama-c
但是，当我使用以下命令打开 frama-c 的 GUI 时：
frama-c-gui
我在左侧 window 找不到 "Impact Analysis" 插件。
下图是我的Frama-c目前可用的插件：
我也提到了 Frama-c web page 但找不到任何链接供我下载或安装影响分析插件。
如何在 Ubuntu 14.04 上启用和使用影响分析？
自 Neon-20140301 版本以来，Impact 插件已随 Frama-C 安装，您无需执行任何特殊操作即可启用它，只需 select 一条语句并找到正确的上下文菜单激活它。
来自您提到的 Frama-C 网页（以粗体突出显示相关部分）：
Impact analysis is available through a contextual menu at each statement in the Frama-C graphical user interface.
屏幕截图的左侧 window 包含 filetree（上半部分，包含文件名和全局 variables/functions）和一个列表插件面板的数量，对于那些注册了自己的 GUI 面板的插件。请注意，并非所有插件都有关联的面板；例如，Impact 是一个只能通过上下文菜单使用的插件。
仔细观察Frama-C网站上的Impact插件页面，您会发现显示的屏幕截图中不包括您屏幕截图中的GUI部分，而是左侧部分已经是Cil 代码（在您的屏幕截图中省略）：
要获得屏幕截图中指示的弹出菜单，您需要突出显示 语句，而不仅仅是一个表达式。请注意，在屏幕截图中，整个 p = T; 语句被突出显示。否则，上下文菜单将不会显示 "Impact analysis" 项。
在 Frama-C GUI 中 select 语句的一种简单方法是单击 在 分号之后。如果是赋值语句，如上图，也可以点击等号select语句。但是，如果您直接单击 p 或 T，您将只 select 对应于这些变量的表达式。因为 Impact 基于语句而不是表达式，所以在这种情况下它不会显示其上下文菜单。
顺便说一句，如果您想检查给定的插件是否在您的 Frama-C 安装中可用，您可以简单地 运行 frama-c -plugins 来获取已安装插件的列表ins，或打开 GUI 中的分析面板（菜单 Analyses/Analyses），每个插件包含一个条目。
编辑：在用虚拟机测试后，我意识到 Ubuntu 14.04 (Trusty) 的包中有 Frama-C Fluorine (from 2013)，这是一个非常旧的版本，确实有 Impact 插件，但出于某种原因它当时没有包含在 Debian 软件包中（这就是你不能使用它的原因）。 Frama-C 正在迅速发展，因此使用这样一个旧版本会导致几个问题。我真的建议尝试通过 OPAM 安装它。