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.
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
And also error about memory leak at the end of main() function.
Full example:
typedef /*...@abstract@*/ /*...@refcounted@*/ struct test_s *test;
struct test_s
{
/*...@refs@*/ int refcount;
};
/*...@external@*/ test
test_ref (test t)
{
t->refcount++;
return t;
}
/*...@external@*/ void
test_unref (/*...@killref@*/ /*...@only@*/ test t)
{
t->refcount--;
if (t->refcount<=0)
free (t);
}
int
main (void)
{
test c = NULL;
c = malloc (sizeof (*c));
if (c==NULL)
return 1;
c->refcount = 1;
c = test_ref (c);
test_unref (c);
test_unref (c);
return 0;
}
--
)\._.,--....,'``.
/, _.. \ _\ (`._ ,.
`._.-(,_..'--(,_..'`-.;.'
_______________________________________________
splint-discuss mailing list
splint-discuss@mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
