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 int sRefSetBASESIZE;@*/ 50 # define sRefSetBASESIZE SMALLBASESIZE 51 52 /*@constant null sRefSet sRefSet_undefined;@*/ 53 # define sRefSet_undefined ((sRefSet) 0) 54 55 extern /*@nullwhentrue@*/ bool sRefSet_isUndefined (sRefSet p_s) /*@*/ ; 56 extern /*@nullwhentrue@*/ bool sRefSet_isEmpty (/*@sef@*/ sRefSet p_s) /*@*/ ; 57 extern /*@falsewhennull@*/ bool sRefSet_isDefined (sRefSet p_s) /*@*/ ; 58 59 # define sRefSet_isUndefined(s) ((s) == sRefSet_undefined) 60 # define sRefSet_isDefined(s) ((s) != sRefSet_undefined) 61 62 # define sRefSet_isEmpty(s) \ 63 ((s) == sRefSet_undefined || ((s)->entries == 0)) 64 65 extern bool sRefSet_equal (sRefSet p_s1, sRefSet p_s2) /*@*/ ; 66 extern bool sRefSet_hasRealElement (sRefSet p_s) /*@*/ ; 67 extern bool sRefSet_hasUnconstrained (sRefSet p_s) /*@*/ ; 68 extern cstring sRefSet_unparsePlain (sRefSet p_s) /*@*/ ; 69 extern cstring sRefSet_unparseUnconstrained (sRefSet p_s) /*@*/ ; 70 extern cstring sRefSet_unparseUnconstrainedPlain (sRefSet p_s) /*@*/ ; 71 extern void sRefSet_fixSrefs (sRefSet p_s); 72 extern bool sRefSet_delete (sRefSet p_s, sRef p_el); 73 extern /*@exposed@*/ sRef sRefSet_lookupMember (sRefSet p_s, sRef p_el); 74 extern bool sRefSet_isSameMember (sRefSet p_s, sRef p_el) /*@*/ ; 75 extern bool sRefSet_isSameNameMember (sRefSet p_s, sRef p_el) /*@*/ ; 76 extern /*@only@*/ sRefSet sRefSet_newCopy (/*@exposed@*/ /*@temp@*/ sRefSet p_s); 77 extern /*@only@*/ sRefSet sRefSet_newDeepCopy (sRefSet p_s); 78 extern int sRefSet_size(sRefSet p_s) /*@*/ ; 79 extern sRefSet sRefSet_unionFree (/*@returned@*/ sRefSet p_s1, /*@only@*/ sRefSet p_s2); 80 extern /*@only@*/ sRefSet sRefSet_new (void) /*@*/ ; 81 extern /*@only@*/ sRefSet sRefSet_single (/*@exposed@*/ sRef); 82 extern sRefSet sRefSet_insert (/*@returned@*/ sRefSet p_s, /*@exposed@*/ sRef p_el); 83 extern bool sRefSet_member (sRefSet p_s, sRef p_el) /*@*/ ; 84 extern bool sRefSet_containsSameObject (sRefSet p_s, sRef p_el) /*@*/ ; 85 extern /*@only@*/ cstring sRefSet_unparse (sRefSet p_s) /*@*/ ; 86 extern void sRefSet_free (/*@only@*/ sRefSet p_s) /*@modifies p_s@*/; 87 extern void sRefSet_clear (sRefSet p_s) /*@modifies p_s@*/; 88 extern /*@only@*/ sRefSet sRefSet_addIndirection (sRefSet p_s) /*@*/ ; 89 extern /*@only@*/ sRefSet sRefSet_removeIndirection (sRefSet p_s) /*@*/ ; 90 extern sRefSet 91 sRefSet_union (/*@returned@*/ sRefSet p_s1, /*@exposed@*/ sRefSet p_s2) 92 /*@modifies p_s1@*/ ; 93 extern void sRefSet_levelPrune (sRefSet p_s, int p_lexlevel) 94 /*@modifies p_s@*/ ; 95 extern void sRefSet_clearStatics (sRefSet p_s) 96 /*@modifies p_s@*/ ; 97 extern sRefSet sRefSet_levelUnion (/*@returned@*/ sRefSet p_sr, sRefSet p_s, int p_lexlevel); 98 extern /*@only@*/ sRefSet sRefSet_intersect (sRefSet p_s1, sRefSet p_s2); 99 extern /*@only@*/ sRefSet sRefSet_fetchKnown (sRefSet p_s, int p_i); 100 extern /*@only@*/ sRefSet sRefSet_fetchUnknown (sRefSet p_s); 101 extern /*@only@*/ sRefSet sRefSet_accessField (sRefSet p_s, /*@observer@*/ cstring p_f); 102 extern /*@only@*/ sRefSet sRefSet_realNewUnion (sRefSet p_s1, sRefSet p_s2); 103 extern /*@only@*/ cstring sRefSet_unparseDebug (sRefSet p_s) /*@*/ ; 104 extern /*@unused@*/ cstring sRefSet_unparseFull (sRefSet p_s) /*@*/ ; 105 extern int sRefSet_compare (sRefSet p_s1, sRefSet p_s2) /*@*/ ; 106 extern bool sRefSet_modifyMember (sRefSet p_s, sRef p_m) /*@modifies p_m@*/ ; 107 extern /*@only@*/ sRefSet sRefSet_undump (char **p_s) /*@modifies *p_s@*/ ; 108 extern /*@only@*/ cstring sRefSet_dump (sRefSet p_sl) /*@*/ ; 109 extern bool sRefSet_deleteBase (sRefSet p_s, sRef p_base) /*@modifies p_s@*/ ; 110 extern /*@exposed@*/ sRef sRefSet_choose (sRefSet p_s) /*@*/ ; 111 extern /*@exposed@*/ sRef sRefSet_mergeIntoOne (sRefSet p_s) /*@*/ ; 112 extern /*@only@*/ sRefSet 113 sRefSet_levelCopy (/*@exposed@*/ sRefSet p_s, int p_lexlevel) /*@*/ ; 114 extern sRefSet 115 sRefSet_unionExcept (/*@returned@*/ sRefSet p_s1, sRefSet p_s2, sRef p_ex) 116 /*@modifies p_s1@*/ ; 117 118 sRefSet sRefSet_copyInto (/*@returned@*/ sRefSet p_s1, /*@exposed@*/ sRefSet p_s2) 119 /*@modifies p_s1@*/ ; 120 121 extern bool sRefSet_hasStatic (sRefSet p_s) /*@*/ ; 122 123 extern void sRefSet_markImmutable (sRefSet p_s) /*@modifies p_s@*/ ; 124 125 # else 126 # error "Multiple include" 127 # endif 128 129 130 131