]> andersk Git - splint.git/blobdiff - src/Headers/fileTable.h
Fixes after removing -unrecogcomments flag for make splintme.
[splint.git] / src / Headers / fileTable.h
index 33c0d2ffe0eef7ee8f827965abeeb107d978131c..607bec1004248f52196f140b00622f59137a095e 100644 (file)
@@ -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.
 **
 */
 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;
@@ -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; @*/
@@ -80,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)
@@ -95,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@*/ ;
@@ -129,6 +124,12 @@ 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@*/ ;
+
+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))
@@ -138,9 +139,16 @@ 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) 
This page took 0.033042 seconds and 4 git commands to generate.