On Jan 16, 2010, at 10:12 AM, AlannY wrote:
> On Sat, Jan 16, 2010 at 09:03:47AM -0500, Jeff Johnson wrote:
>>
>> I', not seeing a specific question there ...
>>
>> ... but I can point you at a complete "real world" set of
>> annotations using splint /*...@refcounted@*/ and /*...@only@*/
>> (and /*...@abstract@*/ which is unique to splint).
>>
>> All of RPM development has used splint annotations for years. Grab
>> a tarball (perhaps rpm-5.1.7.tar.gz) from
>> http://rpm5.org/files/rpm/rpm-5.1
>>
>> There are annotations using /*...@refcounted@*/ throughout with naming like
>> rpmfooNew(), rpmfooLink()/rpmfooUnlink(), and rpmfooFree()
>> analogous to your example program.
>>
>> Note that splint helped immensely in getting a refcounted model
>> in place to attach a mutex protected refcount everywhere to
>> move to thread-safe objects.
>
> I've downloaded rpm's sources and inspect them. There are, for example,
> undocumented annotation @newref@, but I don't know what it do.
>
AFAIK /*...@newref@*/ indicates that the /*...@refs@/ variable has been
incremented.
> The problem is follow: when reference counter goes to zero and there are
> no more links to object, I should release space for this object.
>
> Example:
> void
> test_unref (/*...@killref@*/ /*...@only@*/ test t)
> {
> t->refcount--;
> if (t->refcount<=0)
> 20: free (t);
> }
>
> splint print 2 error messages, which confuses me:
>
> test.c:20:11: Reference counted storage passed as only param: free (t)
> Reference counted storage is transferred in a way that may not be consistent
> with the reference count. (Use -refcounttrans to inhibit warning)
> test.c:20:5: Variable t is released in true branch, but live in continuation.
> The state of a variable is different depending on which branch is taken. This
> means no annotation can sensibly be applied to the storage. (Use -branchstate
> to inhibit warning)
> test.c:20:5: in true branch:
> test.c:20:11: Storage t released
>
Yes. What I did (after wrestling quite a bit w splint) was
to use /*...@only@*/ or /*...@killref@*/ (but not both) when annotating
a dereferncing routine that has a lazy free when nrefs = 1 within.
Initiallu I used /*...@only@*/ which (in most of the code I saw) was
sufficient to hint that a ptr should not be used after being passed
to the routine that free's (or more technically dereferecnes).
The other (and largely equivalent approach) is to use /*...@killref@*/ which
ends up confusing splint's implicit annotation of the argument to
/*...@only@*/ when the reference count goes from 1 -> 0 and one typically
does a lazy free. I just disable the warnings around the free to
get rid of the warnings.
But mixing /*...@only@*/ and /*...@killref@*/ annotations cannot be done
without also keeping track of the value of /*...@refs@*/: the correct
annotation would be an additional /*...@only@*/ iff nrefs = 1. But
the value of nrefs is very hard to track with static annotations.
> And also error about memory leak at the end of main() function.
>
If test_unref() uses /*...@only@*/ and not /*...@killref@/, then
splint should be able to see that the pointer has been free'd.
The other approach would be to hide the malloc and have a creator
that is annotated with /*...@newref@*/.
Its the mixture of /*...@only@*/ and the refcounting annotations
that can lead to spurious messages.
hth
73 de Jeff
_______________________________________________
splint-discuss mailing list
splint-discuss@mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
