A "Clauses exit referencing" Comment I can't get rid of.

[Shlomi Fish]

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.