On Tue, 19 Mar 2002, Syzop wrote:
> Hi,
>
> I'm new to splint and I would like to remove some warnings like
> "fresh storage bla not released before return" if the function is
> returning a pointer to a static buffer, I used following (test) code:
> --
> /*@exposed@*/ static char *func(char *s)
> {
> static char sbuf[512];
> sprintf(sbuf, "[TEST] %s", s);
> return sbuf;
> }
>
> int main()
> {
> char *p;
> char *s;
> p = func("alpha");
> s = func("beta");
> if (strcmp(p, "[TEST] alpha") == 0)
> printf("NOTREACHED\n");
> else
> printf("Result: '%s'\n", p);
> return 1;
> }
> --
> Splint 3.0.1.4 --- 20 Jan 2002
>
> Finished checking --- no warnings
> --
> Ok now I got the warnings gone, but splint doesn't seem to understand
> that after "s = func("beta");" the contents of *p are also changed.
> Is it possible to let splint detect this, and if so, how?
>
There's no easy way to do this, but you can probably define a custom
annotation that does what you want. Its not clear to me what you want
splint to warn about here though.
> Then some slightly different code: I replace sprintf with strcpy, then I get:
> --
> stor2.c: (in function func)
> stor2.c:4:9: Parameter 1 (sbuf) to function strcpy is declared unique but may
> be aliased externally by parameter 2 (s)
> A unique or only parameter may be aliased by some other parameter or visible
> global. (Use -mayaliasunique to inhibit warning)
> --
> So I try to correct this by using /*@unique@*/, it then doesn't like the observer
> value I passed:
> --
> stor2.c:8:5: Function main declared without parameter list
> A function declaration does not have a parameter list. (Use -noparams to
> inhibit warning)
> stor2.c: (in function main)
> stor2.c:12:11: Observer storage passed as unique param: func ("alpha")
> Observer storage is transferred to a non-observer reference. (Use
> -observertrans to inhibit warning)
> stor2.c:12:11: Storage becomes observer
> stor2.c:13:11: Observer storage passed as unique param: func ("beta")
> stor2.c:13:11: Storage becomes observer
> --
> Ok, that's correct, so I change it to /*@unique@*/ /*@observer@*/ since
> the contents aren't changed (I hope that's the right use of "observer").
> So in the end I get the following code:
> --
> /*@exposed@*/ static char *func(char /*@unique@*/ /*@observer@*/ *s)
> {
> static char sbuf[512];
> strcpy(sbuf, s);
> return sbuf;
> }
>
> int main()
> {
> char *p;
> char *s;
> p = func("alpha");
> s = func("beta");
> if (strcmp(p, "alpha") == 0)
> printf("NOTREACHED\n");
> else
> printf("Result: '%s'\n", p);
> return 1;
> }
> --
> Splint doesn't give any warnings, ok...
> But if I replace:
> s = func("beta");
> with:
> s = func(p);
> splint also doesn't complain...
> or did I misinterpretate the word "unique" and does
> it only check if the parameters are unique, not unique
> to other vars in a function.
>
unique means that this parameter cannot alias any other parameter. To be
correct, of course, it would also need to not be aliased by any other
storage reachable within the function body. splint's analyses isn't
sophisticated enough to do this though --- it would require
interprocedural modeling of storage sharing.
If I understand you correctly, what you really want is to get a warning if
the storage returned from one call to func is used after a second call to
func. Because static buffers are used like this so much in the standard
library, it would probably be worth building some mechanisms for checking
this. If you were willing to explicity say when you were done with a
static buffer by passing it as a parameter to a macro (that doesn't do
anything, but has a splint specification), then you could define a check
to do this (http://www.splint.org/manual/html/sec10.html). But, I agree
that it would be worth putting something more straightforward in for
handling this.
--- Dave
