夹板边界检查的奇怪行为

Question

那里有夹板专家吗？我正在尝试使用夹板静态分析我在 C 中拥有的大型项目。我看到过多的边界检查错误显然不是边界错误。我编写了一个小测试程序来尝试隔离问题，并在对代码运行夹板时注意到一些非常奇怪的警告。我有3个不同的例子。这是第一个：

int arr[3];

int main(void)
{
    int i;
    int var;

    arr[3] = 0; // (1) warning with +bounds, no warning with +likely-bounds

    return 0;
}

arr[3] 分配在使用 +bounds 时会产生警告，但当我使用 +likely-bounds 时不会执行任何操作。 +likely-bounds 还能做什么？它似乎不起作用。第二个例子：

int arr[3];

int main(void)
{
    int i;
    int var;

    for (i = 0; i < 3; i++)
        var = arr[i]; // (2) warning, even though I'm within the bounds.

    return 0;
}

在此示例中，splint 抱怨我正在读取数组边界之外的内容（“内存读取引用了分配存储之外的内存。”）var = arr[i]，尽管我显然不是。这应该是一个警告，因为数组中的值没有初始化，但这不是我得到的警告。初始化数组中的最后一个值将清除错误（但初始化第一个或第二个不会）。难道我做错了什么？在第三个例子中：

int arr[3];

int main(void)
{
    int i;
    int var;

    arr[3] = 0; // warning

    for (i = 0; i < 4; i++)
        var = arr[i]; // (3) no warning because arr[3] = 0 statement.

    return 0;
}

会为arr[3] = 0 生成警告，但不会为var = arr[i] 生成警告，即使循环显然超出了数组的边界。看起来写入数组末尾会扩展夹板认为数组的大小。这怎么可能？

简而言之，我的问题是：

1. 可能边界标志有什么作用？
2. 有什么方法可以让夹板给我与越界相关的合法错误？
3. 有什么方法可以使夹板不会增加超出其界限的数组的大小？目前 splint 报告了 750 多个警告，我没有时间逐个验证每个警告。

Answer 1

预先说明：我不知道“夹板”，但通过深入使用 PC Lint 并与制造商讨论几个问题，我非常了解这些技术。

也就是说：

• 在您的第一个示例中，arr[3] 仅被标记为 +bounds，可能是因为最后一个元素是一种特殊情况：允许创建和使用指向最后一个元素的指针，但是不允许取消引用这样的指针。因此，在语法检查器（QA-C 也是如此）中，这种警告对于 N+1 不太严重的情况经常发生。你试过arr[4]吗？我的猜测是，+likely_bounds 就足够了。
• 第二个例子可能是由有点混乱的“夹板”引起的。我在 PC Lint 和 QA-C 的早期版本中看到了类似的错误，因为“价值跟踪”远非易事。但是，我不知道为什么 split 会抱怨。
• 您的第三个示例“夹板”正确地抱怨初始化arr[3]，但出于价值跟踪目的，它假设arr[3] 有效，并避免抱怨循环。我猜你可以初始化 arr[100] 并让循环运行到 100 没有抱怨！