frama-c - Frama-C EVA插件中“后”栏的含义和目的是什么

Question

在EVA 教程中，我找到了这个屏幕截图：带有解释：“导致这种情况的确切值显示在 c5 列中：-1。C 标准将负数的左移视为未定义行为。因为 -1 是此调用堆栈中唯一可能的值，由警报引起的减少导致后状态为 ."

所以，我想问：

Frama-C EVA插件中“后”栏的含义和目的是什么？

是否有更详细的文件来理解 EVA 中使用的“减少”和“后状态”一词？

Answer 1

当您s在 GUI 中选择一条语句时，有两种相关的内存状态：一种是之前s（也称为前状态），另一种是在副作用s完成之后（也称为后状态）。这就是为什么您在选项卡中为您感兴趣的每个 lval 提供两列的原因Values。前状态和后状态的概念在程序验证中是相当标准的，并且基本上可以追溯到Hoare Logic。

术语“减少”是指在发出警报后，EVA 将尝试从其抽象状态中删除与肯定会导致未定义行为的具体状态相对应的元素。实际上，抽象状态应该是所有具体状态的过度近似，这些具体状态可以在没有事先触发未定义行为的情况下到达语句：如果之前发生过失败s，那么推测在评估​​时会发生什么是没有意义的s。在您引用的示例中，我们有一个特殊情况，所有可能的具体状态都会导致错误。因此，我们以BOTTOM抽象状态结束，表示一组空的具体状态，对该分支的分析结束。