[splint-discuss] Introduction and splint patterns

[Carsten.Agger at tietoenator.com]

First of all, I'd like to introduce myself: My name is Carsten Agger, and I work as a software engineer with TietoEnator A/S in Aarhus, Denmark. 

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.

If such questions are inappropriate for this list, please let me know.

An example:

Pattern: COMPDEF, assigned member
Template:

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)

----------------

A possible solution to this is to assign to the struct member explicitly:

s.m->a = << ... >>;
s.m->b = << ... >>;
s.m->c = << ... >>;

But this is not very satisfactory - as I see it, splint might be able to figure that if m's fields are initialized, then s.m is also initialized.

Is there some other annotation I could use?  /*@-compdef@*/ is far too generic to be useful here (the function might e.g. take other parameters that I do want splint to check).

best regards,

Carsten Agger,
Aarhus, Denmark
http://www.tietoenator.com