frama-c - Frama-C EVA插件中 "after"列的含义和用途是什么

Question

在 EVA tutorial ，我找到了这个截图:并解释:“导致此问题的确切值显示在列 c5 中:-1。C 标准将负数的左移视为未定义行为。因为 -1 是此调用堆栈中唯一可能的值，因此减少由警报引起的后状态是 。”

所以，我想问:

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

有没有更详细的文档来理解EVA中使用的“还原”和“后状态”这个词？

Answer 1

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

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