[splint-discuss] ensures isnull?

[David N. Jansen]

Caroline or Jonathan, thank you for the quick answer.
I see that I simplified my program too much. Actually, the pointer is  
a member in a structure, so I should have written:

#include <stdio.h>

struct test {
	int i;
	/*@null@*/ /*@dependent@*/ char * a;
};

void test2(struct test * param) /*@ensures isnull param->a@*/ {
	while ( param->a != NULL )
		param->a = NULL;
	return;
}

Now the trick with an array does no longer work... When I change the  
parameter to ``struct test param[]'', ``struct test (*param)[]'' or  
``struct test *param[]'', I still get the error message:
test.c:11:9: Non-null storage param[0].a corresponds to storage  
listed in
                 ensures isnull clause

David Jansen, Netherlands.