[splint-discuss] Buffer checking and loops

[Hollas Boris (CR/AEY1)]

Hello,

I've done some experiments to find out more about how buffer checking and the loop heuristics work. There are some things I don't fully understand yet. These are the observations I made and the questions I have about them:

- Splint reports a spurious out-of-bounds read in foo in the code below:

t2.c:18:3: Possible out-of-bounds read:
    foo(a)
    Unable to resolve constraint:
    requires maxRead(a @ t2.c:18:7) >= 2
     needed to satisfy precondition:
    requires maxRead(a @ t2.c:18:7) >= 2
     derived from foo precondition: requires maxRead(<parameter 1>) >= 2

However, I don't understand why this happens. From my understanding, a postcondition
maxRead(a) = 2
Is generated from the int a[3] declaration in main. Is this not checked between functions? How are function calls treated, are they replaced by their pre- and postconditions?

- On the other hand, splint reports "Passed storage a not completely defined (*a is undefined)" if I replace the for loop by an equivalent while loop:
  i=0;
  while(i<3) {
    a[i] = i;
    i++;
  }

  Are for and while loops treated differently or are for loops just easier to analyze for splint?

- Splint does not detect that a[2] is undefined if I change the loop bound to
for(i=0; i<1; i++)
Does that mean that splint sets array a[] to "defined" here?

-  While splint reports an out-of-bounds read for
for(i=0; i<5; i++)
It does not for
for(i=-10; i<2; i++)
Is the lower bound not checked for arrays?


Best regards,
Boris

--------------------------------------

void foo(/*@in@*/int *a)
/*@requires maxRead(a) >= 2@*/
{
  int i;

  i = a[2];
}


int main()
{
  int a[3];
  int i;

  for(i=0; i<3; i++)
    a[i] = i;

  foo(a);
  return 0;
}