I was able to verify the problem and I'll try to put together a patch for the internal
error in the next few days.
-David
On Thu, Jun 27, 2002 at 06:33:31PM +0200, Enrico Scholz wrote:
> 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
>
