Odd Behavior From Splint Bounds Checking

Question

Any splint experts out there?? I'm trying to use splint to statically analyze a large project I have in C. I'm seeing an excess number of bounds checking errors that are obviously not bounds errors. I wrote a small test program to try to isolate the problem, and noticed some really strange warnings when I ran splint on the code. I have 3 different examples. Here is the first:

int arr[3];

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

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

    return 0;
}

The arr[3] assignment generates a warning when using +bounds as I would expect, but does nothing when I use +likely-bounds. What does +likely-bounds even do? It seems to not work. The second example:

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;
}

In this example splint complains that I'm reading outside the bounds of the array ("A memory read references memory beyond the allocated storage.") for var = arr[i], even though I'm obviously not. This should be a warning because the values in array are not initialized, but that's not the warning I get. Initializing the last value in the array will clear the error (but initializing the first or second won't). Am I doing something wrong? In the third example:

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;
}

A warning is generated for arr[3] = 0, but not var = arr[i], even though it's obvious that the loop goes outside the bounds of the array. It looks like writing to the end of an array expands how large splint thinks the array is. How is that possible?

In short my questions are:

1. What does the likely-bounds flag do?
2. Is there any way that I can make splint give me legitimate errors that relate to going out of bounds?
3. Is there any way to make splint not increase the size of arrays that are accessed past their bounds? Right now splint is reporting more than 750 warnings and I don't have time to verify each warning one by one.

Answer 1

Up front: I do not know 'splint', but I know the techniques quite well from using PC Lint intensively, and discussing several issues with its makers.

That said:

• In your first example, the arr[3] is only flagged with +bounds propably because the element one past the last is a special case: It is allowed to create and use a pointer to the element one past the last, but it is not allowed to dereference such a pointer. Therefore, in syntax checkers (QA-C as well) it happens quite frequently that such warnings are less severe for N+1. Did you try arr[4]? My guess is, +likely_bounds will be sufficient for that.
• The second example probably is caused by a somewhat confused 'splint'. I have seen similar errors in early versions of PC Lint and QA-C, since "value tracking" is far from easy. However, I cannot tell why split is complaining.
• Your third example, 'splint' is correctly complaining about initializing arr[3], but for value tracking purposes it then has assumed arr[3] to be valid, and refrains from complaining about the loop. I'd guess you could initialize arr[100] and let the loop run until 100 without complaint!