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 extern ctype usymtab_lookupType (cstring p_k)
 128    /*@globals internalState@*/ ;
 129
 130 extern bool usymtab_isDefinitelyNull (sRef p_s)
 131    /*@globals internalState@*/ ;
 132 extern bool usymtab_isDefinitelyNullDeep (sRef p_s)
 133    /*@globals internalState@*/ ;
 134
 135 extern usymId usymtab_supExposedTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
 136    /*@modifies internalState, p_e@*/ ;
 137
 138 extern ctype usymtab_supTypeEntry (/*@only@*/ uentry p_e)
 139    /*@modifies internalState, p_e@*/ ;
 140
 141 extern /*@exposed@*/ uentry usymtab_supReturnTypeEntry (/*@only@*/ uentry p_e)
 142    /*@modifies internalState@*/ ;
 143
 144 extern /*@observer@*/ uentry usymtab_lookupSafe (cstring p_k)
 145    /*@globals internalState@*/ ;
 146
 147 extern /*@observer@*/ uentry usymtab_getGlobalEntry (usymId p_uid)
 148   /*@globals internalState@*/ ;
 149
 150 extern bool usymtab_exists (cstring p_k)
 151    /*@globals internalState@*/ ;
 152
 153 extern bool usymtab_existsVar (cstring p_k)
 154    /*@globals internalState@*/ ;
 155
 156 extern bool usymtab_existsGlob (cstring p_k)
 157    /*@globals internalState@*/ ;
 158
 159 extern bool usymtab_existsType (cstring p_k)
 160    /*@globals internalState@*/ ;
 161
 162 extern bool usymtab_existsEither (cstring p_k)
 163    /*@globals internalState@*/ ;
 164
 165 extern bool usymtab_existsTypeEither (cstring p_k)
 166    /*@globals internalState@*/ ;
 167
 168 extern usymId usymtab_getId (cstring p_k) /*@globals internalState@*/ ;
 169 extern usymId usymtab_getTypeId (cstring p_k) /*@globals internalState@*/ ;
 170
 171 extern void usymtab_supEntry (/*@only@*/ uentry p_e)
 172   /*@modifies internalState, p_e@*/ ;
 173
 174 extern void usymtab_replaceEntry (/*@only@*/ uentry p_s)
 175   /*@modifies internalState, p_s@*/ ;
 176
 177 extern void usymtab_supEntrySref (/*@only@*/ uentry p_e)
 178   /*@modifies internalState, p_e@*/ ;
 179
 180 extern void usymtab_supGlobalEntry (/*@only@*/ uentry p_e)
 181   /*@modifies internalState@*/ ;
 182
 183 extern void usymtab_addGlobalEntry (/*@only@*/ uentry p_e)
 184   /*@modifies internalState, p_e@*/ ;
 185
 186 extern /*@exposed@*/ uentry
 187   usymtab_supEntryReturn (/*@only@*/ uentry p_e)
 188   /*@modifies internalState, p_e@*/ ;
 189
 190 extern usymId usymtab_addEntry (/*@only@*/ uentry p_e)
 191   /*@modifies internalState, p_e@*/ ;
 192
 193 extern ctype usymtab_lookupAbstractType (cstring p_k)
 194      /*@globals internalState@*/ /*@modifies nothing@*/ ;
 195
 196 extern bool usymtab_matchForwardStruct (usymId p_u1, usymId p_u2)
 197      /*@globals internalState@*/ ;
 198
 199 extern bool usymtab_existsEnumTag (cstring p_k)
 200   /*@globals internalState@*/ ;
 201 extern bool usymtab_existsUnionTag (cstring p_k)
 202   /*@globals internalState@*/ ;
 203 extern bool usymtab_existsStructTag (cstring p_k)
 204   /*@globals internalState@*/ ;
 205
 206 extern usymId usymId_fromInt (int p_i) /*@*/ ;
 207 # define usymId_fromInt(i)   ((usymId)(i))
 208
 209 extern bool usymId_isInvalid (usymId p_u) /*@*/ ;
 210 # define usymId_isInvalid(u) ((u) == USYMIDINVALID)
 211
 212 extern bool usymId_isValid (usymId p_u) /*@*/ ;
 213 # define usymId_isValid(u)   ((u) != USYMIDINVALID)
 214
 215 extern bool typeId_isInvalid (typeId p_u) /*@*/ ;
 216 # define typeId_isInvalid(u) ((u) == typeId_invalid)
 217
 218 extern bool typeId_isValid (typeId p_u) /*@*/ ;
 219 # define typeId_isValid(u)   ((u) != typeId_invalid)
 220
 221 extern bool typeId_equal (typeId p_u1, typeId p_u2) /*@*/ ;
 222 # define typeId_equal(u1,u2) ((u1) == (u2))
 223
 224 extern typeId typeId_fromInt (int p_i);
 225 # define typeId_fromInt(i)   ((typeId)(i))
 226
 227 /*@iter usymtab_entries (sef usymtab u, yield exposed uentry el); @*/
 228 # define usymtab_entries(x, m_i)   \
 229     { int m_ind; \
 230       if (usymtab_isDefined (x)) \
 231         for (m_ind = 0; m_ind < (x)->nentries; m_ind++) \
 232            { uentry m_i = (x)->entries[m_ind];
 233
 234 # define end_usymtab_entries }}
 235
 236 extern /*@unused@*/ void usymtab_displayAllUses (void)
 237    /*@globals internalState@*/
 238    /*@modifies *g_warningstream@*/ ;
 239
 240 extern /*@unused@*/ void usymtab_printOut (void)
 241    /*@globals internalState@*/
 242    /*@modifies *g_warningstream@*/ ;
 243
 244 extern /*@unused@*/ void usymtab_printAll (void)
 245    /*@globals internalState@*/
 246    /*@modifies *g_warningstream@*/ ;
 247
 248 extern void usymtab_enterScope (void)
 249   /*@modifies internalState;@*/ ;
 250 extern void usymtab_enterFunctionScope (uentry p_fcn)
 251   /*@modifies internalState;@*/ ;
 252 extern void usymtab_quietExitScope (fileloc p_loc)
 253   /*@modifies internalState;@*/ ;
 254 extern void usymtab_exitScope (exprNode p_expr) /*@modifies internalState@*/ ;
 255 extern void usymtab_addGuards (guardSet p_guards) /*@modifies internalState@*/ ;
 256 extern void usymtab_setExitCode (exitkind p_ex) /*@modifies internalState@*/ ;
 257 extern void usymtab_exitFile (void) /*@modifies internalState@*/ ;
 258 extern void usymtab_enterFile (void) /*@modifies internalState@*/ ;
 259
 260 extern /*@observer@*/ uentry usymtab_lookupEnumTag (cstring p_k)
 261   /*@globals internalState@*/ ;
 262
 263 extern usymId usymtab_convertId (usymId p_uid) /*@globals internalState@*/ ;
 264 extern void usymtab_initMod (void) /*@modifies internalState@*/ ;
 265 extern void usymtab_initBool (void) /*@modifies internalState@*/ ;
 266 extern void usymtab_initGlobalMarker (void) /*@modifies internalState@*/ ;
 267
 268 extern void usymtab_exportHeader (void)
 269    /*@modifies internalState@*/ ;
 270
 271 extern ctype usymtab_structFieldsType (uentryList p_f)
 272    /*@globals internalState@*/ ;
 273
 274 extern ctype usymtab_unionFieldsType (uentryList p_f)
 275    /*@globals internalState@*/ ;
 276
 277 extern ctype usymtab_enumEnumNameListType (enumNameList p_f)
 278    /*@globals internalState@*/ ;
 279
 280 extern /*@exposed@*/ uentry usymtab_getTypeEntrySafe (usymId p_uid)
 281    /*@globals internalState@*/ ;
 282
 283 extern void usymtab_popOrBranch (exprNode p_pred, exprNode p_expr)
 284   /*@modifies internalState@*/ ;
 285 extern void usymtab_popAndBranch (exprNode p_pred, exprNode p_expr)
 286   /*@modifies internalState@*/ ;
 287
 288 extern void usymtab_trueBranch (/*@only@*/ guardSet p_guards)
 289   /*@modifies internalState@*/ ;
 290 extern void usymtab_altBranch (/*@only@*/ guardSet p_guards)
 291   /*@modifies internalState@*/ ;
 292
 293 extern void usymtab_popTrueBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
 294   /*@modifies internalState@*/ ;
 295
 296 extern void
 297   usymtab_popTrueExecBranch (exprNode p_pred, exprNode p_expr, clause p_cl)
 298   /*@modifies internalState@*/ ;
 299
 300 extern void
 301   usymtab_popBranches (exprNode p_pred, exprNode p_tbranch, exprNode p_fbranch,
 302                        bool p_isOpt, clause p_cl)
 303    /*@modifies internalState@*/ ;
 304
 305 extern void usymtab_unguard (sRef p_s) /*@modifies internalState@*/ ;
 306 extern bool usymtab_isGuarded (sRef p_s) /*@globals internalState@*/ ;
 307 extern void usymtab_printGuards (void) /*@globals internalState@*/ /*@modifies *g_warningstream@*/ ;
 308 extern void usymtab_quietPlainExitScope (void) /*@modifies internalState@*/ ;
 309 extern void usymtab_printComplete (void) /*@globals internalState@*/ /*@modifies *stdout@*/ ;
 310
 311 extern bool usymtab_existsGlobEither (cstring p_k) /*@globals internalState@*/ ;
 312
 313 extern bool usymtab_isBoolType (usymId p_uid) /*@globals internalState@*/ ;
 314 extern /*@only@*/ cstring
 315   usymtab_getTypeEntryName (usymId p_uid)
 316   /*@globals internalState@*/ ;
 317 extern /*@exposed@*/ uentry usymtab_getTypeEntry (usymId p_uid)
 318   /*@globals internalState@*/ ;
 319
 320 extern usymId
 321   usymtab_supAbstractTypeEntry (/*@only@*/ uentry p_e, bool p_dodef)
 322   /*@modifies internalState, p_e@*/ ;
 323 extern ctype usymtab_supForwardTypeEntry (/*@only@*/ uentry p_e)
 324   /*@modifies internalState, p_e@*/ ;
 325
 326 extern /*@exposed@*/ uentry
 327   usymtab_supGlobalEntryReturn (/*@only@*/ uentry p_e)
 328   /*@modifies internalState, p_e@*/ ;
 329
 330 extern /*@exposed@*/ uentry
 331   usymtab_supEntrySrefReturn (/*@only@*/ uentry p_e)
 332   /*@modifies internalState, p_e@*/ ;
 333
 334 extern int uentry_directParamNo (uentry p_ue)
 335   /*@globals internalState@*/ ;
 336
 337 extern bool usymtab_newCase (exprNode p_pred, exprNode p_last)
 338   /*@modifies internalState@*/ ;
 339
 340 extern void usymtab_switchBranch (exprNode p_s)
 341   /*@modifies internalState@*/ ;
 342
 343 extern /*@only@*/ cstring usymtab_unparseStack (void)
 344   /*@globals internalState@*/ ;
 345 extern void usymtab_exitSwitch (exprNode p_sw, bool p_allpaths)
 346   /*@modifies internalState@*/ ;
 347
 348 extern /*@observer@*/ uentry usymtab_lookupGlobSafe (cstring p_k)
 349   /*@globals internalState@*/ ;
 350
 351 extern /*@only@*/ sRefSet usymtab_aliasedBy (sRef p_s)
 352   /*@globals internalState@*/ ;
 353
 354 extern /*@only@*/ sRefSet usymtab_canAlias (sRef p_s)
 355   /*@globals internalState@*/ ;
 356
 357 extern void usymtab_clearAlias (sRef p_s)
 358   /*@modifies internalState, p_s@*/ ;
 359
 360 extern void usymtab_addMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
 361   /*@modifies internalState@*/ ;
 362
 363 extern void usymtab_addForceMustAlias (/*@exposed@*/ sRef p_s, /*@exposed@*/ sRef p_al)
 364   /*@modifies internalState@*/ ;
 365
 366 extern /*@only@*/ cstring usymtab_unparseAliases (void)
 367   /*@globals internalState@*/ ;
 368
 369 extern /*@exposed@*/ uentry
 370   usymtab_supReturnFileEntry (/*@only@*/ uentry p_e)
 371    /*@modifies internalState@*/ ;
 372
 373 extern bool usymtab_isAltDefinitelyNullDeep (sRef p_s)
 374    /*@globals internalState@*/ ;
 375
 376 extern bool usymtab_existsReal (cstring p_k)
 377    /*@globals internalState@*/ ;
 378
 379 extern /*@only@*/ sRefSet usymtab_allAliases (sRef p_s)
 380    /*@globals internalState@*/ ;
 381
 382 extern void usymtab_exportLocal (void)
 383    /*@modifies internalState@*/ ;
 384
 385 extern void usymtab_popCaseBranch (void)
 386      /*@modifies internalState@*/ ;
 387
 388 /* special scopes */
 389
 390 /*@constant int invalidScope;@*/
 391 # define invalidScope -1  /* invalid scope */
 392
 393 /*@constant int globScope;@*/
 394 # define globScope 0  /* global variables */
 395
 396 /*@constant int fileScope;@*/
 397 # define fileScope   1  /* file-level static variables */
 398
 399 /*@constant int paramsScope;@*/
 400 # define paramsScope 2  /* function parameters */
 401
 402 /*@constant int functionScope;@*/
 403 # define functionScope 3
 404
 405 extern /*@falsewhennull@*/ bool usymtab_isDefined (usymtab p_u) /*@*/ ;
 406
 407 /*@constant null usymtab usymtab_undefined; @*/
 408 # define usymtab_undefined ((usymtab)NULL)
 409 # define usymtab_isDefined(u) ((u) != usymtab_undefined)
 410
 411 extern void usymtab_checkDistinctName (uentry p_e, int p_scope)
 412   /*@globals internalState@*/
 413   /*@modifies *g_warningstream, p_e@*/ ;
 414
 415 extern /*@exposed@*/ sRef usymtab_lookupGlobalMarker (void) /*@globals internalState@*/ ;
 416
 417 extern int usymtab_getCurrentDepth (void) /*@globals internalState@*/ ;
 418
 419 # else
 420 # error "Multiple include"
 421 # endif
 422
 423
 424