[splint-discuss] ensures isnull?

[David N. Jansen]

Dear all,

I am a bit unsure what to think about the following. Either splint is  
overly cautious, or there is an execution path that I didn't think  
of. The following function generates a warning:

typedef /*@null@*/ char * char_p;

void test2(char_p * param) /*@ensures isnull *param@*/ {
	while ( *param != NULL )
		*param = NULL;
	return;
}

test.c: (in function test2)
test.c:5:9: Non-null storage *param corresponds to storage listed
                             in ensures isnull clause
   A possibly null pointer is reachable from a parameter or global  
variable that
   is not declared using a /*@null@*/ annotation. (Use -nullstate to  
inhibit
   warning)

I can make the warning go away by:
* placing an additional ``*param = NULL;'' after the loop
* replacing the loop by a do ... while loop.

Can you make the warning go away without additional code (and without  
switching the check off either ;) )?

David Jansen.