frama-c - 在 Frama-C 中使用影响分析

Question

我尝试使用frama-c-gui并能够执行影响分析但我无法弄清楚我们如何传递需要在 Frama-C 的批处理模式下执行影响分析的语句编号。

Answer 1

您可以使用一个特殊的注释//@ impact pragma stmt;来表明您对注释后面的语句的影响感兴趣。然后，如果该注释在 function 中f，您可以使用以下命令行在命令行上打印受影响的代码：

frama-c -impact-pragma f -impact-slicing impact.c -then-on "impact slicing" -print

• -impact-pragma f表示您对函数中的 pragma 标记的语句感兴趣f
• -impact-slicing表示您要创建一个名为的项目impact slicing，其中包含受您选择的语句影响的语句。
• -then-on "impact-slicing"让你继续对项目进行分析impact slicing（这里我们只是-print代码，但你可以在后面放任何你喜欢的选项-then-on project_name）

但是请注意，该impact插件是相当实验性的。