[splint-discuss] Dependency on run time function

[Richard A. O'Keefe]

On 31 Mar 2008, at 5:39 pm, Vishal Bayskar wrote:
> After read I have checked the len
> And execution only go to the hdr.member if read was successful
>
Good.  However, splint is an extended lint checker, not a program
verifier.  It's not "smart" enough to figure out the safety of this
code by itself.
>
> len = read (sockfd, &hdr, sizeof (HEADER));
>
> if (len < (ssize_t)sizeof (HEADER)) {
> 	return 1;
> }

Perhaps inadvertently, splint is still drawing your attention to
this code, which is still warranted, because it is still wrong,
but for a different reason.

Now the reason it is wrong is that just because read() returned less
than you asked for, that *doesn't* mean there will never be any more.
With disc files, this is probably so.  With terminals, pipes, sockets,
and several other kinds, it is definitely NOT so.  This means that
your program might give up when it could have succeeded.  (It's hard
to tell, because it can depend on a whole bunch of other things that
are not apparent in this code snippet, neither to splint nor to me.)

 From the name 'sockfd' I surmise that you are reading from a socket.
POSIX says that in that case, read() is equivalent to a call to recv()
with no flags set.  One of the flags you can set in recv() -- but not
in read() -- is MSG_WAITALL, available for SOCKS_STREAM sockets,
which says to wait until _all_ of the requested bytes are available.
	r = recv(sockfd, hdr, sizeof hdr, MSG_WAITALL);
may well be what you want.

Of course, splint probably doesn't know enough about this either,
so whatever you do you will have to help splint out at this point.

You probably already know about the /*@i@*/ annotation which
switches off error reporting until the end of the line.  I'd be
inclined to do something like

#ifdef S_SPLINT_S

static ssize_t receive_header(/*@unused*/ int sockfd, HEADER /*@out@*/  
*hdr) {
     static HEADER const dummy_header = {/* you know what to put here  
*/};

     *hdr = dummy_header;
     return -1;
}

#else

#define receive_header(sockfd, hdr) recv(sockfd, hdr, sizeof *hdr,  
MSG_WAITALL)

#endif

and then change

	len = read(sockfd, hdr, sizeof (HEADER));

to

	len = receive_header(sockfd, &hdr);