[splint-discuss] Introduction and splint patterns

[John Carter]

On Wed, 23 Apr 2008, Carsten.Agger at tietoenator.com wrote:

> I'm running a large program through splint, and while I understand
> most of its warnings and can make an appropriate correction,
> sometimes I see a pattern that makes me bang my head against the
> wall, because yes, I see the problem or at least why splint might
> think there is a problem but no, the code is correct, I just don't
> know how to convince splint of that fact - especially since the
> warnings that would have to be turned off is often too generic -
> like compmempass, compdef, etc.

The advice I give our guys here is, annotate the declarations to
explain to splint what your intent is, rather than tell splint to
shut up.

Often if a typedef is too complex (read two levels or more) splint
doesn't understand it. That's OK, most human programmers won't
understand it either, so break it into smaller levels and typedef and
annotate those.

> struct_type s;
> member_type m;
>
> s = << ... >>
>
> s.m = &m;
>
> m.a = << ... >>;
> m.b = << ... >>;
> m.c = << ... >>;
>
> my_function( ..., s, ...);
>
> Warning:
>
> Passed storage *(s.m) contains 3 undefined fields ...
> 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)

I think whether m is defined or not is not the issue. I think splint
is looking no further than the type and annotation on s.m!

ie. If you need to convince splint that s.m points to a fully defined
object, ie. you need to annotate the m field on struct_type.

typedef struct {
   /*@SOME_ANNOTATION_HERE@*/ member_type * m;
} struct_type;

Which of course may have interesting implications on the rest of your
usage of that struct type. ie. The annotation/type will then say, field m
_always_ points to a fully defined member_type_type.

Conversely, you can argue that if m ever points to something other
that a fully defined member_type, you effectively have a different
type, but you have just used a lazy shorthand and not given it a
different name.

Splint gives the appearance of intelligence, actually it's just paying
very close attention to the strict typing system, and on each
individual hand over from this type to that type. As far as I can see
it doesn't pay much attention to the end-to-end data flow.

But that's OK, if you behave yourself in a very strictly well behaved
manner on each individual step, the end-to-end will be OK.

If you ever, so much as once, tell splint to shut up on any individual
step, well, your guarantees of end-to-end sanity have gone and you
back to the individual programmer smiling beatifically and saying
"Trust Me!"


John Carter                             Phone : (64)(3) 358 6639
Tait Electronics                        Fax   : (64)(3) 359 4632
PO Box 1645 Christchurch                Email : john.carter at tait.co.nz
New Zealand