[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