小编Thu*_*yen的帖子

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

所以,我想问:

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

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