I think you want:
struct freecell_solver_append_string_struct
{
/*@null@*/ /*@reldef@*/ /*@owned@*/ char *buffer;
/*@null@*/ /*@reldef@*/ /*@dependent@*/ char *end_of_buffer;
size_t max_size;
int size_of_margin;
};
This indicates that the buffer field is responsible for the storage it
points to, but there may be other references to that storate; the
end_of_buffer is a dependent reference (since it points to somewhere in
the buffer). The reldef annotations are used to indicate that the fields
may not be defined, since freecell_solver_append_string_alloc returns
an allocated by not defined structure.
--- Dave
On Mon, 22 Jul 2002, Shlomi Fish wrote:
>
> I have the following header:
>
> /********** app_str.h ***********/
>
> #include <string.h>
> #include <stdio.h>
> #include <stdarg.h>
> #include <stdlib.h>
>
> #ifndef __APP_STR_H
> #define __APP_STR_H
>
> #ifdef __cplusplus
> extern "C" {
> #endif
>
> struct freecell_solver_append_string_struct
> {
> /*@kept@*/ /*@out@*/ char * buffer;
> char * end_of_buffer;
> size_t max_size;
> int size_of_margin;
> };
>
> typedef struct freecell_solver_append_string_struct
> freecell_solver_append_string_t;
>
> extern /*@null@*/ freecell_solver_append_string_t *
> freecell_solver_append_string_alloc(int size_margin);
>
> extern int freecell_solver_append_string_sprintf(
> freecell_solver_append_string_t * app_str,
> char * format,
> ...
> );
>
> extern char * freecell_solver_append_string_finalize(
> freecell_solver_append_string_t * app_str
> );
>
> #ifdef __cplusplus
> }
> #endif
>
> #endif /* #ifndef __APP_STR_H */
>
> /***********************/
>
> And the following module:
>
>
> /*************** app_str.c *********************/
>
> #include <string.h>
> #include <stdio.h>
> #include <stdarg.h>
> #include <stdlib.h>
>
> #include "app_str.h"
>
> #define GROW_BY 4000
>
>
> freecell_solver_append_string_t * freecell_solver_append_string_alloc(int
> size_margin)
> {
> freecell_solver_append_string_t * app_str;
>
> if (size_margin > GROW_BY)
> {
> return NULL;
> }
>
> app_str = malloc(sizeof(freecell_solver_append_string_t));
> if (app_str == NULL)
> {
> return NULL;
> }
>
> app_str->max_size = GROW_BY;
> app_str->end_of_buffer = app_str->buffer = malloc(app_str->max_size);
> if (app_str->buffer == NULL)
> {
> free(app_str);
> return NULL;
> }
> app_str->size_of_margin = size_margin;
>
> return app_str;
> }
>
> 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)
> {
> char * old_buffer = app_str->buffer;
> app_str->max_size += GROW_BY;
> app_str->buffer = realloc(app_str->buffer, app_str->max_size);
> /*
> * Adjust end_of_buffer to the new buffer start
> * */
> app_str->end_of_buffer = app_str->buffer + (app_str->end_of_buffer
> - old_buffer);
> }
>
> return num_chars_written;
> }
>
> char * freecell_solver_append_string_finalize(
> freecell_solver_append_string_t * app_str
> )
> {
> char * ret;
> ret = strdup(app_str->buffer);
> free(app_str->buffer);
> free(app_str);
> return ret;
> }
>
> /*****************************/
>
> When I process it with splint (ver. 3.0.1.3.1) I get a gazillion of
> warnings. The first ones are:
>
> <<<
> app_str.c: (in function freecell_solver_append_string_alloc)
> app_str.c:27:30: Only storage assigned to kept:
> app_str->buffer = malloc(app_str->max_size)
> The only reference to this storage is transferred to another reference
> (e.g.,
> by returning it) that does not have the only annotation. This may lead
> to a
> memory leak, since the new reference is not necessarily released. (Use
> -onlytrans to inhibit warning)
> app_str.c:27:5: Kept storage app_str->buffer assigned to implicitly only:
> app_str->end_of_buffer = app_str->buffer = malloc(app_str->max_size)
> storage is transferred to a non-temporary reference after being passed
> as
> keep parameter. The storage may be released or new aliases created. (Use
> -kepttrans to inhibit warning)
> >>>
>
> How do I get rid of them?
>
> 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.
>
