为什么Eva插件可以计算出“(a >> 15) & 1”却不能计算出“(a >> 0) & 1”？

Question

我正在尝试使用 Frama-C 的 Eva 插件分析 C 源代码。

在下面的例子中，我发现Eva可以计算右边大的shift表达式的值，但是右边小的时候就不能计算了。

extern unsigned char a;
int main() {
    int b, c, d;
    b = (a >> 15) & 1;

    c = (a >> 0) & 1;

    d = b + c;
}

在上面的这个例子中，Eva 可以计算出 b 但不能计算出 c 的值。 (a >> 0) & 1 对 Eva 来说是否比 (a >> 15) & 1 更复杂？

Answer 1

Eva 从初始上下文中给出了最精确的答案，其中外部变量 a 在 [0..255] 范围内，即 b 等于 [=13] =] 和 c 可以是 0 或 1.

如果您想探索正在发生的事情，图形用户界面底部的 Values 面板（与 frama-c-gui -eva file.c 一同推出）是最佳选择。它的用法记录在 the Eva user manual 的第 4.3 节中，但基本上如果您单击规范化代码视图（左侧缓冲区）中的任何（子）表达式，此时 Eva 为该表达式计算的抽象值将显示在面板中。

在您的示例中，我们有以下用于计算 b 的中间值：

a -> [0..255]
(int)a -> [0..255]（算术操作数的隐式提升）
(int)a >> 15 -> {0}（只有前 8 位可能是非 0）
(int)a >> 15 & 1 -> {0}（第一个参数是0，按位也是0}

对于c，前两步是一样的，但是接下来我们有

(int)a >> 0 -> [0..255]（no-op，我们的值与 (int)a 相同）
((int)a >> 0) & 1 -> {0; 1}（在区间 [0..255] 中，我们有奇数和偶数，因此按位和的结果可以是 0 或1).

为什么Eva插件可以计算出“(a >> 15) & 1”却不能计算出“(a >> 0) & 1”？

Why can Eva plugin calculate "(a >> 15) & 1" but cannot calculate "(a >> 0) & 1"?

frama-c