The problem is splint's annotations aren't precise enough to specify
realloc adequately. If realloc returns null, the ownership of the
parameter should not change; if realloc returns non-null the ownership of
the parameter is transferred to the return value. So, splint thinks the
result of realloc is only instead of owned. This should actually be okay,
so even with the realloc problem, its a bug that the warning is produced.
There's no easy workaround, other than rewriting your code to avoid using
realloc (which you probably don't want to do). Instead, you can use
/*@-branchstate@*/ } /* Line 67 */
/*@=branchstate@*/
to inhibit the warning message.
--- Dave
On Tue, 23 Jul 2002, Shlomi Fish wrote:
>
> I have the following structure definition:
>
> <<<
> struct freecell_solver_append_string_struct
> {
> /*@null@*/ /*@reldef@*/ /*@owned@*/ char * buffer;
> /*@reldef@*/ /*@dependent@*/ char * end_of_buffer;
> size_t max_size;
> int size_of_margin;
> };
>
> typedef struct freecell_solver_append_string_struct
> freecell_solver_append_string_t;
> >>>
>
> And the following function:
>
> <<<
> int freecell_solver_append_string_sprintf(
> freecell_solver_append_string_t * app_str,
> char * format,
> ...
> )
> {
> int num_chars_written;
> va_list my_va_list;
>
> va_start(my_va_list, format);
> num_chars_written = vsprintf(app_str->end_of_buffer, format,
> my_va_list);
> app_str->end_of_buffer += num_chars_written;
> /*
> * Check to see if we don't have enough space in which case we should
> * resize
> * */
> if (app_str->buffer + app_str->max_size - app_str->end_of_buffer <
> app_str->size_of_margin)
> {
> int offset = app_str->end_of_buffer - app_str->buffer;
> app_str->max_size += GROW_BY;
> app_str->buffer = realloc(app_str->buffer, app_str->max_size);
> /*L58*/
> if (app_str->buffer == NULL)
> {
> return -1;
> }
> /*
> * Adjust end_of_buffer to the new buffer start
> * */
> app_str->end_of_buffer = app_str->buffer + offset;
> } /* Line 67 */
>
> return num_chars_written;
> }
> >>>
>
> Now I get the following warning which I can't get rid of:
>
> <<<
> app_str.c:67:5: Clauses exit with app_str->buffer referencing only storage
> in
> true branch, owned storage in continuation
> The state of a variable is different depending on which branch is taken.
> This
> means no annotation can sensibly be applied to the storage. (Use
> -branchstate
> to inhibit warning)
> app_str.c:58:70: Storage app_str->buffer becomes only
> >>>
>
> How do I get rid of it?
>
> Regards,
>
> Shlomi Fish
>
>
>
> ----------------------------------------------------------------------
> Shlomi Fish [EMAIL PROTECTED]
> Home Page: http://t2.technion.ac.il/~shlomif/
> Home E-mail: [EMAIL PROTECTED]
>
> He who re-invents the wheel, understands much better how a wheel works.
>
