> Op 24-okt-2009, om 21:19 heeft Bill Pringlemeir het volgende geschreven:

>> I am not also sure why fopen() isn't annotated with /*...@owned@*/?
>> Also, commenting out the 'fclose()' line doesn't seem to give me an
>> error.  This is the whole point of this tracking.  The /*...@owned@*/
>> annotation is the better choice as it indicated that the fopen()
>> return value must be closed.

On 24 Oct 2009, d.jan...@cs.ru.nl wrote:

> A possible implementation of fopen() has statically allocated  
> buffers, and fopen() would then return a pointer to one of them. In
> these implementations, fopen() cannot have type /*...@owned@*/.

Hmm.  You can implement malloc this way as well.  The fact is that the
memory region [or file] is owned by the caller of malloc() [or
fopen()].  They return it to a pool by calling free() [or fclose()].
At the allocator level, everything is static; you only have as much
memory as the system has.

> Additionally, the C standard explicitly states that files are closed
> upon calling exit(), so the user is not required to close them  
> himself. (Although splint will not complain if the files are closed  
> by exit(), as this syntactically is just a function call.)

The same can be said for memory allocate with malloc().  sbrk() and
friends will associate the memory for a process and the OS/kernel
should reclaim any tables associated with them when the process exits.

I think that most people would like unmatched fopen()/fclose() calls
to be flagged.  It is a design choice to depend on this.  Some people
believe that malloc() should be wrapped and call exit() if memory is
exhausted.  If someone did an analysis of the memory usage, this might
be a valid strategy.  However, for many designs code should free
memory that is allocated.  I think the same can be said for file,
sockets, etc.

I have debugged problems where the code had opened 1024+ files in a
production environment.  It went through several years of QA and no
one detected this issue.  Other people had implemented sanity checks
in legacy code and if a condition didn't work the process would exit
to be re-spawned by inittab/crontab.  The code was turned into a SOA
service and this behavior was no longer acceptable.  I think it is
useful to have a tools that would detect files opened, but not closed.

I can see that some designs wouldn't care about this.  I also think
that it would be least surprising for splint to detect this and if a
design relies on exit() to close files, an annotation would be good
documentation of this fact.

> Finally, I can find discussions on the web that suggest that fclose 
> (stdout) is legal.

Yes,  I think that stdin/stdout/stderr would have to be flagged as
initialized somehow.  However, that is a separate issue isn't it?

Thanks,
Bill Pringlemeir.

-- 
Someday we'll look back on all this and plow into a parked car.
_______________________________________________
splint-discuss mailing list
splint-discuss@mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss

Reply via email to