[splint-discuss] Dependency on run time function

[Vishal Bayskar]

Dear All,

After read I have checked the len

And execution only go to the hdr.member if read was successful 


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

if (len < (ssize_t)sizeof (HEADER)) {
	return 1;
}


if (hdr.member == 2)
{
	Printf("  Successful    \n");
}


Even then the warning is displaying



Thanks and Regards
 
Vishal Bayskar
 
Ext. no. 927
-----Original Message-----
From: splint-discuss-bounces at cs.virginia.edu
[mailto:splint-discuss-bounces at cs.virginia.edu] On Behalf Of Richard A.
O'Keefe
Sent: Monday, March 31, 2008 9:23 AM
To: Discussions about the Splint annotation-assisted static analysis
project
Cc: splint-discuss at mail.cs.virginia.edu
Subject: Re: [splint-discuss] Dependency on run time function

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?


_______________________________________________
splint-discuss mailing list
splint-discuss at mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss