Почему плагин Eva может вычислить "(a >> 15) & 1", но не может рассчитать "(a >> 0) & 1"?

Question

Я пытаюсь проанализировать исходный код на C, используя плагин Eva Frama-C.

В следующем примере я обнаружил, что Eva может вычислить значение выражения сдвига, в котором значение правой части велико, но не может вычислить, когда значение правой части мало.

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 сложнее, чем (a >> 15) & 1 для Евы?

Answer 1

Ева дает наиболее точный ответ из исходного контекста, где a, внешняя переменная, находится в диапазоне [0..255], а именно, что b равно 0, а c может быть либо 0 или 1.

Если вы хотите узнать, что происходит, панель Values в нижней части графического интерфейса пользователя (запущена с frama-c-gui -eva file.c) - это путь.Его использование описано в разделе 4.3 руководства пользователя Eva , но в основном, если вы щелкаете по любому (под) выражению в представлении нормализованного кода (левый буфер), абстрактное значение, вычисленное 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] (нет, у нас те же значения, что и (int)a)
• ((int)a >> 0) & 1 ->{0; 1} (в интервале [0..255] мы имеем нечетные и четные значения, следовательно, результат побитовый и может быть либо 0, либо 1).