[splint-discuss] Splint reporting a memory leak when none exists

[Roland Illig]

jds wrote:
> Anyway, Splint reports a memory leak at the malloc line, saying that
> the only pointer g_int1 has not been deallocated before being
> assigned.  If I explicitly free(g_int1) instead of calling a function
> to do it, no memory lead reported.  I can't figure out how to tell
> Splint that g_int1 is being deallocated in function killInt().

I tried it, but with no complete success.

#include <stdlib.h>

/*@null@*//*@only@*/ static int* g_int1 = NULL;

typedef /*@only@*//*@null@*/ int* pInt;

static void killInt(/*@special@*/ /*@notnull@*/ pInt* pi)
	/*@releases *pi; @*/
	/*@ensures isnull *pi; @*/
{
   free(*pi);
   *pi = NULL;
}

int main(/*@unused@*/ int argc __attribute__((unused)), /*@unused@*/ 
char** argv __attribute__((unused)))
{
   killInt(&g_int1);
   g_int1 = (int*)malloc(sizeof(int));
   if (NULL != g_int1)
     *g_int1 = 1;
   killInt(&g_int1);

   return 0;
}

Resulting in this:
 > Splint 3.1.1 --- 31 May 2005

 > foo.c: (in function main)
 > foo.c:23:12: Function returns with global g_int1 referencing released 
storage
 >   A global variable does not satisfy its annotations when control is
 >   transferred. (Use -globstate to inhibit warning)
 >    foo.c:21:11: Storage g_int1 released

Roland