[splint-discuss] Help me with @refcounted@

[AlannY]

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 ;-)

Thank for patience.

-- 
   )\._.,--....,'``.
  /,   _.. \   _\  (`._ ,.
 `._.-(,_..'--(,_..'`-.;.'