lclint-interest message 43

From tgm@netcom.com Tue Mar 19 15:31:59 1996
Date: Fri, 8 Mar 1996 20:15:40 -0500
From: tgm@netcom.com (Thomas G. McWilliams)
To: lclint-interest@larch.lcs.mit.edu
Subject: LCLint 2.0 anomaly?


LCLint 2.0 shows a lot of promise, particularly the ability to
statically check memory management. However, consider the following bit
of code and the error message generated by LCLint 2.0. I have a hard
time understanding why this simple code fragment generates an error.

Questions with respect to the example below:
  What does it mean that storage becomes dependent?
  What does it mean that storage becomes owned?

I've read David's new paper and the guide.  At face value, in the
example below it would seem that the no matter which branch is taken at
the if(1) conditional statement, there is no change of state.  Obviously
I'm missing something. 

/* example.c */
#include 
#include 

int
main()
{
    char *buf = malloc(10);

    if (buf != NULL) {
	char *line = buf;
	if (1) {
	    line = buf;
	}
	free(buf);
    }
    return 0;
}
/* end example.c */

LCLint 2.0 --- 07 Mar 96

example.c: (in function main)
example.c:15,2: Variable buf is dependent in true branch, but independent in
                   continuation.
  The state of a variable is different depending on which branch is taken. 
  This means no annotation can sensibly be applied to the storage.  Use
  -branchstate to suppress message.
   example.c:12,19: Storage buf becomes dependent
   example.c:14,6: Storage buf becomes owned

Finished LCLint checking --- 1 code error found