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

[Wenzel, Bodo]

Hi.

This works without any /*@i@*/ annotation, Splint 3.1.1 called with 
"+checks", which is quite strict, but not as "+strict" ;-)

struct s1 {
}

struct s2 {
}

static void
s1_free (/*@only@*/ /*@null@*/ struct s1 * f) {
  if ( f == NULL )
    return;
  free(f);
}

static void
s2_free (/*@only@*/ /*@null@*/ struct s2 * f) {
  if ( f == NULL )
    return;
  free(f);
}

struct s {
  struct s1 * f1;
  struct s2 * f2;
}

static void
s_free (/*@only@*/ /*@null@*/ struct s * f) {
  if ( f == NULL )
    return;
  s1_free(f->f1);
  s2_free(f->f2);
  free(f);
}

int
main (void) {
  struct s *s = malloc( sizeof *s );  assert( s != NULL );
  s->f1 = malloc( sizeof * (s->f1) ); assert( s->f1 != NULL );
  s->f2 = malloc( sizeof * (s->f2) ); assert( s->f2 != NULL );
  s_free( NULL );
  s_free( s );
  return 0;
}

Mit freundlichen Grüßen,
Bodo Wenzel
- Entwicklung Software -

-- 
BBR - Baudis Bergmann Rösch
Verkehrstechnik GmbH
Pillaustraße 1e	
D - 38126 Braunschweig

T: +49.531.27300-766
F: +49.531.27300-999
@: wenzel at bbr-vt.de
W: http://www.bbr-vt.de

Registergericht:   
AG Braunschweig  HRB 3037

Geschäftsführer: 
Dipl.-Ing. Arne Baudis
Dipl.-Ing. Thomas Bergmann
Dipl.-Ing. Frank-Michael Rösch

USt.-ID-Nr.:
DE 114 877 881