]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
28bf4b0b | 2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001. |
885824d3 | 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 | ||
28bf4b0b | 15 | typedef /*@exposed@*/ sRef ex_sRef; |
16 | ||
17 | struct s_sRefSet | |
885824d3 | 18 | { |
19 | int entries; | |
20 | int nspace; | |
28bf4b0b | 21 | /*@reldef@*/ /*@relnull@*/ ex_sRef *elements; |
885824d3 | 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 /*@truenull@*/ bool sRefSet_isUndefined (sRefSet p_s) /*@*/ ; | |
56 | extern /*@truenull@*/ bool sRefSet_isEmpty (/*@sef@*/ sRefSet p_s) /*@*/ ; | |
57 | extern /*@falsenull@*/ 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) /*@*/ ; | |
885824d3 | 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) /*@*/ ; | |
28bf4b0b | 84 | extern bool sRefSet_containsSameObject (sRefSet p_s, sRef p_el) /*@*/ ; |
885824d3 | 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 | |
28bf4b0b | 91 | sRefSet_union (/*@returned@*/ sRefSet p_s1, /*@exposed@*/ sRefSet p_s2) |
885824d3 | 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) /*@*/ ; | |
885824d3 | 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) /*@*/ ; | |
28bf4b0b | 111 | extern /*@exposed@*/ sRef sRefSet_mergeIntoOne (sRefSet p_s) /*@*/ ; |
885824d3 | 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 | ||
28bf4b0b | 118 | sRefSet sRefSet_copyInto (/*@returned@*/ sRefSet p_s1, /*@exposed@*/ sRefSet p_s2) |
119 | /*@modifies p_s1@*/ ; | |
120 | ||
885824d3 | 121 | extern bool sRefSet_hasStatic (sRefSet p_s) /*@*/ ; |
122 | ||
28bf4b0b | 123 | extern void sRefSet_markImmutable (sRefSet p_s) /*@modifies p_s@*/ ; |
124 | ||
885824d3 | 125 | # else |
126 | # error "Multiple include" | |
127 | # endif | |
128 | ||
129 | ||
130 |