static-analysis - 溢出检查 Frama-C 的无效断言

Question

在为添加操作检查 short 和 char 数据类型的溢出时，Frama-C 插入的断言似乎不正确:

对于char和short数据，最大正负值都是整数数据类型。

这可能是什么原因？

Answer 1

小于 int 的整数类型在用于算术运算时被转换为 int 或 unsigned(参见 C11 6.3.1.8通常的算术转换)。这就是您看到 x 和 y 转换为 (int) 的原因。请注意，默认情况下 -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;
}

不会有任何沮丧警告(但会出现签名溢出警告)。