X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/885824d34f6f6626fde2fb041801408cbaf1f6f1..HEAD:/src/Headers/fileloc.h diff --git a/src/Headers/fileloc.h b/src/Headers/fileloc.h index 590353c..7b7f7b3 100644 --- a/src/Headers/fileloc.h +++ b/src/Headers/fileloc.h @@ -1,5 +1,5 @@ /* -** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000. +** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. ** See ../LICENSE for license information. ** */ @@ -18,7 +18,7 @@ typedef enum FL_PREPROC, FL_RC, FL_EXTERNAL } flkind; -struct __fileloc +struct s_fileloc { flkind kind; fileId fid; @@ -34,11 +34,9 @@ extern fileloc fileloc_update (/*@only@*/ fileloc p_old, fileloc p_fnew) extern fileloc fileloc_create (fileId p_fid, int p_line, int p_col) /*@*/ ; extern bool fileloc_isSystemFile (fileloc p_f1) /*@*/ ; +extern bool fileloc_isXHFile (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) /*@*/ ; @@ -46,11 +44,9 @@ 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 void fileloc_destroyMod (void) /*@modifies internalState@*/ ; 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) /*@*/ ; @@ -59,6 +55,7 @@ extern 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 bool fileloc_sameFileAndLine (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) /*@*/ ; @@ -81,22 +78,19 @@ 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 /*@falsewhennull@*/ bool fileloc_isDefined (/*@null@*/ fileloc p_f) /*@*/ ; +extern /*@nullwhentrue@*/ 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_undefined ((fileloc) NULL) # 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) @@ -113,13 +107,11 @@ extern /*@unused@*/ bool fileloc_columnDefined (/*@sef@*/ fileloc p_f) /*@*/ ; # 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); +extern /*@falsewhennull@*/ bool fileloc_isValid (/*@sef@*/ fileloc p_f); # define fileloc_isValid(f) \ (fileloc_isDefined(f) && ((f)->lineno >= 0)) @@ -165,16 +157,20 @@ 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 /*@only@*/ cstring fileloc_outputFilename (fileloc) /*@*/ ; +extern bool fileloc_isStandardLibrary (fileloc p_f) /*@*/ ; 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) /*@*/ ; +extern bool fileloc_storable (/*@sef@*/ fileloc p_f) /*@*/; +# define fileloc_storable(f) ((f) != g_currentloc || fileloc_isBuiltin (f) || fileloc_isExternal (f)) + + # else # error "Multiple include" # endif