Недопустимое утверждение для проверки переполнения Frama-C

При проверке переполнения для типов данных short и char для операции добавления утверждения, вставленные Frama-C, кажутся неверными:

введите здесь описание изображения

Для char и коротких данных максимальные положительные и отрицательные значения имеют целочисленный тип данных.

Что может быть причиной этого?


static-analysis frama-c
person karan    schedule 05.10.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Целочисленные типы ранга меньше int преобразуются либо в int, либо в unsigned при использовании в арифметической операции (см. C11 6.3.1.8 Обычные арифметические преобразования). Вот почему вы видите приведение к (int) для x и y. Обратите внимание, что по умолчанию -rte не будет выдавать предупреждение о приведении вниз, поскольку они не являются неопределенным поведением (6.3.1.3§3 указывает, что подписанное преобразование вниз определяется реализацией и что реализация может вызвать сигнал). Если вы добавите опцию -warn-signed-downcast, вы увидите утверждения, которые вы, вероятно, искали, из-за приведения результата к (char):

/*@ assert rte: signed_downcast: (int)x+(int)y ≤ 127; */
/*@ assert rte: signed_downcast: -128 ≤ (int)x+(int)y; */

Обратите внимание, что если вы сохраните результат в int, как в

void main(void) {
    char x;
    char y;
    int z;
    x = 1;
    y = 127;
    z = x + y;
    return;
}

Предупреждения о переполнении не будет (но будут присутствовать подписанные предупреждения о переполнении).

person Virgile    schedule 05.10.2016