[splint-discuss] ensures isnull?

[Jonathan and Caroline Moore]

allington:Fri 01:0616:~:$ cat t.c
#include <stdio.h>

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

void test2(struct test *param) {
       while ( param->a != NULL )
               param->a = NULL;
       return;
}
allington:Fri 01:0617:~:$ gcc -c t.c
allington:Fri 01:0617:~:$ splint t.c
Splint 3.1.2 --- 07 Nov 2008

Finished checking --- no warnings

Jonathan

2009/5/1 David N. Jansen <D.Jansen at cs.ru.nl>:
> 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.
> _______________________________________________
> 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/