[splint-discuss] Dependency on run time function

[Richard A. O'Keefe]

On 30 Mar 2008, at 7:54 pm, Vishal Bayskar wrote:
> In my program a variable is initializing by read command

> len = read (sockfd, &hdr, sizeof (HEADER));
>
> And Splint is showing warning
>
> Field hdr.member used before definition

Splint is right.  The problem is that read() does NOT have to return
all you asked for.  By the way, I prefer

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

because that way it is *certain* that the size is the right size.
Anyway, if nothing goes wrong, you'll get 0 <= len <= sizeof (HEADER).
The most you can be sure of is that if all goes well and you didn't
reach the end of the file, you will get at least one byte.  But that
is ALL you can assume from read(), especially from a socket.

So Splint is quite right to warn you that the read() call might NOT
initialise the whole of hdr; it really truly might not.

It's nothing to do with "runtime" as such, it's to do with what
might *happen* (or not happen) at run time.

As for gettimeofday(), it may be that Splint doesn't have an
/*out*/ annotation for it.  Did you check that?