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.
