1 /* 2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. 3 ** See ../LICENSE for license information. 4 */ 5 /* 6 ** usymtab.h 7 */ 8 9 # ifndef USYMTAB_H 10 # define USYMTAB_H 11 12 /*@constant null usymtab GLOBAL_ENV; @*/ 13 # define GLOBAL_ENV usymtab_undefined 14 15 typedef enum { 16 US_GLOBAL, 17 US_NORMAL, 18 US_TBRANCH, US_FBRANCH, 19 US_CBRANCH, US_SWITCH 20 } uskind; 21 22 typedef struct { int level; int index; } *refentry; 23 typedef /*@only@*/ refentry o_refentry; 24 typedef o_refentry *refTable; 25 26 struct s_usymtab 27 { 28 uskind kind; 29 int nentries; 30 int nspace; 31 int lexlevel; 32 bool mustBreak; 33 exitkind exitCode; 34 /*@reldef@*/ /*@only@*/ o_uentry *entries; 35 /*@null@*/ /*@only@*/ cstringTable htable; /* for the global environment */ 36 /*@null@*/ /*@only@*/ refTable reftable; /* for branched environments */ 37 /*@only@*/ guardSet guards; /* guarded references (not null) */ 38 aliasTable aliases; 39 /*@owned@*/ usymtab env; 40 } ; 41 42 /* 43 ** rep invariant: 44 ** 45 ** (left as exercise to reader) ;) 46 */ 47 48 extern void usymtab_printTypes (void) 49 /*@globals internalState@*/ 50 /*@modifies g_warningstream@*/ ; 51 52 extern void usymtab_setMustBreak (void) /*@modifies internalState@*/ ; 53 54 extern bool usymtab_inGlobalScope (void) /*@globals internalState@*/ ; 55 extern bool usymtab_inFunctionScope (void) /*@globals internalState@*/ ; 56 extern bool usymtab_inFileScope (void) /*@globals internalState@*/ ; 57 extern void usymtab_checkFinalScope (bool p_isReturn) 58 /*@globals internalState@*/ 59 /*@modifies *g_warningstream@*/ ; 60 61 extern void usymtab_allUsed (void) 62 /*@globals internalState@*/ 63 /*@modifies *g_warningstream@*/ ; 64 65 extern void usymtab_allDefined (void) 66 /*@globals internalState@*/ 67 /*@modifies *g_warningstream@*/ ; 68 69 extern void usymtab_prepareDump (void) 70 /*@modifies internalState@*/ ; 71 72 extern void usymtab_dump (FILE *p_fout) 73 /*@globals internalState@*/ 74 /*@modifies *p_fout@*/ ; 75 76 77 extern void usymtab_load (FILE *p_f) /*@modifies p_f, internalState@*/ ; 78 79 extern /*@exposed@*/ /*@dependent@*/ uentry 80 usymtab_getRefQuiet (int p_level, usymId p_index) 81 /*@globals internalState@*/ ; 82 83 extern void usymtab_printLocal (void) 84 /*@globals internalState@*/ 85 /*@modifies stdout@*/ ; 86 87 extern /*@exposed@*/ /*@dependent@*/ uentry usymtab_getParam (int p_paramno) 88 /*@globals internalState@*/; 89 extern void usymtab_free (void) /*@modifies internalState@*/ ; 90 extern bool usymtab_inDeepScope (void) /*@globals internalState@*/ ; 91 92 extern /*@exposed@*/ uentry usymtab_lookupExpose (cstring p_k) 93 /*@globals internalState@*/ ; 94 95 extern /*@observer@*/ uentry usymtab_lookup (cstring p_k) 96 /*@globals internalState@*/ ; 97 98 # define usymtab_lookup(s) (usymtab_lookupExpose (s)) 99 100 extern /*@observer@*/ uentry usymtab_lookupGlob (cstring p_k) 101 /*@globals internalState@*/ ; 102 extern /*@exposed@*/ uentry usymtab_lookupExposeGlob (cstring p_k) 103 /*@globals internalState@*/ ; 104 extern /*@observer@*/ uentry usymtab_lookupUnionTag (cstring p_k) 105 /*@globals internalState@*/ ; 106 extern /*@observer@*/ uentry usymtab_lookupStructTag (cstring p_k) 107 /*@globals internalState@*/ ; 108 extern /*@observer@*/ uentry usymtab_lookupEither (cstring p_k) 109 /*@globals internalState@*/ ; 110 111 extern ctype usymtab_lookupType (cstring p_k) 112 /*@globals internalState@*/ ; 113 114 extern bool usymtab_isDefinitelyNull (sRef p_s) 115 /*@globals internalState@*/ ; 116 extern bool usymtab_isDefinitelyNullDeep (sRef p_s) 117 /*@globals internalState@*/ ; 118 119 extern usymId usymtab_supExposedTypeEntry (/*@only@*/ uentry p_e, bool p_dodef) 120 /*@modifies internalState, p_e@*/ ; 121 122 extern ctype usymtab_supTypeEntry (/*@only@*/ uentry p_e) 123 /*@modifies internalState, p_e@*/ ; 124 125 extern /*@exposed@*/ uentry usymtab_supReturnTypeEntry (/*@only@*/ uentry p_e) 126 /*@modifies internalState@*/ ; 127 128 extern /*@observer@*/ uentry usymtab_lookupSafe (cstring p_k) 129 /*@globals internalState@*/ ; 130 131 extern /*@observer@*/ uentry 132 usymtab_lookupSafeScope (cstring p_k, int p_lexlevel) 133 /*@globals internalState@*/ ; 134 135 extern /*@observer@*/ uentry usymtab_getGlobalEntry (usymId p_uid) 136 /*@globals internalState@*/ ; 137 138 extern bool usymtab_exists (cstring p_k) 139 /*@globals internalState@*/ ; 140 141 extern bool usymtab_existsVar (cstring p_k) 142 /*@globals internalState@*/ ; 143 144 extern bool usymtab_existsGlob (cstring p_k) 145 /*@globals internalState@*/ ; 146 147 extern bool usymtab_existsType (cstring p_k) 148 /*@globals internalState@*/ ; 149 150 extern bool usymtab_existsEither (cstring p_k) 151 /*@globals internalState@*/ ; 152 153 extern bool usymtab_existsTypeEither (cstring p_k) 154 /*@globals internalState@*/ ; 155 156 extern usymId usymtab_getId (cstring p_k) /*@globals internalState@*/ ; 157 extern typeId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ; 158 159 extern void usymtab_supEntry (/*@only@*/ uentry p_e) 160 /*@modifies internalState, p_e@*/ ; 161 162 extern void usymtab_replaceEntry (/*@only@*/ uentry p_s) 163 /*@modifies internalState, p_s@*/ ; 164 165 extern void usymtab_supEntrySref (/*@only@*/ uentry p_e) 166 /*@modifies internalState, p_e@*/ ; 167 168 extern void usymtab_supGlobalEntry (/*@only@*/ uentry p_e) 169 /*@modifies internalState@*/ ; 170 171 extern void usymtab_addGlobalEntry (/*@only@*/ uentry p_e) 172 /*@modifies internalState, p_e@*/ ; 173 174 extern /*@exposed@*/ uentry 175 usymtab_supEntryReturn (/*@only@*/ uentry p_e) 176 /*@modifies internalState, p_e@*/ ; 177 178 extern usymId usymtab_addEntry (/*@only@*/ uentry p_e) 179 /*@modifies internalState, p_e@*/ ; 180 181 extern ctype usymtab_lookupAbstractType (cstring p_k) 182 /*@globals internalState@*/ /*@modifies nothing@*/ ; 183 184 extern bool usymtab_matchForwardStruct (typeId p_u1, typeId p_u2) 185 /*@globals internalState@*/ ; 186 187 extern bool usymtab_existsEnumTag (cstring p_k) 188 /*@globals internalState@*/ ; 189 extern bool usymtab_existsUnionTag (cstring p_k) 190 /*@globals internalState@*/ ; 191 extern bool usymtab_existsStructTag (cstring p_k) 192 /*@globals internalState@*/ ; 193 194 /*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/ 195 # define usymtab_entries(x, m_i) \ 196 { int m_ind; \ 197 if (usymtab_isDefined (x)) \ 198 for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \ 199 { uentry m_i = (x)->entries[m_ind]; 200 201 # define end_usymtab_entries }} 202 203 extern /*@unused@*/ void usymtab_displayAllUses (void) 204 /*@globals internalState@*/ 205 /*@modifies *g_warningstream@*/ ; 206 207 extern /*@unused@*/ void usymtab_printOut (void) 208 /*@globals internalState@*/ 209 /*@modifies *g_warningstream@*/ ; 210 211 extern /*@unused@*/ void usymtab_printAll (void) 212 /*@globals internalState@*/ 213 /*@modifies *g_warningstream@*/ ; 214 215 extern void usymtab_enterScope (void) 216 /*@modifies internalState;@*/ ; 217 extern void usymtab_enterFunctionScope (uentry p_fcn) 218 /*@modifies internalState;@*/ ; 219 extern void usymtab_quietExitScope (fileloc p_loc) 220 /*@modifies internalState;@*/ ; 221 extern void usymtab_exitScope (exprNode p_expr) /*@modifies internalState@*/ ; 222 extern void usymtab_addGuards (guardSet p_guards) /*@modifies internalState@*/ ; 223 extern void usymtab_setExitCode (exitkind p_ex) /*@modifies internalState@*/ ; 224 extern void usymtab_exitFile (void) /*@modifies internalState@*/ ; 225 extern void usymtab_enterFile (void) /*@modifies internalState@*/ ; 226 227 extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k) 228 /*@globals internalState@*/ ; 229 230 extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ; 231 extern typeId usymtab_convertTypeId (typeId p_uid) /*@globals internalState@*/ ; 232 extern void usymtab_initMod (void) /*@modifies internalState@*/ ; 233 extern void usymtab_destroyMod (void) /*@modifies internalState@*/ ; 234 extern void usymtab_initBool (void) /*@modifies internalState@*/ ; 235 extern void usymtab_initGlobalMarker (void) /*@modifies internalState@*/ ; 236 237 extern void usymtab_exportHeader (void) 238 /*@modifies internalState@*/ ; 239 240 extern ctype usymtab_structFieldsType (uentryList p_f) 241 /*@globals internalState@*/ ; 242 243 extern ctype usymtab_unionFieldsType (uentryList p_f) 244 /*@globals internalState@*/ ; 245 246 extern ctype usymtab_enumEnumNameListType (enumNameList p_f) 247 /*@globals internalState@*/ ; 248 249 extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (typeId p_uid) 250 /*@globals internalState@*/ ; 251 252 extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr) 253 /*@modifies internalState@*/ ; 254 extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr) 255 /*@modifies internalState@*/ ; 256 257 extern void usymtab_trueBranch (/*@only@*/ guardSet p_guards) 258 /*@modifies internalState@*/ ; 259 extern void usymtab_altBranch (/*@only@*/ guardSet p_guards) 260 /*@modifies internalState@*/ ; 261 262 extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl) 263 /*@modifies internalState@*/ ; 264 265 extern void 266 usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl) 267 /*@modifies internalState@*/ ; 268 269 extern void 270 usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch, 271 bool p_isOpt, clause p_cl) 272 /*@modifies internalState@*/ ; 273 274 extern void usymtab_unguard (sRef p_s) /*@modifies internalState@*/ ; 275 extern bool usymtab_isGuarded (sRef p_s) /*@globals internalState@*/ ; 276 extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_warningstream@*/ ; 277 extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ; 278 extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ; 279 280 extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ; 281 282 extern bool usymtab_isBoolType (typeId p_uid) /*@globals internalState@*/ ; 283 extern /*@only@*/ cstring usymtab_getTypeEntryName (typeId p_uid) 284 /*@globals internalState@*/ ; 285 extern /*@exposed@*/ uentry usymtab_getTypeEntry (typeId p_uid) 286 /*@globals internalState@*/ ; 287 288 extern typeId 289 usymtab_supAbstractTypeEntry (/*@only@*/ uentry p_e, bool p_dodef) 290 /*@modifies internalState, p_e@*/ ; 291 extern ctype usymtab_supForwardTypeEntry (/*@only@*/ uentry p_e) 292 /*@modifies internalState, p_e@*/ ; 293 294 extern /*@exposed@*/ uentry 295 usymtab_supGlobalEntryReturn (/*@only@*/ uentry p_e) 296 /*@modifies internalState, p_e@*/ ; 297 298 extern /*@exposed@*/ uentry 299 usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e) 300 /*@modifies internalState, p_e@*/ ; 301 302 extern usymId usymtab_directParamNo (uentry p_ue) 303 /*@globals internalState@*/ ; 304 305 extern bool usymtab_newCase (exprNode p_pred, exprNode p_last) 306 /*@modifies internalState@*/ ; 307 308 extern void usymtab_switchBranch (exprNode p_s) 309 /*@modifies internalState@*/ ; 310 311 extern /*@only@*/ cstring usymtab_unparseStack (void) 312 /*@globals internalState@*/ ; 313 extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths) 314 /*@modifies internalState@*/ ; 315 316 extern /*@observer@*/ uentry usymtab_lookupGlobSafe (cstring p_k) 317 /*@globals internalState@*/ ; 318 319 extern /*@only@*/ sRefSet usymtab_aliasedBy (sRef p_s) 320 /*@globals internalState@*/ ; 321 322 extern /*@only@*/ sRefSet usymtab_canAlias (sRef p_s) 323 /*@globals internalState@*/ ; 324 325 extern void usymtab_clearAlias (sRef p_s) 326 /*@modifies internalState, p_s@*/ ; 327 328 extern void usymtab_addMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al) 329 /*@modifies internalState@*/ ; 330 331 extern void usymtab_addForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al) 332 /*@modifies internalState@*/ ; 333 334 extern /*@only@*/ cstring usymtab_unparseAliases (void) 335 /*@globals internalState@*/ ; 336 337 extern /*@exposed@*/ uentry 338 usymtab_supReturnFileEntry (/*@only@*/ uentry p_e) 339 /*@modifies internalState@*/ ; 340 341 extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s) 342 /*@globals internalState@*/ ; 343 344 extern bool usymtab_existsReal (cstring p_k) 345 /*@globals internalState@*/ ; 346 347 extern /*@only@*/ sRefSet usymtab_allAliases (sRef p_s) 348 /*@globals internalState@*/ ; 349 350 extern void usymtab_exportLocal (void) 351 /*@modifies internalState@*/ ; 352 353 extern void usymtab_popCaseBranch (void) 354 /*@modifies internalState@*/ ; 355 356 /* special scopes */ 357 358 /*@constant int globScope;@*/ 359 # define globScope 0 /* global variables */ 360 361 /*@constant int fileScope;@*/ 362 # define fileScope 1 /* file-level static variables */ 363 364 /*@constant int paramsScope;@*/ 365 # define paramsScope 2 /* function parameters */ 366 367 /*@constant int functionScope;@*/ 368 # define functionScope 3 369 370 extern /*@falsewhennull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ; 371 372 /*@constant null usymtab usymtab_undefined; @*/ 373 # define usymtab_undefined ((usymtab)NULL) 374 # define usymtab_isDefined(u) ((u) != usymtab_undefined) 375 376 extern void usymtab_checkDistinctName (uentry p_e, int p_scope) 377 /*@globals internalState@*/ 378 /*@modifies *g_warningstream, p_e@*/ ; 379 380 extern /*@exposed@*/ sRef usymtab_lookupGlobalMarker (void) /*@globals internalState@*/ ; 381 extern void usymtab_addReallyForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al) /*@modifies internalState@*/ ; 382 extern int usymtab_getCurrentDepth (void) /*@globals internalState@*/ ; 383 384 # ifdef DEBUGSPLINT 385 extern void usymtab_checkAllValid (void) /*@modifies g_errorstream@*/ ; 386 # endif 387 388 # else 389 # error "Multiple include" 390 # endif 391 392 393 394