溢出检查 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;
}

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

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

Invalid assertion for overflow check Frama-C

static-analysis

frama-c