Splint unable to check maxSet on pointer to stack variable

Question

I have a program that does something like the following:

#include <stdio.h>
#include <stdlib.h>

int f(char *result)
{
    if (result != NULL)
    {
        *result = 'a';
    }
    return 0;
}

int main ()
{
    char s = 0;
    (void)f(&s);
    printf("f gave %c\n", s);
    return 1;
}

I pass a pointer to a function, dereference it, and store something. Splint reports that it is unable to resolve the maxSet(result) >= 0 constraint in f:

test.c: (in function f)
test.c:8:9: Possible out-of-bounds store: *result
    Unable to resolve constraint:
    requires maxSet(result @ test.c:8:10) >= 0
     needed to satisfy precondition:
    requires maxSet(result @ test.c:8:10) >= 0
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)

&s points to a single char on the stack, so it should have a maxSet of 1 without adding any annotations. Why is Splint complaining?

Answer 1

As far as I can tell, splint reports that it is unable to verify the constraint with any pointer that does not verifiably point to an actual buffer, or array. This seems odd, since there seems to be no reason why it couldn't treat a single variable equivalent to an array of 1, but it seems to be so.

For instance, with the following code:

int main (void)
{
    int a = 5;
    int b[1] = {6};
    int * pa = &a;
    int * pb = b;

    char c = (char) 0;
    char d[1] = {(char) 0};
    char * pc = &c;
    char * pd = d;

    *pa  = 6;       /*  maxSet warning  */
    *pb  = 7;       /*  No warning      */
    *b   = 8;       /*  No warning      */

    *pc = 'b';      /*  maxSet warning  */
    *pd = 'c';      /*  No warning      */
    *d  = 'd';      /*  No warning      */

    return 0;
}

splint gives the following output:

paul@thoth:~/src/sandbox$ splint -nof +bounds sp.c
Splint 3.1.2 --- 20 Feb 2009

sp.c: (in function main)
sp.c:15:5: Possible out-of-bounds store: *pa
    Unable to resolve constraint:
    requires maxSet(&a @ sp.c:7:16) >= 0
     needed to satisfy precondition:
    requires maxSet(pa @ sp.c:15:6) >= 0
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)
sp.c:19:5: Possible out-of-bounds store: *pc
    Unable to resolve constraint:
    requires maxSet(&c @ sp.c:12:17) >= 0
     needed to satisfy precondition:
    requires maxSet(pc @ sp.c:19:6) >= 0

Finished checking --- 2 code warnings
paul@thoth:~/src/sandbox$ 

where dereferencing the pointer to the first character of the (one element) array, and dereferencing the array name itself, both yield no errors, but dereferencing a pointer which just points to a single variable does, both for char and int. Seems like a curious behavior, but it's what it is.

Incidentally, in your f() function, you can't really reason about what result points to in main(). Although when you just look at these two functions in isolation, it seems obvious that result points to what ought to be a valid reference, as far as splint knows, a bunch more calls could be made to f from other translation units, and it has no idea what result might point to in those cases, so it just has to go by the information it has for f() in and of itself.

For instance, here:

static void f(char * pc)
{
    if ( pc ) {
        *pc = 'E';      /*  maxSet warning  */
    }
}

int main(void)
{
    char c[25] = "Oysters and half crowns.";
    *c = 'U';           /*  No warning      */

    f(c);

    return 0;
}

splint will warn about the assignment in f(), but not about the assignment in main(), for this very reason. If you annotate it, however, then it has enough information to figure it out:

static void f(char * pc) /*@requires maxSet(pc) >= 0; @*/
{
    if ( pc ) {
        *pc = 'E';      /*  No warning      */
    }
}

int main(void)
{
    char c[25] = "Oysters and half crowns.";
    *c = 'U';           /*  No warning      */

    f(c);

    return 0;
}

but even here, if you change c to a single char, you get the same problem described because splint won't verify that the annotated constraint is satisfied, so this:

static void f(/*@out@*/ char * pc) /*@requires maxSet(pc) >= 0; @*/
{
    if ( pc ) {
        *pc = 'E';      /*  No warning      */
    }
}

int main(void)
{
    char c;
    f(&c);              /*  maxSet warning  */

    return 0;
}

gives you this:

paul@thoth:~/src/sandbox$ splint -nof +bounds sp3.c
Splint 3.1.2 --- 20 Feb 2009

sp3.c: (in function main)
sp3.c:11:5: Possible out-of-bounds store: f(&c)
    Unable to resolve constraint:
    requires maxSet(&c @ sp3.c:11:7) >= 0
     needed to satisfy precondition:
    requires maxSet(&c @ sp3.c:11:7) >= 0
     derived from f precondition: requires maxSet(<parameter 1>) >= 0
  A memory write may write to an address beyond the allocated buffer. (Use
  -boundswrite to inhibit warning)

Finished checking --- 1 code warning
paul@thoth:~/src/sandbox$