Hi Niklaus,

Here's an example of how you prevent the warnings for free_buffer2:

> static void free_buffer2(
>    /*@null *bufPtr->buffer@*/
>    /*@notnull bufPtr@*/ buf_t *bufPtr)
> {
>    if (bufPtr == NULL)
>    {
>       return;
>    }
>    free(bufPtr->buffer);
> }

(Aside: The /*@null *bufPtr ... */ annotation doesn't mean what you
want here --- splint ignores everything else in the comment after null,
so what this actually looks like is /*@null@*/ /*@notnull@*/ buf_t
*bufPtr.  Splint should provide a useful warning for this, but instead
just interprets the /*@null@*/ annotation as overriding the /*@notnull@*/
anootation on bufPtr.)

So, what you want is to specify free_buffer2 as a function that
deallocates the ->buffer of its parameter.  The /*@releases ... @*/ clause
(see http://www.splint.org/manual/html/sec7.html, Section 7.4 of the
manual for details) does this.  We also need to put a /*@special@*/
annotation on the parameter, to prevent a warning about it being in an
inconsistent state when the function returns:

static void free_buffer2(/*@special@*/ /*@null@*/ buf_t *bufPtr)
   /*@releases bufPtr->buffer@*/
   if (bufPtr == NULL)

Now, when splint checks test_two:

> static void test_two( void )
> {
>   free_buffer(my_global_buf_ptr);
>   free_buffer2(my_global_buf_ptr2);
> }

We get these warnings:

tst.c: (in function test_two)
tst.c:82:2: Function returns with global my_global_buf_ptr referencing released
  A global variable does not satisfy its annotations when control is
  transferred. (Use -globstate to inhibit warning)
   tst.c:79:15: Storage my_global_buf_ptr is released
tst.c:82:2: Released storage my_global_buf_ptr2->buffer reachable from global
   tst.c:81:16: Storage my_global_buf_ptr2->buffer is released

Since free_buffer2 is specified to release ->buffer of the parameter, we
get a warning about the state of the global variable being inconsistent
when test_two returns.

Hope this helps.  Some of the other issues are a bit trickier, but the
/*@allocates ...@*/ clause can specify what you need, I believe.

--- Dave

Reply via email to