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