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

[Wenzel, Bodo]

> 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
> [...]
> Passed storage *(s->f2) contains 1 undefined field: b
That's correct. The fields _ARE_ undefined. If values are stored, no 
error is reported.

> So, naturally we need to declare *_free as /*@out@*/ (and this is
> how libc function free is annotated).
This annotation is only necessary if it is really your intention to 
release the struct's memory while some field is undefined. See above.

> But then
> 
> Unallocated storage f->f1 passed as out parameter to s1_free:
>                  f->f1
> [...]
> Unallocated storage f->f2 passed as out parameter to s2_free:
>                  f->f2
> 
> This is a problem I was talking about..
Again the error message is correct, as the Splint manual describes: 
"The out annotation denotes a pointer to storage that may be 
undefined." And so it assumes that fields of struct s are undefined, 
say unallocated, right?

But if we annotate just s[12]_free, because all fields of struct s 
ARE defined, the "Passed storage..." messages re-appear. Well, it 
seems that Splint refers the annotation on the fields recursively...

You can use "partial" in s_free, but then you won't get any error 
message if you don't define f1 or f2 or both.

No more clues at the moment... :-(

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