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
I'm trying to annotate getnameinfo, which takes among its inputs two
buffer pointers and their lengths. Each buffer pointer can be null if
the supplied length for it is zero.
I don't see a way to indicate that a maxSet relationship need only
hold if the size is nonzero. Perhaps maxSet(NULL) ==
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
