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 @obser...@?
Thanks for patience.
--
)\._.,--....,'``.
/, _.. \ _\ (`._ ,.
`._.-(,_..'--(,_..'`-.;.'
_______________________________________________
splint-discuss mailing list
splint-discuss@mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
