spurious use before definition warning

[Ed Beroset]

I think I'm getting spurious "use before definition warnings" and I want to 
see if there's a capability, annotation or switch in Splint that I'm 
overlooking.  When I run Splint on this test program (with no command line 
switches and no .splintrc file):

#include <stdio.h>
#define READ_OK ((int)0)

extern int readMemoryDevice(/*@out@*/ void *buffer, size_t buffSize);

typedef struct {
     int first;
     int second;
} bongo;

int main()
{
     int testResult;
     bongo test1, test2;

     testResult = 1;
     if (readMemoryDevice(&test1, sizeof(test1)) != READ_OK ||
             readMemoryDevice(&test2, sizeof(test2)) != READ_OK ||
             test2.second != test1.second)     /* this is line 19 */
         testResult = 0;

     return testResult;
}

I get this result:

Splint 3.0.1.6 --- 11 Feb 2002

dummy.c: (in function main)
dummy.c(19,13): Field test2.second used before definition
   An rvalue is used that may not be initialized to a value on some execution
   path. (Use -usedef to inhibit warning)

Finished checking --- 1 code warning

The ANSI C standard (6.3.14) says that "... the || operator guarantees 
left-to-right evaluation; there is a sequence point after the evaluation of 
the first operand."  It seems to me that using the /*@out@*/ annotation 
should give Splint sufficient clue that both the test1 and test2 structures 
will be fully defined by the time it gets to line 19 (if it gets that 
far).  While I could use nested if statements, I'd really rather not 
clutter my code that way.  Is there a graceful way to explain this to Splint?

Ed