从夹板边界检查的奇怪行为

Question

任何夹板专家在那里？我试图用夹板静态分析大量的项目,我有C.我看到过多数量的边界检查显然不能界失误的错误.我写了一个小测试程序试图找出问题,并在我对代码运行splint时注意到一些非常奇怪的警告.我有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]仅用+boundspropproply 标记，因为最后一个元素是一种特殊情况：允许创建和使用指向最后一个元素的指针，但不允许取消引用这样的指针。因此，在语法检查器（以及 QA-C）中，经常会发生这样的警告对于 N+1 来说不太严重的情况。你试过了吗arr[4]？我的猜测是，+likely_bounds就足够了。
• 第二个例子可能是由有点混乱的“夹板”引起的。我在 PC Lint 和 QA-C 的早期版本中看到了类似的错误，因为“价值跟踪”远非易事。然而，我不知道为什么 split 会抱怨。
• 您的第三个示例“splint”正确地抱怨初始化arr[3]，但出于价值跟踪的目的，它假设arr[3]是有效的，并且避免抱怨循环。我猜你可以初始化arr[100]并让循环运行到 100 而不抱怨！