[splint-discuss] how to annotate a pointer to static memory returned by a function

[Tommy Pettersson]

On Sun, Mar 04, 2007 at 07:01:23AM -0300, Jorge Peixoto de Morais Neto wrote:
> static char *statictest(){
>  static char buff[10];
>  return buff;
> }
> int main(){
>  /*@unused@*/
>  char *p=statictest();
>  return 0;
> }
> When the above program is fed to  splint, the following output results:
[...]
> How can I correctly annotate the code to avoid this? I couldn't find in the
> manual.

Splint has a model for memory management. It is much more
complex than the usual pointers and types in C. It is also far
more restrictive in how pointers can be used. The purpose is to
make it impossible to get memory faults. Though, for practical
use it is sometimes too restrictive. It can not, for one thing,
handle dynamically changing properties. It is also incapable of
modeling the realloc() function.

So, the task is not always how to "correctly annotate the code",
because splint's model is just not always powerful enough. In
such cases one must resort to more relaxed checking, or even
ignore some (false) warnings. This does not mean the code is
necessarily bad, it just means splint can't be used to verify it
is all good.

In your case, however, the problem is quite simple. The
statictest() function has no annotation for what kind (in the
splint model) of pointer it returns, so splint uses the default,
which is 'only pointer'. This is supposed to be memory that you
have allocated in the function, and that you return to the
calling function together with the obligation to free it. This
is clearly not the case. The ownership of the static array
'buff' should not be transfered out of the function, and
certainly not free()ed by the calling function.

I think /*@dependent@*/ or /*@shared@*/ could both work, i.e.,
"static /*@dependent@*/ char *statictest(){..."

The way you put your question makes me thing that you perhaps is
not yet entirely familiar with the more complex way of looking
at memory that splint uses. That is understandable. There is
something with the splint manual that makes it hard to
understand. At least I think so. I had to read it many, many
times before I got (most of) it. But once you do, the warnings
from splint becomes very precise and to the point about what
splint is upset about.


-- 
Tommy Pettersson <ptp at lysator.liu.se>