Блог

Главная - Вопросы по программированию - Могу ли я пропустить утверждение eva при signed overflow?

Могу ли я пропустить утверждение eva при signed overflow?

#frama-c

#frama-c

Вопрос:

Пример кода:

 void main(){
    unsigned int x;
    x = 1U << 31;  // OK
    x = 1 << 31; // Sign overflowed
    return;
}

frama-c-gui -eva main.c:

 void main(void)
{
    unsigned int x;
    x = 1U << 31;
    /*@ assert Eva: signed_overflow: 1 << 31 ≤ 2147483647; */
    x = (unsigned int)(1 << 31);
    return;
}

Получить красный сигнал тревоги из-за подписанного переполнения в строке 4. У меня есть существующий код с тонной аппаратных регистров, определенных с помощью битов маски и сдвигающих битов, подобных этому. Неразумно изменять код, добавляя «U» для всех битов маски. Есть ли в плагине eval опция для обработки этих констант как целых чисел без знака?

Ответ №1:

В ядре есть несколько опций для управления тем, какие типы аварийных сигналов должны выдаваться (см. frama-c -kernel-h или руководство, особенно его раздел 6.3, для получения дополнительной информации).

В вашем конкретном случае вас, вероятно, интересует -no-warn-signed-overflow , это отключит сигналы тревоги, связанные с переполнениями в арифметике со знаком. Затем Eva примет арифметику с двумя дополнениями и выдаст предупреждение об этом, если возникнет ситуация, но только один раз за весь анализ.