Могу ли я пропустить утверждение Евы о подписанном переполнении?

Question

Пример кода:

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 возможность трактовать эти константы как целое число без знака?

Answer 1

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

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