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

I am trying to analyze a C source code using Eva plugin of Frama-C.

In the following example, I found that Eva can calculate the value of a shift expression in which the right-hand-side value is big, but cannot calculate when the right-hand-side value is small.

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

    c = (a >> 0) & 1;

    d = b + c;
}

In this example above, Eva can calculate the value of b but not c. Is (a >> 0) & 1 more complex than (a >> 15) & 1 to Eva?

Solution

Eva is giving the most precise answer from the initial context where a, an external variable, is in the range [0..255], namely that b is equal to 0 and c may be either 0 or 1.

If you want to explore what is going on, the Values panel at the bottom of of the graphical user interface (launched with frama-c-gui -eva file.c) is the way to go. Its usage is documented in section 4.3 of the Eva user manual, but basically if you click on any (sub)-expression in the normalized code view (the left buffer), the abstract value computed by Eva for this expression at this point will be displayed in the panel.

In your example, we have the following intermediate values for the computation of b:

a -> [0..255]
(int)a -> [0..255] (implicit promotion of an arithmetic operand)
(int)a >> 15 -> {0} (only the first 8 bits might be non 0)
(int)a >> 15 & 1 -> {0} (first argument is 0, the bitwise and is also 0}

For c, the first two steps are identical, but then we have

(int)a >> 0 -> [0..255] (no-op, we have the same values as (int)a)
((int)a >> 0) & 1 -> {0; 1} (in the interval [0..255], we have odd and even values, hence the result of the bitwise and can be either 0 or 1).