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
