src/Headers/usymtab-branch.h

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