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

[Roman Cheplyaka]

* Wenzel, Bodo <wenzel at bbr-vt.de> [2007-06-18 08:43:32+0200]
> 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;
> }

Yes, _this_ actually works. But if we add some fields to our structures
(say, struct s1 { int a; } and struct s2 { int b; }), then 

Passed storage *(s->f1) contains 1 undefined field: a
  Storage derivable from a parameter, return value or global is not defined.
  Use /*@out@*/ to denote passed or returned storage which need not be defined.
  (Use -compdef to inhibit warning)
Passed storage *(s->f2) contains 1 undefined field: b

So, naturally we need to declare *_free as /*@out@*/ (and this is how libc
function free is annotated). But then 

Unallocated storage f->f1 passed as out parameter to s1_free:
                 f->f1
  An rvalue is used that may not be initialized to a value on some execution
  path. (Use -usedef to inhibit warning)
Unallocated storage f->f2 passed as out parameter to s2_free:
                 f->f2

This is a problem I was talking about..

-- 
Roman I. Cheplyaka
http://ro-che.info/
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 307 bytes
Desc: Digital signature
Url : http://www.cs.Virginia.EDU/pipermail/splint-discuss/attachments/20070621/3c73ef25/attachment.bin