Frama-C EVA插件中"后"列的含义和目的是什么？

Question

在EVA教程中,我找到了这个截图: 解释:"导致这一点的确切值显示在第c5列:-1.C标准将负数的左移视为未定义的行为.因为-1是此callstack中唯一可能的值,所以减少由警报引起的后状态就是这样."

所以,我想问:

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

有没有更详细的文件来理解EVA中使用的术语"减少"和"后状态"？

Answer 1

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

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