【发布时间】:2015-05-13 02:50:58
【问题描述】:
影响分析插件有一个方法切片,它根据影响分析对给定的语句进行切片。 是否像我们创建项目的切片插件然后我们选择切片区域并在将此区域添加到请求后?如何打印此影响分析切片的结果?
【问题讨论】:
-
有没有像切片插件这样的关卡,还是完全静态的?
-
我不确定我是否理解这条评论。
标签: frama-c
影响分析插件有一个方法切片,它根据影响分析对给定的语句进行切片。 是否像我们创建项目的切片插件然后我们选择切片区域并在将此区域添加到请求后?如何打印此影响分析切片的结果?
【问题讨论】:
标签: frama-c
函数Db.Impact.slice 实际上并没有真正链接到Impact 插件。它只是在给定的语句列表上计算切片请求,而无需在任何地方调用Impact。如您所见,您已经可以从 Slicing 的 API 构建此请求,而 Db.Impact.Stmt 不可自定义。
(这个函数slice应该是Impact的内部函数。当用户选择冲击后切片选项时,它会在GUI中使用。我们将在下一个版本中删除它以消除这种歧义。)
【讨论】: