buffer sizes and null pointers

[Ken Raeburn]

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