Splint does not allow #defined constants to be used in function constraints unless
they are defined with the constant anotation.
For example in the code below after the line
#define SIZE 1024
you would add
/*@constant int SIZE=1024@*/
(In most other cases Splint does handle #defined constants correctly even if the the
constant annotation is not used.)
The version of splint in CVS has now been patched in print an error describing the
problem and suggestioning the constant annotation instead of crashing.
On Sat, Jun 29, 2002 at 04:01:14AM -0400, David Richard Larochelle wrote:
> 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
> >
>
