On Sat, Nov 01, 2003 at 09:58:46PM -0500, David Evans wrote:
>
> Splint's analysis isn't sophisticated enough to figure this out. If you
> do,
>
> free(this_string);
> this_string = NULL;
>
> it will prevent the warning.
I just checked the manual, and in clause 5.2.1#5 it states that
"After the release obligation is transferred, the original reference
is a dead pointer and the storage it points to may not be used."
5.2.1#3 says:
* assign it to an external reference declared with an only annotation
According to these statements, the following program should be ok,
shouldn't it?
------------------------------------------------------------------
typedef /[EMAIL PROTECTED]@*/ /[EMAIL PROTECTED]@*/ char *cstring;
/[EMAIL PROTECTED]@*/ extern cstring make_string(const char *) /[EMAIL PROTECTED]/;
extern int main(void)
{
cstring oldstr = NULL;
cstring newstr = make_string("newstr");
if (oldstr == NULL) {
oldstr = newstr;
/* oldstr should be live */
/* newstr should be dead */
} else {
free(oldstr);
oldstr = make_string("oldstr");
/* oldstr should be live */
free(newstr);
/* newstr should be dead */
}
free(oldstr);
return 0;
}
------------------------------------------------------------------
Roland
_______________________________________________
splint-discuss mailing list
[EMAIL PROTECTED]
http://www.splint.org/mailman/listinfo/splint-discuss
