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) == 0 should be assumed? The patch below seems to do it. Ken ---------------- file m3.c #include <stdio.h> struct sockaddr; typedef size_t socklen_t; extern int getnameinfo (const struct sockaddr *addr, socklen_t addrsz, /*@out@*/ /*@null@*/ char *h, socklen_t hsz, /*@out@*/ /*@null@*/ char *s, socklen_t ssz, int flags) /*@requires (maxSet(h)+1) >= hsz /\ (maxSet(s)+1) >= ssz @*/ /*@modifies *h, *s@*/; void f (struct sockaddr *sa, socklen_t salen) { char hbuf[2000]; int r; /*13*/ r = getnameinfo (sa, salen, hbuf, (socklen_t) sizeof (hbuf), 0, 0, 0); if (r == 0) printf ("%s\n", hbuf); } ---------------- output % splint +bounds m3.c Splint 3.0.1.6 --- 25 May 2002 m3.c: (in function f) m3.c:13:9: Possible out-of-bounds store: getnameinfo(sa, salen, hbuf, (socklen_t)sizeof((hbuf)), 0, 0, 0) Unable to resolve constraint: requires maxSet(0) >= -1 needed to satisfy precondition: requires maxSet(0) >= -1 derived from getnameinfo precondition: requires maxSet(<parameter 5>) + 1 >= <parameter 6> A memory write may write to an address beyond the allocated buffer. (Use -boundswrite to inhibit warning) Finished checking --- 1 code warning % ---------------- patch --- constraintExpr.c~ Wed Jan 9 01:07:43 2002 +++ constraintExpr.c Sun May 26 03:25:00 2002 @@ -1359,6 +1359,21 @@ BADEXIT; } + if (constraintTerm_isIntLiteral(cterm) ) + { + if (constraintTerm_getValue(cterm) == 0) + { + /* Null pointers indicate no readable or settable storage. */ + constraintExpr temp; + + temp = constraintExpr_makeIntLiteral (0); + constraintExpr_free(c); + constraintExpr_free(exp); + + return temp; + } + } + /* slight Kludge to hanlde var [] = { , , }; ** type syntax I don't think this is sounds but it should be good ** enough. The C stanrad is very confusing about initialization