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)
{
return;
}
free(bufPtr->buffer);
}
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
storage
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
