在EVA tutorial 中，我找到了这个截图： 并有一个解释：“导致这种情况的确切值显示在 c5 列中：-1。C 标准将负数的左移视为未定义的行为。因为 -1 是此调用堆栈中唯一可能的值，所以由警报引起的减少会导致后状态为 。”
所以，我想问一下：
Frama-C EVA插件中“after”栏的含义和用途是什么？
有没有更详细的文档来理解EVA中使用的“reduction”和“post-state”这个词？
【问题讨论】：
当您在 GUI 中选择语句 s 时，有两种相关的内存状态：s 之前的一种（也称为预状态），以及s 的副作用之后的一种已经完成（也称为后状态）。这就是为什么您在 Values 选项卡中为您感兴趣的每个 lval 提供两列的原因。pre 和 post-state 的概念在程序验证中是相当标准的，基本上可以追溯到 Hoare Logic。
术语“减少”是指在发出警报后，EVA 将尝试从其抽象状态中删除与肯定会导致未定义行为的具体状态相对应的元素。实际上，抽象状态应该是所有具体状态的过度近似，可以达到语句事先没有触发未定义的行为：如果在s 之前发生故障，那么推测没有意义评估s 时会发生什么。在您引用的示例中，我们遇到了所有可能的具体状态都会导致错误的特殊情况。因此，我们最终得到了BOTTOM 抽象状态，代表了一个空的具体状态集，这个分支的分析就结束了。
【讨论】：