lclint-interest message 64
From evs Mon Mar 25 12:35:49 1996
Date: Mon, 25 Mar 96 12:14:47 -0500
From: evs (David Evans)
In-Reply-To: Eric Bloodworth's message of Sun, 24 Mar 1996 20:08:27 -0500 <3155F20B.167E@rrinc.com>
Subject: can lclint detect this leak?
Yes, I think you're right that some extensions to lclint to allow this
to be described would be worthwhile.
Currently, what I have in mind is to add a /*@special@*/ annotation on
parameters to indicate that none of the implicit assumptions apply to
storage derived from the parameter. Then clauses can be used to
describe derived storage. I think 4 clauses are needed:
/*@uses x->size, x->num@*/
References that are used in the implementation. Must be
defined before the call, assumed to be defined checking
References that are defined in all possible paths
through the implementation. Must not refer to allocated
storage before the call (or a memory leak), assumed to
be undefined checking the implementation, assumed to
be defined after the call returns.
Same as defines, except storage is allocated but not
References that are released in the implementation.
Must be allocated before the call, and a memory leak
is reported if it is not deallocated in the
implementation. After the call, the corresponding
reference is dead storage.
Then, you would be able to specify
extern int alloc_booga_s (/*@special@*/ booga_s *stuff)
or /*@allocates *stuff@*/ [ semantics of this might be unclear? ]
extern int free_booga_s (/*@special@*/ booga_s *stuff)
or /*@releases *stuff@*/
This would also have the advantage that instead of using /*@partial@*/
to indicate structure fields may not be defined on call but are checked
as though they are defined, programmers can explicitly specify what
fields are used and defined.
Perhaps, this should be extended to allow /*@special@*/ annotations on
the return value also, and use a special name (e.g., "result") to
specify the return values in the uses, defines, allocates, releases
I'm open to suggestions of alternate ways of doing this, especially with
respect to what kinds of (simple) things programmers would like to
specify about function interfaces that cannot be done with the current
lclint annotations, and I'll add something like this to an update
University of Virginia, Computer Science