[splint-discuss] Can't fit our memory management to Splint's model

[Tommy Pettersson]

On Sat, Jun 16, 2007 at 12:43:25PM +0300, Roman Cheplyaka wrote:
> Hi all!

Hi,

> We use nested structures like
> struct s {
>   struct s1 * f1;
>   struct s2 * f2;
> }
> and each has its alloc and free function, e.g.
> void s_free(struct s * f) {
>   if ( f == NULL )
>     return;
>   s1_free(f->f1);
>   s2_free(f->f2);
>   free(f);
> }
[...]
> How can I explain
> splint that in this case they have not to be released?

I'm not totally sure this is correct in every way, but it seems
to work:


  #include <assert.h>
  #include <stdlib.h>
  
  struct s {
  	/*@only@*/ char *f1;
  	/*@only@*/ char *f2;
  };
  
  static void
  s_free (/*@special@*/ struct s *p_f)
  	/*@releases p_f->f1, p_f->f2, p_f; @*/
  ;
  
  static void
  s_free (struct s *f)
  {
  	if ( f == NULL )
  		/*@i3@*/ return;
  	
  	free( f->f1 );
  	free( f->f2 );
  	free( f );
  }
  
  int
  main (void)
  {
  	struct s *s = malloc( sizeof *s ); assert( s != NULL );
  	s->f1 = malloc( 1 );	assert( s->f1 != NULL );
  	s->f2 = malloc( 1 );	assert( s->f2 != NULL );
  	s_free( NULL );
  	s_free( s );
  	
  	return 0;
  }


On the /*@i3@*/ line splint will complain that f, f1 and f2 are
not released as claimed by the declaration, but it is an
obviously false warning. A slightly better way would perhaps be
to surround the return line with annotations that temporarily
turns of just the expected bogus warning.

(To my surprise, the order of the arguments in the @releases@
clause seem to matter. I had to put p_f last, or I got
unexplainable warnings about undefined storage passed to the
s_free function.)



-- 
Tommy Pettersson <ptp at lysator.liu.se>