[splint-discuss] Tell me more about @only@

[Bill Pringlemeir]

On 13 Jan 2010, m at alanny.ru wrote:

> struct my_struct {
> int n; /* doesn't matter */
> /*@null@*/ struct my_struct *next;
> }

> new_item = (struct my_struct *) malloc (sizeof (struct my_struct));

> How to tell splint, that my_struct->next is not defined (because my_struct
> 	have just allocated with malloc)
> at all and this cannot be memory leak?

Short answer: try,

> struct my_struct {
> int n; /* doesn't matter */
> /*@null@*/ /*@dependent@*/ struct my_struct *next;
> }

malloc() is annotated like this,

extern /*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@modifies errno@*/
     /*drl 09-20-001 added errno*/
     /*@ensures MaxSet(result) == (size - 1); @*/ ;

The '/*@null@*/' is independant of 'only'.  By default all structure
members are declared only (see sec 5.3 of the manual).  This makes
sense for things that are not links (like a dynamically sized string
or buffer).  For a link you might like /*@dependent@*/.  I think this
would solve your problem, but it is not as strict in the checking.

I think that annotating old_item with 'only' would also work.

Sections five and six of the manual will be helpful.  The other thing
is that calloc() could be used or explicitly setting 'next' with
'NULL' The difference in the annotation,

     extern /*@null@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/

The 'out' parameter means that things have yet to be defined.
memset's return value might also be used if you insist on that,

   new_item = memset(new_item, 0, sizeof(*new_item));

Using memset is generally not the best as zero may not be appropriate
in all circumstances.  Ie, for some structure fields a value of one
might be appropriate (now or in the future).  If new_item will now and
forever needs zero initialized elements, it is questionable whether
calloc versus 'malloc/memset' is better... but if you think that the
inline memset is more efficient, you can either annotate to ignore the
error here or use a macro for 'malloc' and 'memset' which have
alternative annotations.

hth,
Bill Pringlemeir.

-- 
I never did give anybody hell.  I just told the truth and they thought it
was hell. - Harry S. Truman