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