[splint-discuss] HOWTO query

[Mark Johnson]

I have gone through the manual and a few of the papers, but when and 
how to make annotations is not clear. Has someone put together a "how 
to annotate", FAQ, or similar guide to Splint? If so - where? If not, 
I'm willing to help put one together, but need a better understanding 
of the "real rules".

Here are a few examples / questions raised:

A function like fopen can return NULL. So a function like

void log_on(void)
{
   static char *logfile = "logfile"; /* name of log file */

   if ((fecho = fopen(logfile, "w")) == NULL)
     {
       logging = 0;
     }
   else
     {
       (void)fprintf(fecho, "Roman log file.\n\n");
       logging = 1;
     }
}

will generate warnings such as
% splint player.c io.c
Splint 3.0.1.6 --- 03 Mar 2003

io.c: (in function log_on)
io.c:69:36: Observer storage assigned to unqualified reference:
                char * logfile = "logfile" = "logfile"
   Observer storage is transferred to a non-observer reference. (Use
   -observertrans to inhibit warning)
    io.c:69:26: Storage becomes observer
io.c:80:2: Function returns with non-null global fecho referencing null 
storage
   A global variable does not satisfy its annotations when control is
   transferred. (Use -globstate to inhibit warning)
    io.c:71:16: Storage fecho may become null

Finished checking --- 2 code warnings

For the first warning, the manual does not provide any clear 
explanation of what "observer storage" is or how it should be handled.
  - observer is not in the index
  - storage model is in the index, refers to section 5 which doesn't 
describe observer storage
  - there is an oblique reference in Appendix C (which points to 6.2.1)
The last one talks about functions, not storage declarations, but 
apparently changing it to
   static char /*@observer@*/ *logfile = "logfile"; /* name of log file 
*/
makes the warning go away. Do I need to add that annotation whenever I 
initialize a string? If so, why?

The definition of fopen does not have any special annotations about 
NULL values, but this function seems to need some according to Splint. 
I also tried
static FILE /*@relnull@*/ *fecho; /* record the action */
but that did not help either. The warning suggests -globstate, but that 
appears to be a global flag - not one local to this specific case. In 
addition, I noticed the declarations for fdopen and fopen vary as 
follows:

extern /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char 
*type)
     /*@modifies errno, fileSystem@*/;

extern FILE * fopen (char *filename, char *mode)
     /*@modifies errno, fileSystem;@*/ ;

which would imply that fopen should be returning null / dependent 
references as well. Is there some reason for this difference?

Thanks.
   --Mark