lclint-interest message 65
From email@example.com Fri Mar 29 18:39:27 1996
Date: Fri, 29 Mar 1996 16:30:40 -0500
From: Eric Bloodworth
Organization: Recognition Research, Inc
X-Mailer: Mozilla 2.01 (X11; I; AIX 2)
To: David Evans
Subject: Re: can lclint detect this leak?
Content-Type: text/plain; charset=us-ascii
David Evans wrote:
> 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
> the implementation.
> /*@defines x->elements@*/
> 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.
> /*@allocates x->stuff@*/
> Same as defines, except storage is allocated but not
> /*@releases x->name@*/
> 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)
> /*@allocates stuff->bar@*/
> or /*@allocates *stuff@*/ [ semantics of this might be unclear? ]
> extern int free_booga_s (/*@special@*/ booga_s *stuff)
> /*@releases stuff->bar@*/
> 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
> --- Dave
You should consider improving support for internal storage (reference: LUG 5.2.7)
It's unreasonable to require an existing API's types to be changed just to
annotate inner storage. Example:
/* this function returns and int * in resp which is read-only */
int foo(/*@special@*/ int **resp) /*@observer *resp@*/;
It would be ideal if you could apply of the usual suspects (out, only, dependent, observer, etc)
to arguments in this fashion, in addition to the ones you defined above.
University of Virginia, Computer Science