maxRead()/Set() annotations

[Enrico Scholz]

Hello,

while trying to check the following program-fragment which copies the
content of one list into another one, splint generates bounds-checking
warnings.

The first one probably appears because 'src->elems[i]->data' may contain
uninitialized values. The

                 (maxRead(src->elems[].data)+1) == SIZE

in the @requires@ clause in line 20 does not help. I tried a helper
function 'getData()' (lines 10-14), but when using it by uncommenting
line 26, splint fails with an internal error:

| vec.c:33:2: *** Fatal bug: Invalid sRef
| *** Last code point: exprNode.c:10066
| *** Previous code point: exprNode.c:10066
|      *** Please report bug to [EMAIL PROTECTED] ***


The last two warnings are caused because splint can not derive 

                  maxSet(dst->elems)  >= i

from the

                  (maxRead(dst->elems)+1) >= src->cnt   (line 19)
and
                  i<src->cnt                            (line 24)

relations. I tried to give hints like 'assert(i<=src->cnt-1)' but the
warnings remain. 

How can I write the code so that it can be checked with splint?



------
     1  #include <string.h>
     2  #define SIZE    1024

     3  struct Data {
     4      char        data[SIZE];
     5  };
       
     6  struct Vector {
     7      /*@owned@*/struct Data      *elems;
     8      unsigned int                cnt;
     9  };
       
    10  char *getData(/*@returned@*/struct Data *dta)
    11      /*@ensures (maxRead(result)+1) == SIZE@*/
    12  {
    13    return dta->data;
    14  }
       
    15  void foo(struct Vector *dst,
    16           /*@in@*/struct Vector const *src)
    17      /*@modifies dst->elems@*/
    18      /*@requires (maxRead(src->elems)+1) == src->cnt
    19               /\ (maxRead(dst->elems)+1) >= src->cnt
    20               /\ (maxRead(src->elems[].data)+1) == SIZE
    21               @*/
    22  {
    23    unsigned int          i;
       
    24    for (i=0; i<src->cnt; ++i) {
    25      memcpy(dst->elems[i].data, src->elems[i].data, SIZE);
    26      //memcpy(getData(dst->elems+i), getData(src->elems+i), SIZE);
    27    }
    28  }
------

| $ splint +bounds vec.c 
| Splint 3.0.1.6 --- 17 Jun 2002
| 
| vec.c: (in function foo)
| vec.c:30:5: Possible out-of-bounds read:
|     memcpy(dst->elems[i].data, src->elems[i].data, 1024)
|     Unable to resolve constraint:
|     requires <undef> >= 1024
|      needed to satisfy precondition:
|     requires maxRead(src->elems[i].data @ vec.c:30:32) >= 1023
|      derived from memcpy precondition: requires maxRead(<parameter 2>) >=
|     <parameter 3> + -1
|   A memory read references memory beyond the allocated storage. (Use
|   -boundsread to inhibit warning)
| vec.c:30:12: Possible out-of-bounds read:
|     dst->elems[i]
|     Unable to resolve constraint:
|     requires maxRead(dst->elems @ vec.c:30:12) >= i @ vec.c:30:23
|      needed to satisfy precondition:
|     requires maxRead(dst->elems @ vec.c:30:12) >= i @ vec.c:30:23
| vec.c:30:32: Possible out-of-bounds read:
|     src->elems[i]
|     Unable to resolve constraint:
|     requires *(<parameter 2>).cnt >= i @ vec.c:30:43 + 1
|      needed to satisfy precondition:
|     requires maxRead(src->elems @ vec.c:30:32) >= i @ vec.c:30:43
| 
| Finished checking --- 3 code warnings




Enrico