Fixes after removing -unrecogcomments flag for make splintme.

[splint.git] / src / Headers / fileTable.h

diff --git a/src/Headers/fileTable.h b/src/Headers/fileTable.h
index d1dd875a3b5c4369eb671bac85fe9c5d0687508f..607bec1004248f52196f140b00622f59137a095e 100644 (file)
--- a/src/Headers/fileTable.h
+++ b/src/Headers/fileTable.h
@@ -1,5 +1,5 @@
 /*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
 ** See ../LICENSE for license information.
 **
 */
@@ -20,12 +20,12 @@
 typedef enum { FILE_NORMAL, FILE_LSLTEMP, FILE_NODELETE,
               FILE_HEADER, FILE_XH, FILE_MACROS, FILE_METASTATE } fileType;
 
-/*@private@*/ typedef struct
+/*:private:*/ typedef struct
 {
   bool     ftemp     BOOLBITS;
   bool     fsystem   BOOLBITS;
   bool     fspecial  BOOLBITS;
-  cstring  fname;
+  /*@only@*/ cstring fname;
   cstring  basename;
   fileType ftype;
   fileId   fder;
@@ -34,7 +34,7 @@ typedef enum { FILE_NORMAL, FILE_LSLTEMP, FILE_NODELETE,
 typedef /*@only@*/ ftentry o_ftentry;
 
 typedef /*@only@*/ struct {
-  /*@dependent@*/ /*@exposed@*/ FILE *f;
+  /*@null@*/ /*@dependent@*/ /*@exposed@*/ FILE *f;
   /*@only@*/ cstring fname;
 } *foentry;
 
@@ -51,7 +51,7 @@ abst_typedef /*@null@*/ struct
 
   int nopen;
   int nopenspace;
-  /*@reldef@*/ /*@only@*/ foentry *openelements;
+  /*@reldef@*/ /*@only@*/ foentry *openelements; /* evans 2002-07-12: removed reldef */
 } *fileTable ;
 
 /*@constant null fileTable fileTable_undefined; @*/
@@ -68,6 +68,11 @@ extern /*@observer@*/ cstring fileTable_getName (fileTable p_ft, fileId p_fid) /
 extern /*@observer@*/ cstring fileTable_getNameBase (fileTable p_ft, fileId p_fid) ; 
 extern fileId fileTable_addFile (fileTable p_ft, cstring p_name)
    /*@modifies p_ft@*/ ;
+
+extern void fileTable_addStreamFile (fileTable p_ft, /*@dependent@*/ FILE *p_fstream,
+                                    cstring p_name)
+   /*@modifies p_ft@*/ ;
+
 extern fileId fileTable_addHeaderFile (fileTable p_ft, cstring p_name)
    /*@modifies p_ft@*/ ;
 extern fileId fileTable_addXHFile (fileTable p_ft, cstring p_name)
@@ -75,14 +80,11 @@ extern fileId fileTable_addXHFile (fileTable p_ft, cstring p_name)
 extern fileId fileTable_addLibraryFile (fileTable p_ft, cstring p_name)
    /*@modifies p_ft@*/ ;
 
-# ifndef NOLCL
 extern fileId fileTable_addLCLFile (fileTable p_ft, cstring p_name)
    /*@modifies p_ft@*/ ;
 
 extern fileId fileTable_addltemp (fileTable p_ft);
 
-# endif
-
 extern /*@notnull@*/ /*@only@*/ fileTable fileTable_create (void) /*@*/ ;
 extern fileId fileTable_lookup (fileTable p_ft, cstring p_s) /*@*/ ;
 extern fileId fileTable_addCTempFile (fileTable p_ft, fileId p_fid)
@@ -90,10 +92,8 @@ extern fileId fileTable_addCTempFile (fileTable p_ft, fileId p_fid)
 extern fileId fileTable_addFileOnly (fileTable p_ft, /*@only@*/ cstring p_name)
    /*@modifies p_ft@*/ ;
 
-# ifndef NOLCL
 extern fileId fileTable_addImportFile (fileTable p_ft, cstring p_name)
    /*@modifies p_ft@*/ ;
-# endif
 
 extern fileId fileTable_addMacrosFile (fileTable p_ft)
    /*@modifies p_ft@*/ ;
@@ -112,7 +112,7 @@ extern bool fileId_isHeader (fileId p_f) /*@*/ ;
 extern bool fileTable_sameBase (fileTable p_ft, fileId p_f1, fileId p_f2);
 extern void fileTable_cleanup (fileTable p_ft) /*@modifies fileSystem@*/;
 extern fileId fileTable_lookupBase (fileTable p_ft, cstring p_base) /*@modifies p_ft@*/ ;
-extern void fileTable_printTemps (fileTable p_ft) /*@modifies g_msgstream@*/ ;
+extern void fileTable_printTemps (fileTable p_ft) /*@modifies g_warningstream@*/ ;
 extern /*@unused@*/ /*@only@*/ cstring fileTable_unparse (fileTable p_ft) /*@*/ ;
 extern bool fileTable_exists (fileTable p_ft, cstring p_s) /*@*/ ;
 extern void fileTable_free (/*@only@*/ fileTable p_f);
@@ -120,24 +120,35 @@ extern bool fileTable_isSpecialFile (fileTable p_ft, fileId p_fid) /*@*/ ;
 extern bool fileTable_isSystemFile (fileTable p_ft, fileId p_fid) /*@*/ ;
 extern bool fileTable_isXHFile (fileTable p_ft, fileId p_fid) /*@*/ ;
 
-/*@-czechfcns@*/
-extern /*@observer@*/ cstring fileName (fileId p_fid) /*@*/ ;
-extern /*@observer@*/ cstring fileNameBase (fileId p_fid) /*@*/ ;
-extern /*@observer@*/ cstring rootFileName (fileId p_fid) /*@*/ ;
-/*@=czechfcns@*/
+extern /*@observer@*/ cstring fileTable_fileName (fileId p_fid) /*@*/ ;
+extern /*@observer@*/ cstring fileTable_fileNameBase (fileId p_fid) /*@*/ ;
+extern /*@observer@*/ cstring fileTable_rootFileName (fileId p_fid) /*@*/ ;
+
+extern /*@null@*/ /*@open@*/ /*@dependent@*/ FILE *fileTable_createFile (fileTable p_ft, cstring p_fname) 
+     /*@modifies p_ft, fileSystem@*/ ;
 
-# define fileName(fid)     (fileTable_getName(context_fileTable(), fid))
-# define fileNameBase(fid) (fileTable_getNameBase(context_fileTable(), fid))
-# define rootFileName(fid) (fileTable_getRootName(context_fileTable(), fid))
+extern /*@null@*/ /*@open@*/ /*@dependent@*/ FILE *fileTable_createMacrosFile (fileTable p_ft, cstring p_fname) 
+     /*@modifies p_ft, fileSystem@*/ ;
+
+# define fileTable_fileName(fid)     (fileTable_getName(context_fileTable(), fid))
+# define fileTable_fileNameBase(fid) (fileTable_getNameBase(context_fileTable(), fid))
+# define fileTable_rootFileName(fid) (fileTable_getRootName(context_fileTable(), fid))
 
 extern void fileTable_noDelete (fileTable, cstring);
 extern bool fileId_baseEqual (/*@sef@*/ fileId p_t1, /*@sef@*/ fileId p_t2) /*@*/ ;
 # define fileId_baseEqual(t1,t2) \
   (fileId_equal (t1, t2) || fileTable_sameBase (context_fileTable (), t1, t2))
 
+extern /*@null@*/ /*@open@*/ /*@dependent@*/ FILE *
+fileTable_openReadFile (fileTable p_ft, cstring p_fname) 
+     /*@modifies p_ft@*/ ;
+
+extern /*@null@*/ /*@open@*/ /*@dependent@*/ FILE *
+fileTable_openWriteFile (fileTable p_ft, cstring p_fname) 
+     /*@modifies p_ft@*/ ;
 
 extern /*@null@*/ /*@open@*/ /*@dependent@*/ FILE *
-fileTable_openFile (fileTable p_ft, cstring p_fname, /*@observer@*/ char *p_mode) 
+fileTable_openWriteUpdateFile (fileTable p_ft, cstring p_fname) 
      /*@modifies p_ft@*/ ;
 
 extern bool fileTable_closeFile (fileTable p_ft, FILE *p_f)