]>
Commit | Line | Data |
---|---|---|
28bf4b0b | 1 | /* |
2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001. | |
3 | ** See ../LICENSE for license information. | |
4 | */ | |
5 | /* | |
6 | ** sRefList.h (from slist_templace.h) | |
7 | */ | |
8 | ||
9 | # ifndef sRefLIST_H | |
10 | # define sRefLIST_H | |
11 | ||
12 | typedef /*@dependent@*/ sRef d_sRef ; | |
13 | ||
14 | struct s_sRefList | |
15 | { | |
16 | int nelements; | |
17 | int nspace; | |
18 | /*@reldef@*/ /*@relnull@*/ d_sRef *elements; | |
19 | } ; | |
20 | ||
21 | /*@iter sRefList_elements (sef sRefList x, yield exposed sRef el); @*/ | |
22 | # define sRefList_elements(x, m_el) \ | |
23 | { if (!sRefList_isUndefined(x)) \ | |
24 | { int m_ind; sRef *m_elements = &((x)->elements[0]); \ | |
25 | for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ | |
26 | { sRef m_el = *(m_elements++); | |
27 | ||
28 | # define end_sRefList_elements }}} | |
29 | ||
30 | extern int sRefList_size (sRefList p_s) /*@*/ ; | |
31 | ||
32 | extern /*@truenull@*/ bool sRefList_isUndefined (sRefList p_s) /*@*/ ; | |
33 | extern /*@unused@*/ /*@truenull@*/ bool sRefList_isEmpty (sRefList p_s) /*@*/ ; | |
34 | extern /*@unused@*/ /*@falsenull@*/ bool sRefList_isDefined (sRefList p_s) /*@*/ ; | |
35 | ||
36 | # define sRefList_isEmpty(s) (sRefList_size(s) == 0) | |
37 | ||
38 | /*@constant null sRefList sRefList_undefined; @*/ | |
39 | # define sRefList_undefined ((sRefList)0) | |
40 | ||
41 | # define sRefList_isUndefined(c) ((c) == sRefList_undefined) | |
42 | # define sRefList_isDefined(c) ((c) != sRefList_undefined) | |
43 | ||
44 | extern /*@only@*/ sRefList sRefList_new (void); | |
45 | extern /*@only@*/ sRefList sRefList_single (/*@dependent@*/ sRef p_el); | |
46 | ||
47 | extern /*@notnull@*/ sRefList | |
48 | sRefList_add (/*@returned@*/ sRefList p_s, /*@exposed@*/ sRef p_el) /*@modifies p_s@*/ ; | |
49 | ||
50 | extern cstring sRefList_unparse (sRefList p_s) /*@*/ ; | |
51 | extern void sRefList_free (/*@only@*/ sRefList p_s) ; | |
52 | extern /*@only@*/ sRefList sRefList_copy (sRefList p_s) /*@*/ ; | |
53 | ||
54 | /*@constant int sRefListBASESIZE;@*/ | |
55 | # define sRefListBASESIZE MIDBASESIZE | |
56 | ||
57 | # else | |
58 | # error "Multiple include" | |
59 | # endif | |
60 | ||
61 | ||
62 | ||
63 |