Going through your code, there a few bugs that need to be fixed. I
marked your code with '>', lines to be replaced with '|'. Some things
have been mentioned already, but not all, so here it goes (sorry for the
long lines):
Niklaus Giger wrote:
> The file tst.c looks like this:
>
> #include <stdlib.h>
>
> typedef struct
> {
> /*@only@*/ /*@null@*/ char *buffer;
> int buf_length;
>
> } buf_t ;
>
> /*@only@*/ /*@null@*/ static buf_t *alloc_buffer(int size)
> {
> buf_t *bufPtr;
| bufPtr = malloc((size_t)size);
bufPtr = malloc(sizeof *bufPtr); /* bufPtr has to hold the struct only! */
> if (bufPtr == 0)
> {
> return 0;
> }
> bufPtr->buffer = malloc((size_t)size);
| if (bufPtr == 0)
if (bufPtr->buffer == NULL) /* we already know here bufPtr != NULL */
> {
> free(bufPtr);
> return 0;
> }
> bufPtr->buf_length = size;
> return bufPtr;
> }
>
> static void alloc_buffer2(/*@notnull@*/ buf_t *bufPtr, int size)
> {
> free(bufPtr->buffer);
> bufPtr->buffer = malloc((size_t)size);
| if (bufPtr == 0)
if (bufPtr->buffer == NULL)
> {
> bufPtr->buf_length = 0;
> return;
> }
> bufPtr->buf_length = size;
> return;
> }
>
>
| static void free_buffer(/*@only *bufPtr->buffer@*/
| /*@null *bufPtr->buffer@*/
| buf_t *bufPtr)
| requires maxRead(*bufPtr->buffer) <= *bufPtr->cfg_length@*/
static void free_buffer(/*@null@*/ /*@only@*/ buf_t *bufPtr)
> {
> if (bufPtr == NULL)
> {
> return;
> }
> free(bufPtr->buffer);
> free(bufPtr);
> }
>
| static void free_buffer2(
| /*@null *bufPtr->buffer@*/
| /*@notnull bufPtr@*/ buf_t *bufPtr)
static void free_buffer2(/*@null@*/ buf_t *bufPtr)
> {
> if (bufPtr == NULL)
> {
> return;
> }
> free(bufPtr->buffer);
bufPtr->buffer = NULL; /* don't let them use dangling pointers */
bufPtr->buf_length = 0; /* let them know there is no room */
> }
>
> static /*@only@*/ /*@null@*/ buf_t *my_global_buf_ptr;
> static /*@only@*/ /*@null@*/ buf_t *my_global_buf_ptr2;
>
> static void test_one( void )
> {
> free_buffer(my_global_buf_ptr);
> my_global_buf_ptr = alloc_buffer(1024);
>
| alloc_buffer2(my_global_buf_ptr2, 1024);
if (my_global_buf_ptr2 != NULL)
alloc_buffer2(my_global_buf_ptr2, 1024);
> }
> static void test_two( void )
> {
> free_buffer(my_global_buf_ptr);
my_global_buf_ptr = NULL; /* don't accidentally use freed storage */
>
> free_buffer2(my_global_buf_ptr2);
> }
>
> int main(/*@unused@*/int argc, /*@unused@*/char *argv[])
> {
> test_one();
> test_two();
> return 0;
> }
This does not eliminate all splint warnings, but IMVHO you first need to
fix your code! Also, if your system's free() has trouble with a
parameter of NULL, you need to insert additional checks (try +unixlib
then).
HTH&HAND
Ralf
