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

/*
** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
** See ../LICENSE for license information.
**
*/
/*
** fileloc.h
*/

# ifndef FILELOC_H
# define FILELOC_H

# include "fileId.h"

typedef enum 
{ 
  FL_NORMAL, FL_SPEC, FL_LIB, FL_STDLIB, FL_STDHDR, FL_IMPORT, FL_BUILTIN,
  FL_PREPROC, FL_RC, FL_EXTERNAL
} flkind;

struct __fileloc
{
  flkind  kind;
  fileId  fid;
  int     lineno;
  int     column;
} ;

/* typedef in forwardTypes */
typedef /*@only@*/ fileloc o_fileloc;

extern fileloc fileloc_update (/*@only@*/ fileloc p_old, fileloc p_fnew) 
   /*@modifies p_old@*/ ;

extern fileloc fileloc_create (fileId p_fid, int p_line, int p_col) /*@*/ ;
extern bool fileloc_isSystemFile (fileloc p_f1) /*@*/ ;

# ifndef NOLCL
extern fileloc fileloc_createSpec (fileId p_fid, int p_line, int p_col) /*@*/ ;
# endif

extern fileloc fileloc_createLib (cstring p_ln) /*@*/ ;
extern fileloc fileloc_createRc (cstring p_name) /*@*/ ;
extern fileloc fileloc_decColumn (fileloc p_f, int p_x) /*@*/ ;
extern void fileloc_subColumn (fileloc p_f, int p_x) /*@modifies p_f@*/ ;
extern fileloc fileloc_getBuiltin (void) /*@*/ ;
extern /*@observer@*/ fileloc fileloc_observeBuiltin (void) /*@*/ ;
extern fileloc fileloc_createBuiltin (void) /*@*/ ;

# ifndef NOLCL
extern fileloc fileloc_createImport (cstring p_fname, int p_lineno) /*@*/ ;
# endif

extern bool fileloc_isSpecialFile (fileloc p_f) /*@*/ ;
extern bool fileloc_sameBaseFile (fileloc p_f1, fileloc p_f2) /*@*/ ;
extern /*@observer@*/ cstring fileloc_filename (fileloc p_f) /*@*/ ;
extern int fileloc_column (fileloc p_f) /*@*/ ;
extern /*@only@*/ cstring fileloc_unparse (fileloc p_f) /*@*/ ;
extern cstring fileloc_unparseRaw (cstring p_fname, int p_lineno) /*@*/ ;
extern cstring fileloc_unparseRawCol (cstring p_fname, int p_lineno, int p_col) /*@*/ ;
extern bool fileloc_sameFile (fileloc p_f1, fileloc p_f2) /*@*/ ;
extern void fileloc_free (/*@only@*/ fileloc p_f);
extern void fileloc_reallyFree (/*@only@*/ fileloc p_f);
extern int fileloc_lineno (fileloc p_f) /*@*/ ;
extern bool fileloc_equal (fileloc p_f1, fileloc p_f2) /*@*/ ;
extern bool fileloc_lessthan (fileloc p_f1, fileloc p_f2) /*@*/ ;
extern int fileloc_compare (fileloc p_f1, fileloc p_f2) /*@*/ ;
extern /*@observer@*/ cstring fileloc_getBase (fileloc p_f) /*@*/ ;
extern bool fileloc_isHeader (fileloc p_f) /*@*/ ;
extern bool fileloc_isSpec (fileloc p_f) /*@*/ ;
extern bool fileloc_isRealSpec (fileloc p_f) /*@*/ ;
extern fileloc fileloc_copy (fileloc p_f) /*@*/ ;
extern cstring fileloc_unparseDirect (fileloc p_fl) /*@*/ ;
extern bool fileloc_notAfter (fileloc p_f1, fileloc p_f2) /*@*/ ;
extern bool fileloc_almostSameFile (fileloc p_f1, fileloc p_f2) /*@*/ ;
extern fileloc fileloc_noColumn (fileloc p_f) /*@*/ ;
extern /*@observer@*/ fileloc fileloc_getExternal (void) /*@*/ ;
extern fileloc fileloc_createExternal (void) /*@*/ ;

extern bool fileloc_isExternal (/*@sef@*/ fileloc p_f) /*@*/;
# define fileloc_isExternal(f) \
     (fileloc_isDefined(f) && ((f)->kind == FL_EXTERNAL))

extern /*@falsenull@*/ bool fileloc_isDefined (/*@null@*/ fileloc p_f) /*@*/ ;
extern /*@truenull@*/ bool fileloc_isUndefined (/*@null@*/ fileloc p_f) /*@*/ ;
extern bool fileloc_isInvalid (/*@sef@*/ /*@null@*/ fileloc p_f) /*@*/ ;

/*@constant null fileloc fileloc_undefined; @*/
# define fileloc_undefined      ((fileloc)0)
# define fileloc_isDefined(f)   ((f) != fileloc_undefined)
# define fileloc_isUndefined(f) ((f) == fileloc_undefined)
# define fileloc_isInvalid(f)   (!(fileloc_isValid(f)))

extern bool fileloc_isLib (fileloc p_f) /*@*/ ;
extern bool fileloc_isRealLib (fileloc p_f) /*@*/ ;

# ifndef NOLCL
extern fileloc fileloc_fromTok (ltoken p_t) /*@*/ ;
# endif

/*@constant int UNKNOWN_LINE; @*/
# define UNKNOWN_LINE (0)

/*@constant int UNKNOWN_COLUMN; @*/
# define UNKNOWN_COLUMN (0)

extern /*@unused@*/ bool fileloc_linenoDefined (/*@sef@*/ fileloc p_f) /*@*/ ;
extern /*@unused@*/ bool fileloc_columnDefined (/*@sef@*/ fileloc p_f) /*@*/ ;

# define fileloc_linenoDefined(f) \
  (fileloc_isValid (f) && (f)->lineno != UNKNOWN_LINE)

# define fileloc_columnDefined(f) \
  (fileloc_isValid (f) && (f)->column != UNKNOWN_COLUMN)

# ifndef NOLCL
extern void fileloc_setColumnUndefined (/*@sef@*/ fileloc p_f) /*@modifies p_f@*/;
# define fileloc_setColumnUndefined(f) \
  (fileloc_isDefined(f) ? (f)->column = UNKNOWN_COLUMN : UNKNOWN_COLUMN)
# endif

extern /*@falsenull@*/ bool fileloc_isValid (/*@sef@*/ fileloc p_f);
# define fileloc_isValid(f) \
  (fileloc_isDefined(f) && ((f)->lineno >= 0))

extern bool fileloc_isImport (/*@sef@*/ fileloc p_fl);
# define fileloc_isImport(fl)  (fileloc_isDefined(fl) && (fl)->kind == FL_IMPORT)

extern bool fileloc_isPreproc (/*@sef@*/ fileloc p_fl);
# define fileloc_isPreproc(fl)  (fileloc_isDefined(fl) && (fl)->kind == FL_PREPROC)

extern void fileloc_setLineno (/*@sef@*/ fileloc p_f, int p_i) /*@modifies p_f@*/ ;
# define fileloc_setLineno(fl, i) \
      (fileloc_isDefined(fl) ? ((fl)->lineno = (i), (fl)->column = 1) : (i))

extern void fileloc_nextLine (/*@sef@*/ fileloc p_f) /*@modifies p_f@*/ ;
# define fileloc_nextLine(fl) \
      (fileloc_isDefined(fl) ? ((fl)->lineno++, (fl)->column = 1) : 0)

extern void fileloc_addLine (/*@sef@*/ fileloc p_f, int p_i) /*@modifies p_f@*/ ;
# define fileloc_addLine(fl, i) \
      (fileloc_isDefined(fl) ? ((fl)->lineno += (i), (fl)->column = 1) : (i))

extern fileId fileloc_fileId (/*@sef@*/ fileloc p_fl) /*@*/ ;
# define fileloc_fileId(fl) \
      (fileloc_isDefined (fl) ? (fl)->fid : fileId_invalid)

extern void fileloc_setColumn (/*@sef@*/ fileloc p_fl, int p_i) /*@modifies p_fl@*/ ;
# define fileloc_setColumn(fl, i) \
      (fileloc_isDefined (fl) ? ((fl)->column = (i)) : (i))

extern void fileloc_addColumn (/*@sef@*/ fileloc p_fl, int p_i) /*@modifies p_fl@*/ ;
# define fileloc_addColumn(fl, i) \
      (fileloc_isDefined (fl) ? ((fl)->column += (i)) : (i))

extern void fileloc_incColumn (/*@sef@*/ fileloc p_fl) /*@modifies p_fl@*/ ;
# define fileloc_incColumn(fl) \
      (fileloc_isDefined (fl) ? ((fl)->column++) : 0)

extern bool fileloc_isBuiltin (/*@sef@*/ fileloc p_fl) /*@*/ ;
# define fileloc_isBuiltin(fl) \
   (fileloc_isDefined (fl) && ((fl)->kind == FL_BUILTIN))

extern fileloc fileloc_updateFileId (/*@only@*/ fileloc p_old, fileId p_s) /*@*/ ;
extern fileloc fileloc_makePreproc (fileloc p_loc) /*@*/ ;
extern fileloc fileloc_makePreprocPrevious (fileloc p_loc) /*@*/ ;

# ifndef NOLCL
extern bool fileloc_isStandardLibrary (fileloc p_f) /*@*/ ;
# endif

extern bool fileloc_isStandardLib (fileloc p_f) /*@*/ ;
extern cstring fileloc_unparseFilename (fileloc p_f) /*@*/ ;
extern bool fileloc_withinLines (fileloc p_f1, fileloc p_f2, int p_n) /*@*/ ;
extern bool fileloc_isUser (fileloc p_f) /*@*/ ;
extern bool fileloc_sameModule (fileloc p_f1, fileloc p_f2) /*@*/ ;

# else
# error "Multiple include"
# endif
Commit	Line	Data
885824d3	1	/*
	2	** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
	3	** See ../LICENSE for license information.
	4	**
	5	*/
	6	/*
	7	** fileloc.h
	8	*/
	9
	10	# ifndef FILELOC_H
	11	# define FILELOC_H
	12
	13	# include "fileId.h"
	14
	15	typedef enum
	16	{
	17	FL_NORMAL, FL_SPEC, FL_LIB, FL_STDLIB, FL_STDHDR, FL_IMPORT, FL_BUILTIN,
bb25bea6	18	FL_PREPROC, FL_RC, FL_EXTERNAL
885824d3	19	} flkind;
	20
	21	struct __fileloc
	22	{
	23	flkind kind;
	24	fileId fid;
	25	int lineno;
	26	int column;
	27	} ;
	28
	29	/* typedef in forwardTypes */
	30	typedef /@only@/ fileloc o_fileloc;
	31
	32	extern fileloc fileloc_update (/@only@/ fileloc p_old, fileloc p_fnew)
	33	/@modifies p_old@/ ;
	34
	35	extern fileloc fileloc_create (fileId p_fid, int p_line, int p_col) /@/ ;
	36	extern bool fileloc_isSystemFile (fileloc p_f1) /@/ ;
	37
	38	# ifndef NOLCL
	39	extern fileloc fileloc_createSpec (fileId p_fid, int p_line, int p_col) /@/ ;
	40	# endif
	41
	42	extern fileloc fileloc_createLib (cstring p_ln) /@/ ;
	43	extern fileloc fileloc_createRc (cstring p_name) /@/ ;
	44	extern fileloc fileloc_decColumn (fileloc p_f, int p_x) /@/ ;
	45	extern void fileloc_subColumn (fileloc p_f, int p_x) /@modifies p_f@/ ;
	46	extern fileloc fileloc_getBuiltin (void) /@/ ;
	47	extern /@observer@/ fileloc fileloc_observeBuiltin (void) /@/ ;
	48	extern fileloc fileloc_createBuiltin (void) /@/ ;
	49
	50	# ifndef NOLCL
	51	extern fileloc fileloc_createImport (cstring p_fname, int p_lineno) /@/ ;
	52	# endif
	53
	54	extern bool fileloc_isSpecialFile (fileloc p_f) /@/ ;
	55	extern bool fileloc_sameBaseFile (fileloc p_f1, fileloc p_f2) /@/ ;
	56	extern /@observer@/ cstring fileloc_filename (fileloc p_f) /@/ ;
	57	extern int fileloc_column (fileloc p_f) /@/ ;
d46ce6a4	58	extern /@only@/ cstring fileloc_unparse (fileloc p_f) /@/ ;
885824d3	59	extern cstring fileloc_unparseRaw (cstring p_fname, int p_lineno) /@/ ;
	60	extern cstring fileloc_unparseRawCol (cstring p_fname, int p_lineno, int p_col) /@/ ;
	61	extern bool fileloc_sameFile (fileloc p_f1, fileloc p_f2) /@/ ;
	62	extern void fileloc_free (/@only@/ fileloc p_f);
	63	extern void fileloc_reallyFree (/@only@/ fileloc p_f);
	64	extern int fileloc_lineno (fileloc p_f) /@/ ;
	65	extern bool fileloc_equal (fileloc p_f1, fileloc p_f2) /@/ ;
	66	extern bool fileloc_lessthan (fileloc p_f1, fileloc p_f2) /@/ ;
	67	extern int fileloc_compare (fileloc p_f1, fileloc p_f2) /@/ ;
	68	extern /@observer@/ cstring fileloc_getBase (fileloc p_f) /@/ ;
	69	extern bool fileloc_isHeader (fileloc p_f) /@/ ;
	70	extern bool fileloc_isSpec (fileloc p_f) /@/ ;
	71	extern bool fileloc_isRealSpec (fileloc p_f) /@/ ;
	72	extern fileloc fileloc_copy (fileloc p_f) /@/ ;
	73	extern cstring fileloc_unparseDirect (fileloc p_fl) /@/ ;
	74	extern bool fileloc_notAfter (fileloc p_f1, fileloc p_f2) /@/ ;
	75	extern bool fileloc_almostSameFile (fileloc p_f1, fileloc p_f2) /@/ ;
	76	extern fileloc fileloc_noColumn (fileloc p_f) /@/ ;
	77	extern /@observer@/ fileloc fileloc_getExternal (void) /@/ ;
	78	extern fileloc fileloc_createExternal (void) /@/ ;
	79
	80	extern bool fileloc_isExternal (/@sef@/ fileloc p_f) /@/;
	81	# define fileloc_isExternal(f) \
	82	(fileloc_isDefined(f) && ((f)->kind == FL_EXTERNAL))
	83
	84	extern /@falsenull@/ bool fileloc_isDefined (/@null@/ fileloc p_f) /@/ ;
	85	extern /@truenull@/ bool fileloc_isUndefined (/@null@/ fileloc p_f) /@/ ;
	86	extern bool fileloc_isInvalid (/@sef@/ /@null@/ fileloc p_f) /@/ ;
	87
	88	/@constant null fileloc fileloc_undefined; @/
	89	# define fileloc_undefined ((fileloc)0)
	90	# define fileloc_isDefined(f) ((f) != fileloc_undefined)
	91	# define fileloc_isUndefined(f) ((f) == fileloc_undefined)
	92	# define fileloc_isInvalid(f) (!(fileloc_isValid(f)))
	93
	94	extern bool fileloc_isLib (fileloc p_f) /@/ ;
	95	extern bool fileloc_isRealLib (fileloc p_f) /@/ ;
	96
	97	# ifndef NOLCL
	98	extern fileloc fileloc_fromTok (ltoken p_t) /@/ ;
	99	# endif
	100
	101	/@constant int UNKNOWN_LINE; @/
	102	# define UNKNOWN_LINE (0)
	103
	104	/@constant int UNKNOWN_COLUMN; @/
	105	# define UNKNOWN_COLUMN (0)
	106
	107	extern /@unused@/ bool fileloc_linenoDefined (/@sef@/ fileloc p_f) /@/ ;
	108	extern /@unused@/ bool fileloc_columnDefined (/@sef@/ fileloc p_f) /@/ ;
	109
	110	# define fileloc_linenoDefined(f) \
	111	(fileloc_isValid (f) && (f)->lineno != UNKNOWN_LINE)
	112
	113	# define fileloc_columnDefined(f) \
	114	(fileloc_isValid (f) && (f)->column != UNKNOWN_COLUMN)
	115
	116	# ifndef NOLCL
	117	extern void fileloc_setColumnUndefined (/@sef@/ fileloc p_f) /@modifies p_f@/;
	118	# define fileloc_setColumnUndefined(f) \
	119	(fileloc_isDefined(f) ? (f)->column = UNKNOWN_COLUMN : UNKNOWN_COLUMN)
	120	# endif
	121
	122	extern /@falsenull@/ bool fileloc_isValid (/@sef@/ fileloc p_f);
123	# define fileloc_isValid(f) \
124	(fileloc_isDefined(f) && ((f)->lineno >= 0))
125
126	extern bool fileloc_isImport (/@sef@/ fileloc p_fl);
127	# define fileloc_isImport(fl) (fileloc_isDefined(fl) && (fl)->kind == FL_IMPORT)
128
129	extern bool fileloc_isPreproc (/@sef@/ fileloc p_fl);
130	# define fileloc_isPreproc(fl) (fileloc_isDefined(fl) && (fl)->kind == FL_PREPROC)
131
132	extern void fileloc_setLineno (/@sef@/ fileloc p_f, int p_i) /@modifies p_f@/ ;
133	# define fileloc_setLineno(fl, i) \
134	(fileloc_isDefined(fl) ? ((fl)->lineno = (i), (fl)->column = 1) : (i))
135
136	extern void fileloc_nextLine (/@sef@/ fileloc p_f) /@modifies p_f@/ ;
137	# define fileloc_nextLine(fl) \
138	(fileloc_isDefined(fl) ? ((fl)->lineno++, (fl)->column = 1) : 0)
139
140	extern void fileloc_addLine (/@sef@/ fileloc p_f, int p_i) /@modifies p_f@/ ;
141	# define fileloc_addLine(fl, i) \
142	(fileloc_isDefined(fl) ? ((fl)->lineno += (i), (fl)->column = 1) : (i))
143
144	extern fileId fileloc_fileId (/@sef@/ fileloc p_fl) /@/ ;
145	# define fileloc_fileId(fl) \
146	(fileloc_isDefined (fl) ? (fl)->fid : fileId_invalid)
147
148	extern void fileloc_setColumn (/@sef@/ fileloc p_fl, int p_i) /@modifies p_fl@/ ;
149	# define fileloc_setColumn(fl, i) \
150	(fileloc_isDefined (fl) ? ((fl)->column = (i)) : (i))
151
152	extern void fileloc_addColumn (/@sef@/ fileloc p_fl, int p_i) /@modifies p_fl@/ ;
153	# define fileloc_addColumn(fl, i) \
154	(fileloc_isDefined (fl) ? ((fl)->column += (i)) : (i))
155
156	extern void fileloc_incColumn (/@sef@/ fileloc p_fl) /@modifies p_fl@/ ;
157	# define fileloc_incColumn(fl) \
158	(fileloc_isDefined (fl) ? ((fl)->column++) : 0)
159
160	extern bool fileloc_isBuiltin (/@sef@/ fileloc p_fl) /@/ ;
161	# define fileloc_isBuiltin(fl) \
162	(fileloc_isDefined (fl) && ((fl)->kind == FL_BUILTIN))
163
164	extern fileloc fileloc_updateFileId (/@only@/ fileloc p_old, fileId p_s) /@/ ;
165	extern fileloc fileloc_makePreproc (fileloc p_loc) /@/ ;
166	extern fileloc fileloc_makePreprocPrevious (fileloc p_loc) /@/ ;
167
168	# ifndef NOLCL
169	extern bool fileloc_isStandardLibrary (fileloc p_f) /@/ ;
170	# endif
171
172	extern bool fileloc_isStandardLib (fileloc p_f) /@/ ;
173	extern cstring fileloc_unparseFilename (fileloc p_f) /@/ ;
174	extern bool fileloc_withinLines (fileloc p_f1, fileloc p_f2, int p_n) /@/ ;
175	extern bool fileloc_isUser (fileloc p_f) /@/ ;
176	extern bool fileloc_sameModule (fileloc p_f1, fileloc p_f2) /@/ ;
177
178	# else
179	# error "Multiple include"
180	# endif
181
182
183
184
185
186