[splint-discuss] Splint usage help

[Phil Longstaff]

For routines from external libraries, I created a single file I called splintdefs.h, which was included from my source files:

#ifdef S_SPLINT_S
#include "splintdefs.h"
#endif

so that it doesn't affect normal compilation.  I then copy the prototypes from the external headers into that file and annotate them.

Phil



________________________________
From: Marcus Martin <nymaen at yahoo.com>
To: splint-discuss at mail.cs.virginia.edu
Sent: Saturday, April 18, 2009 9:38:33 AM
Subject: [splint-discuss] Splint usage help


<Please ignore the first message, this one is in plain text.>


I
am a new splint user and am having some difficutly with the
annotations. I read the documentation and looked at the examples and
still have some trouble. Can someone please help me get started?

I have the source code line:
const char *subCmds[] = { "-file", "-stream", NULL }; 

This
array needs to have the last element be NULL so when used a parameter
in a method, the method knows when to stop reading the array. Splint
produces the following errors.

test.c:94:68: Index of possibly null pointer subCmds: subCmds
  A possibly null pointer is dereferenced.  Value is either the result of a
  function which may return null (in which case, code should check it is not
  null), or a global, parameter or structure field declared with the null
  qualifier. (Use -nullderef to inhibit warning)
   test.c:94:27: Storage subCmds may become null
test.c:94:61: Local subCmds[2] initialized to null value: subCmds[2] = NULL
  A reference with no null annotation is assigned or initialized to NULL.  Use
  /*@null@*/ to declare the reference as a possibly null pointer. (Use
  -nullassign to inhibit warning)

After reading the warnings I tried changing the source line in the following ways, none of which worked for me.

/*@-nullderef@*/ const char *subCmds[] = { "-file", "-stream", NULL };  /*@=nullderef@*/ 
/*@-nullassign@*/ const char *subCmds[] = { "-file", "-stream", NULL };  /*@=nullassign@*/
const char *subCmds[] = { "-file", "-stream", /*@null@*/  NULL }; 

The
second problem I encountered is that splint wants me to annotate the
header files of exeternal packages I call to indicate out parameters
and parameters that can be NULL. Since I don't own that source code,I
really don't want to change it. How do I indicate to splint where I
invoked the method that my parameters are correct and the method is
used correctly.

The third issue is that I am creating a shared
library that  implements the interface. At no place in my code base
will I call these public interface methods. How can I tell splint that
these methods are exported and not called directly, but that is okay.

Can
someone tell me what I am doing wrong? Once I understand these three
problems, I should be able to fix the rest of my module.

Marcus


      
_______________________________________________
splint-discuss mailing list
splint-discuss at mail.cs.virginia.edu
http://www.cs.virginia.edu/mailman/listinfo/splint-discuss
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.cs.virginia.edu/pipermail/splint-discuss/attachments/20090418/bd5eba47/attachment-0002.html