[splint-discuss] 'splint' and sys/types.h

[Roman Mashak]

Hello, Michael!
You wrote to "Discussions about the Splint annotation-assisted static 
analysisproject" <splint-discuss at cs.virginia.edu> on Thu, 26 Oct 2006 
06:28:23 -0700:

 MW> No, I'm afraid that doesn't demonstrate anything of the sort.  First,
 MW> what you wrote above doesn't demonstrate that sys/types.h is actually
 MW> defining u_int8_t *at the point where you explicitly include it in your
 MW> program*.  It may be, but as I wrote previously, sys/types.h may be
 MW> included by some earlier header, rendering your Splint annotation moot.
No, the sample code I'm testing has only one header file - sys/types.h. It's 
interesting to note that if I include 'sys/types.h' and don't declare the 
variable of type 'u_int8_t' (or whatever from sys/types.h), then it's 
perfectly passed through splint.

 MW> Second, there's no guarantee that the result of preprocessing with gcc
 MW> will be the same as what the Splint parser sees.  You still have to
 MW> find out why you get that definition from sys/types.h when you
 MW> preprocess with gcc, and not when you parse with Splint.
Is there a way to see the output what 'splint' is parser?

 MW> Again, conditional compilation and a different set of predefined macros
 MW> is the most likely explanation.

 MW> (Richard O'Keefe wrote in another note that this issue has been
 MW> discussed on the list before, so you might want to download the
 MW> archives - follow the link at the bottom of every list message - and
 MW> search through them.  Unfortunately, that's hardly convenient.)
In archives I've found only one suggested solution so far: write my own 
splint-specific sys/types.h

#ifdef S_SPLINT_S
# include "splint-include/sys/types.h"
#else
# include <sys/types.h>
#endif

==== splint-include/sys/types.h ====
typedef /*@unsignedintegraltype@*/ u_int8_t;

/* ... other definitions ... */
==== EOF ====

With best regards, Roman Mashak.  E-mail: mrv at corecom.co.kr