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

AlannY m at alanny.ru
Fri Jan 22 04:41:27 PST 2010


Hi there. Several days already spent trying to understand what @observer@ annotation
really do.

I can undestand the following:

    /*@observer@*/ const char*
    my_func (e_t *e)
    {
      return e->name;
    }

It's obvious. But what @observer@ means for structure fields and function parameters?

For example:
    void
    my_func (/*@observer@*/ char *name)
    {
      ...
    }

Will it tell, that *name is `const'? Or not?

Or
    struct my_struct
    {
      /*@observer@*/ char *name;
    }

Why we have it? For the my_struct->name = my_func which returns @observer@?

Thanks for patience.

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


More information about the splint-discuss mailing list