Null pointers and buffer sizes are a tricky issue. The bounds checking code isn't to detect bounds accesses of null pointers. (There is of course separate null terminated checking in splint.)
There are enough library function that use the convention maxSet(ptr) > N or ptr == NULL. I think that the patch you submitted is probably reasonable solution. We need to do some house cleaning with the splint code first, but I should be able to add the patch to the cvs tree soon. The maxSet(NULL) = 0 and maxRead(NULL) = 0 probably makes more sense since other splint checking would catches cases of dereferencing a null pointer. > I wrote: > > I don't see a way to indicate that a maxSet relationship need only > > hold if the size is nonzero. Perhaps maxSet(NULL) == 0 should be > > assumed? > > Nope, silly me, I keep thinking "how many" when I should be thinking > "max index", so 0 is no good, it means one location can be set. > Perhaps -1? Changing the literal value constructed in my patch still > produces a version that accepts my test case. > > Ken >
