<div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"><br>I think /*@dependent@*/ or /*@shared@*/ could both work, i.e.,<br>"static /*@dependent@*/ char *statictest(){..."
<br><br>at memory that splint uses. That is understandable. There is<br>something with the splint manual that makes it hard to<br>understand. At least I think so. </blockquote><div>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.
<br><br>In my real program, (not the one I put in my first post) I had already tried to use /*@shared@*/, but splint complained <br>"Fresh storage returned as shared (should be only): ret<br> Fresh storage (newly allocated in this function) is transferred in a way that
<br> the obligation to release storage is not propagated. Use the /*@only@*/<br> annotation to indicate the a return value is the only reference to the<br> returned storage. (Use -freshtrans to inhibit warning)<br>
arrumanomes.c:56:46: Fresh storage ret created"<br><br>The <span style="font-style: italic;">only</span> 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
<span style="font-style: italic;">only</span> storage. I have now worked around the problem with the following code in the beginning of the program:<br><br>#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.
<br>/*@shared@*/<br>extern char *dirname(char *path);<br>/*@shared@*/<br>extern char *__xpg_basename (char *__path);<br>#define basename __xpg_basename<br>#else <br>#include <libgen.h> //basename,dirname<br>#endif //S_SPLINT_S
<br><br>Perhaps I would have seen this workaround earlier if the splint warning told me that if the storage should not have been created with <span style="font-style: italic;">only</span>, 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
<span style="font-style: italic;">only</span> 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. <br><br>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).
<br><br>Perhaps the splint's unixlib should be enhanced? <br><br>PS: How would owned/dependent work? splint would still expect the memory to be deallocated, wouldn't it?<br></div></div>-- <br>Software is like sex: it is better when it is free.