src/Headers/sRefSet.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
   3 ** See ../LICENSE for license information.
   4 **
   5 */
   6 /*
   7 ** sRefSet.h
   8 **
   9 ** based on set_template.h
  10 */
  11
  12 # ifndef sRefSET_H
  13 # define sRefSET_H
  14
  15 typedef /*@exposed@*/ sRef ex_sRef;
  16
  17 struct s_sRefSet
  18 {
  19   int entries;
  20   int nspace;
  21   /*@reldef@*/ /*@relnull@*/ ex_sRef *elements;
  22 } ;
  23
  24 /* in forwardTypes: typedef _sRefSet *sRefSet; */
  25
  26 /*
  27 ** realElements --- only non-objects
  28 */
  29
  30 /*@iter sRefSet_realElements (sef sRefSet s, yield exposed sRef el)@*/
  31 # define sRefSet_realElements(x, m_el) \
  32    { int m_ind; if (sRefSet_isDefined (x)) \
  33      { for (m_ind = 0 ; m_ind < (x)->entries; m_ind++) \
  34        { sRef m_el = (x)->elements[m_ind]; if (!(sRef_isExternal(m_el))) {
  35 # define end_sRefSet_realElements }}}}
  36
  37 /*@iter sRefSet_elements (sef sRefSet s, yield exposed sRef el)@*/
  38 # define sRefSet_elements(s,m_el) sRefSet_allElements (s, m_el)
  39 # define end_sRefSet_elements   end_sRefSet_allElements
  40
  41 /*@iter sRefSet_allElements (sef sRefSet s, yield exposed sRef el)@*/
  42 # define sRefSet_allElements(x, m_el) \
  43    { int m_ind; if (sRefSet_isDefined (x)) { \
  44      for (m_ind = 0 ; m_ind < (x)->entries; m_ind++) \
  45        { sRef m_el = (x)->elements[m_ind];
  46
  47 # define end_sRefSet_allElements }}}
  48
  49 /*@constant null sRefSet sRefSet_undefined;@*/
  50 # define sRefSet_undefined ((sRefSet) 0)
  51
  52 extern /*@nullwhentrue@*/ bool sRefSet_isUndefined (sRefSet p_s) /*@*/ ;
  53 extern /*@nullwhentrue@*/ bool sRefSet_isEmpty (/*@sef@*/ sRefSet p_s) /*@*/ ;
  54 extern /*@falsewhennull@*/ bool sRefSet_isDefined (sRefSet p_s) /*@*/ ;
  55
  56 # define sRefSet_isUndefined(s) ((s) == sRefSet_undefined)
  57 # define sRefSet_isDefined(s)   ((s) != sRefSet_undefined)
  58
  59 # define sRefSet_isEmpty(s) \
  60   ((s) == sRefSet_undefined || ((s)->entries == 0))
  61
  62 extern bool sRefSet_equal (sRefSet p_s1, sRefSet p_s2) /*@*/ ;
  63 extern bool sRefSet_hasRealElement (sRefSet p_s) /*@*/ ;
  64 extern bool sRefSet_hasUnconstrained (sRefSet p_s) /*@*/ ;
  65 extern cstring sRefSet_unparsePlain (sRefSet p_s) /*@*/ ;
  66 extern cstring sRefSet_unparseUnconstrained (sRefSet p_s) /*@*/ ;
  67 extern cstring sRefSet_unparseUnconstrainedPlain (sRefSet p_s) /*@*/ ;
  68 extern void sRefSet_fixSrefs (sRefSet p_s);
  69 extern bool sRefSet_delete (sRefSet p_s, sRef p_el);
  70 extern /*@exposed@*/ sRef sRefSet_lookupMember (sRefSet p_s, sRef p_el);
  71 extern bool sRefSet_isSameMember (sRefSet p_s, sRef p_el) /*@*/ ;
  72 extern bool sRefSet_isSameNameMember (sRefSet p_s, sRef p_el) /*@*/ ;
  73 extern /*@only@*/ sRefSet sRefSet_newCopy (/*@exposed@*/ /*@temp@*/ sRefSet p_s);
  74 extern /*@only@*/ sRefSet sRefSet_newDeepCopy (sRefSet p_s);
  75 extern int sRefSet_size(sRefSet p_s) /*@*/ ;
  76 extern sRefSet sRefSet_unionFree (/*@returned@*/ sRefSet p_s1, /*@only@*/ sRefSet p_s2);
  77 extern /*@only@*/ sRefSet sRefSet_new (void) /*@*/ ;
  78 extern /*@only@*/ sRefSet sRefSet_single (/*@exposed@*/ sRef);
  79 extern sRefSet sRefSet_insert (/*@returned@*/ sRefSet p_s, /*@exposed@*/ sRef p_el);
  80 extern bool sRefSet_member (sRefSet p_s, sRef p_el) /*@*/ ;
  81 #ifdef DEADCODE
  82 extern bool sRefSet_containsSameObject (sRefSet p_s, sRef p_el) /*@*/ ;
  83 #endif
  84 extern /*@only@*/ cstring sRefSet_unparse (sRefSet p_s) /*@*/ ;
  85 extern void sRefSet_free (/*@only@*/ sRefSet p_s) /*@modifies p_s@*/;
  86 extern void sRefSet_clear (sRefSet p_s) /*@modifies p_s@*/;
  87 extern /*@only@*/ sRefSet sRefSet_addIndirection (sRefSet p_s) /*@*/ ;
  88 extern /*@only@*/ sRefSet sRefSet_removeIndirection (sRefSet p_s) /*@*/ ;
  89 extern sRefSet
  90   sRefSet_union (/*@returned@*/ sRefSet p_s1, /*@exposed@*/ sRefSet p_s2)
  91   /*@modifies p_s1@*/ ;
  92 extern void sRefSet_levelPrune (sRefSet p_s, int p_lexlevel)
  93   /*@modifies p_s@*/ ;
  94 extern void sRefSet_clearStatics (sRefSet p_s)
  95   /*@modifies p_s@*/ ;
  96 extern sRefSet sRefSet_levelUnion (/*@returned@*/ sRefSet p_sr, sRefSet p_s, int p_lexlevel);
  97 extern /*@only@*/ sRefSet sRefSet_intersect (sRefSet p_s1, sRefSet p_s2);
  98 extern /*@only@*/ sRefSet sRefSet_fetchKnown (sRefSet p_s, int p_i);
  99 extern /*@only@*/ sRefSet sRefSet_fetchUnknown (sRefSet p_s);
 100 extern /*@only@*/ sRefSet sRefSet_accessField (sRefSet p_s, /*@observer@*/ cstring p_f);
 101 extern /*@only@*/ sRefSet sRefSet_realNewUnion (sRefSet p_s1, sRefSet p_s2);
 102 extern /*@only@*/ cstring sRefSet_unparseDebug (sRefSet p_s) /*@*/ ;
 103 extern /*@unused@*/ cstring sRefSet_unparseFull (sRefSet p_s) /*@*/ ;
 104 extern bool sRefSet_modifyMember (sRefSet p_s, sRef p_m) /*@modifies p_m@*/ ;
 105 extern /*@only@*/ sRefSet sRefSet_undump (char **p_s) /*@modifies *p_s@*/ ;
 106 extern /*@only@*/ cstring sRefSet_dump (sRefSet p_sl) /*@*/ ;
 107 extern bool sRefSet_deleteBase (sRefSet p_s, sRef p_base) /*@modifies p_s@*/ ;
 108 extern /*@exposed@*/ sRef sRefSet_choose (sRefSet p_s) /*@*/ ;
 109 extern /*@exposed@*/ sRef sRefSet_mergeIntoOne (sRefSet p_s) /*@*/ ;
 110 extern /*@only@*/ sRefSet
 111   sRefSet_levelCopy (/*@exposed@*/ sRefSet p_s, int p_lexlevel) /*@*/ ;
 112 extern sRefSet
 113   sRefSet_unionExcept (/*@returned@*/ sRefSet p_s1, sRefSet p_s2, sRef p_ex)
 114      /*@modifies p_s1@*/ ;
 115
 116 sRefSet sRefSet_copyInto (/*@returned@*/ sRefSet p_s1, /*@exposed@*/ sRefSet p_s2)
 117      /*@modifies p_s1@*/ ;
 118
 119 extern bool sRefSet_hasStatic (sRefSet p_s) /*@*/ ;
 120
 121 extern void sRefSet_markImmutable (sRefSet p_s) /*@modifies p_s@*/ ;
 122
 123 # else
 124 # error "Multiple include"
 125 # endif
 126