> 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@bbr-...
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


_______________________________________________
splint-discuss mailing list
splint-discuss@ares...
http://www.cs.Virginia.EDU/mailman-2.1.5/listinfo/splint-discuss