【发布时间】：2014-04-22 15:13:57
【问题描述】：
我尝试使用frama-c-gui 并且能够执行影响分析
但我无法弄清楚我们如何传递需要在 Frama-C 的批处理模式下执行影响分析的语句编号。
【问题讨论】：
标签： frama-c
【发布时间】：2014-04-22 15:13:57
【问题描述】：
有一个特殊的注解//@ impact pragma stmt;，您可以使用它来表明您对注解后面的语句的影响感兴趣。然后，如果该注释在函数f 中，您可以使用以下命令行在命令行上打印受影响的代码：
frama-c -impact-pragma f -impact-slicing impact.c -then-on "impact slicing" -print
-
-impact-pragma f表示您对函数f中的 pragma 标记的语句感兴趣 -
-impact-slicing表示您要创建一个名为impact slicing的项目，其中包含受您选择的语句影响的语句。 -
-then-on "impact-slicing"让你继续对项目impact slicing进行分析（这里我们只写-print代码，但你可以在-then-on project_name后面放任何你喜欢的选项）
但请注意，impact 插件是相当实验性的。
【讨论】：
-
谢谢它的帮助。但是它只执行过程内影响分析，是否有任何选项可用于影响插件的过程间分析，可以帮助我们在源代码中提供我们想要进行影响分析的确切行号？还有是否可以获得受影响语句的源代码行号？
-
据我所知，默认情况下影响是跨程序的。选项
-impact-not-in-callers将阻止调用者中的分析，但默认不激活。 -
此外，如果您想打印受影响语句的位置，您必须编写一个小脚本来执行此操作。在
impact slicing项目和Cil_datatype.Stmt.loc函数上使用访问者，这应该不会太难。有关 Frama-C 脚本的更多信息，请参阅 Frama-C 的开发人员手册 (frama-c.com/download/plugin-development-guide-Neon-20140301.pdf)。