]> andersk Git - splint.git/blame - src/Headers/fileTable.h
Updating to use the LEnsures and LRequires instead of the ensures requires so
[splint.git] / src / Headers / fileTable.h
CommitLineData
885824d3 1/*
2** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
3** See ../LICENSE for license information.
4**
5*/
6/*
7** fileTable.h
8*/
9
10# ifndef FILETABLE_H
11# define FILETABLE_H
12
13/*@constant int FTBASESIZE; @*/
14# define FTBASESIZE 64
15
16/* moved to fileloc.h
17** typedef int fileId;
18*/
19
20typedef enum { FILE_NORMAL, FILE_LSLTEMP, FILE_NODELETE,
21 FILE_HEADER, FILE_MACROS } fileType;
22
23typedef struct _ftentry
24{
25 bool ftemp BOOLBITS;
26 bool fsystem BOOLBITS;
27 bool fspecial BOOLBITS;
28 cstring fname;
29 cstring basename;
30 fileType ftype;
31 fileId fder;
32} *ftentry;
33
34typedef /*@only@*/ ftentry o_ftentry;
35
36abst_typedef /*@null@*/ struct _fileTable
37{
38 int nentries;
39 int nspace;
40 hashTable htable;
41 /*@reldef@*/ /*@only@*/ o_ftentry *elements;
42} *fileTable ;
43
44/*@constant null fileTable fileTable_undefined; @*/
45# define fileTable_undefined ((fileTable) NULL)
46
47extern /*@unused@*/ /*@truenull@*/ bool
48 fileTable_isUndefined (/*@null@*/ fileTable p_f) /*@*/ ;
49extern /*@unused@*/ /*@falsenull@*/ bool
50 fileTable_isDefined (/*@null@*/ fileTable p_f) /*@*/ ;
51
52# define fileTable_isUndefined(ft) ((ft) == fileTable_undefined)
53# define fileTable_isDefined(ft) ((ft) != fileTable_undefined)
54extern /*@observer@*/ cstring fileTable_getName (fileTable p_ft, fileId p_fid) /*@*/ ;
55extern /*@observer@*/ cstring fileTable_getNameBase (fileTable p_ft, fileId p_fid) ;
56extern fileId fileTable_addFile (fileTable p_ft, cstring p_name)
57 /*@modifies p_ft@*/ ;
58extern fileId fileTable_addHeaderFile (fileTable p_ft, cstring p_name)
59 /*@modifies p_ft@*/ ;
60extern fileId fileTable_addLibraryFile (fileTable p_ft, cstring p_name)
61 /*@modifies p_ft@*/ ;
62
63# ifndef NOLCL
64extern fileId fileTable_addLCLFile (fileTable p_ft, cstring p_name)
65 /*@modifies p_ft@*/ ;
66
67extern fileId fileTable_addltemp (fileTable p_ft);
68
69# endif
70
71extern /*@notnull@*/ /*@only@*/ fileTable fileTable_create (void) /*@*/ ;
72extern fileId fileTable_lookup (fileTable p_ft, cstring p_s) /*@*/ ;
73extern fileId fileTable_addCTempFile (fileTable p_ft, fileId p_fid)
74 /*@modifies p_ft@*/ ;
75extern fileId fileTable_addFileOnly (fileTable p_ft, /*@only@*/ cstring p_name)
76 /*@modifies p_ft@*/ ;
77
78# ifndef NOLCL
79extern fileId fileTable_addImportFile (fileTable p_ft, cstring p_name)
80 /*@modifies p_ft@*/ ;
81# endif
82
83extern fileId fileTable_addMacrosFile (fileTable p_ft)
84 /*@modifies p_ft@*/ ;
85extern /*@observer@*/ cstring fileTable_getRootName (fileTable p_ft, fileId p_fid) /*@*/ ;
86extern bool fileTable_isHeader (fileTable p_ft, fileId p_fid) /*@*/ ;
87extern bool fileId_isHeader (fileId p_f) /*@*/ ;
88# define fileId_isHeader(f) (fileTable_isHeader (context_fileTable(), f))
89
90extern bool fileTable_sameBase (fileTable p_ft, fileId p_f1, fileId p_f2);
91extern void fileTable_cleanup (fileTable p_ft) /*@modifies fileSystem@*/;
92extern fileId fileTable_lookupBase (fileTable p_ft, cstring p_base) /*@modifies p_ft@*/ ;
93extern void fileTable_printTemps (fileTable p_ft) /*@modifies g_msgstream@*/ ;
94extern /*@unused@*/ /*@only@*/ cstring fileTable_unparse (fileTable p_ft) /*@*/ ;
95extern bool fileTable_exists (fileTable p_ft, cstring p_s) /*@*/ ;
96extern void fileTable_free (/*@only@*/ fileTable p_f);
97extern bool fileTable_isSpecialFile (fileTable p_ft, fileId p_fid) /*@*/ ;
98extern bool fileTable_isSystemFile (fileTable p_ft, fileId p_fid) /*@*/ ;
99
100/*@-czechfcns@*/
101extern /*@observer@*/ cstring fileName (fileId p_fid) /*@*/ ;
102extern /*@observer@*/ cstring fileNameBase (fileId p_fid) /*@*/ ;
103extern /*@observer@*/ cstring rootFileName (fileId p_fid) /*@*/ ;
104/*@=czechfcns@*/
105
106# define fileName(fid) (fileTable_getName(context_fileTable(), fid))
107# define fileNameBase(fid) (fileTable_getNameBase(context_fileTable(), fid))
108# define rootFileName(fid) (fileTable_getRootName(context_fileTable(), fid))
109
110extern void fileTable_noDelete (fileTable, cstring);
111extern bool fileId_baseEqual (/*@sef@*/ fileId p_t1, /*@sef@*/ fileId p_t2) /*@*/ ;
112# define fileId_baseEqual(t1,t2) \
113 (fileId_equal (t1, t2) || fileTable_sameBase (context_fileTable (), t1, t2))
114
115# else
116# error "Multiple include"
117#endif
118
This page took 0.060456 seconds and 5 git commands to generate.