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

[Jorge Peixoto de Morais Neto]

>
>
> I think /*@dependent@*/ or /*@shared@*/ could both work, i.e.,
> "static /*@dependent@*/ char *statictest(){..."
>
> 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 was thinking about saying *precisely the same thing* in my first post, but
I thought that I would be flamed with comments like "If you don't know what
is the problem than shut up".  I also have read it multiple times, and find
it hard to understand.

In my real program, (not the one I put in my first post) I had already tried
to  use /*@shared@*/, but splint complained
"Fresh storage returned as shared (should be only): ret
  Fresh storage (newly allocated in this function) is transferred in a way
that
  the obligation to release storage is not propagated.  Use the /*@only@*/
  annotation to indicate the a return value is the only reference to the
  returned storage. (Use -freshtrans to inhibit warning)
   arrumanomes.c:56:46: Fresh storage ret created"

The only storage was being returned by function basename. It turns out that
basename  does not seem to have an annotated version for splint; therefore,
splint assumes it returns only storage. I have now worked around the problem
with the following code in the beginning of the program:

#ifdef S_SPLINT_S //if this macro is defined, then the program is being
analyzed by splint. splint doesn't seem to understand that the functions
dirname and basename return pointers to static storage; the annotations
below tell this to splint.
/*@shared@*/
extern char *dirname(char *path);
/*@shared@*/
extern char *__xpg_basename (char *__path);
#define basename    __xpg_basename
#else
#include <libgen.h> //basename,dirname
#endif //S_SPLINT_S

Perhaps I would have seen this workaround earlier if the splint warning told
me that  if the storage should not have been created with only, I should
annotate the function that creates it with /*@shared*@/, since /*@only@*/ is
implicit. Perhaps this could be emphasized in the splint manual too. It
should be emphasized that only is the default and that if splint does not
understand that some memory does not need to be deallocated, perhaps the
culprit is a function that is not annotated.

Anyway, The biggest problem is that, since I was using +unixlib (also tried
with +posixlib), I thought that basename and dirname would be correctly
annotated. At first I didn't even consider the possibility that
{base,dir}name lacked annotations. I was trying to solve the problem by
annotating my variables and functions, and even considered the possibility
that {base,dir}name did in fact return dynamically allocated memory that
should be freed (I have studied them and found out that the storage they
return should *not* be freed).

Perhaps the splint's unixlib should be enhanced?

PS: How would owned/dependent work? splint would still expect the memory to
be deallocated, wouldn't it?
-- 
Software is like sex: it is better when it is free.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.cs.Virginia.EDU/pipermail/splint-discuss/attachments/20070305/068cb4ab/attachment.htm