[splint-discuss] ensures isnull?

[Jonathan and Caroline Moore]

allington:Thu 30:2302:~:$ cat t.c
#include <stdio.h>
void test2(char *param[]) {
       while ( *param != NULL ) {
               *param = NULL;
	}
       return;
}

allington:Thu 30:2302:~:$ gcc -c t.c
allington:Thu 30:2302:~:$ splint t.c
Splint 3.1.2 --- 07 Nov 2008

Finished checking --- no warnings

2009/4/30 David N. Jansen <D.Jansen at cs.ru.nl>:
> 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.
> _______________________________________________
> splint-discuss mailing list
> splint-discuss at mail.cs.virginia.edu
> http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
>



-- 
Jonathan (and Caroline)

Jonathan and Caroline Moore
JandCMoore at gmail.com (Jonathan)
CandJMoore at gmail.com (Caroline)
http://jandcmoore.googlepages.com/