On Jan 16, 2010, at 4:47 AM, AlannY wrote:
> Hi there. I have another lame question now about using @refcounted@
> annotation.
>
> Several days already I'm trying to solve it, but cannot.
>
> There are minor program, which uses refcounted as I can it imaging.
> Please don't send me to the manual to the section 5.4, I've already
> read it hundred times.
>
> typedef /*...@refcounted@*/ struct ref* ref;
>
> struct ref
> {
> /*...@refs@*/ int refcount;
> void *b;
> };
>
> void
> c_ref (/*...@null@*/ ref c)
> {
> if (c==NULL)
> return;
>
> c->refcount++;
> }
>
> void
> c_unref (/*...@null@*/ /*...@killref@*/ ref c)
> {
> if (c==NULL)
> return;
>
> c->refcount--;
> if (c->refcount<=0)
> free (c);
> }
>
> int
> main (void)
> {
> ref c = NULL;
> c = malloc (sizeof (struct ref));
> c_ref (c);
> c_unref (c);
> return NULL;
> }
>
> I think, that I'm not understanding something fundamental about refcounted.
> Please, explain ;-)
>
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.
73 de Jeff
> Thank for patience.
>
> --
> )\._.,--....,'``.
> /, _.. \ _\ (`._ ,.
> `._.-(,_..'--(,_..'`-.;.'
> _______________________________________________
> splint-discuss mailing list
> splint-discuss@mail.cs.virginia.edu
> http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
_______________________________________________
splint-discuss mailing list
splint-discuss@mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
