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

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,
    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 <
        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);
        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
                   true branch, owned storage in continuation
  The state of a variable is different depending on which branch is taken.
  means no annotation can sensibly be applied to the storage. (Use
  to inhibit warning)
   app_str.c:58:70: Storage app_str->buffer becomes only

How do I get rid of it?


        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.

Reply via email to