[splint-discuss] memory management

[David Evans]

Yes, splint's analysis merges the null state after the if, but loses the
information from the predicate test (to know that buf->data was already
NULL), so you get the spurious warnings.

If you change the code to,

  if (buf->data != NULL) {
    free(buf->data);
  }
  buf->data = NULL;

the warning will go away (although you may rightly prefer the original
code and need to use syntactic comments to supress the spurious warnings.

--- Dave

On Sun, 19 Sep 2004, Roland Illig wrote:

> /**
> Hi,
>
> I didn't manage to completely splint the following program using:
>
> splint +strict +posixstrictlib +quiet -exportlocal -exportfcn \
> -exporttype
>
> Is it a bug in splint?
>
> Roland
> */
>
> struct buffer {
> 	/*@only@*/ /*@null@*/ void *data;
> 	size_t size;
> };
>
> static void buffer_free(/*@special@*/ struct buffer *buf)
> 	/*@modifies *buf; @*/
> 	/*@releases buf->data; @*/
> 	/*@ensures isnull buf->data; @*/
> {
> 	if (buf->data != NULL) {
> 		free(buf->data);
> 		buf->data = NULL;
> 	}
> 	buf->size = 0;
> }
> _______________________________________________
> splint-discuss mailing list
> splint-discuss at cs.virginia.edu
> http://www.splint.org/mailman/listinfo/splint-discuss
>