]>
Commit | Line | Data |
---|---|---|
ccf0a4a8 | 1 | /* |
2 | ** metaStateConstraintList.h (from slist_templace.h) | |
3 | */ | |
4 | ||
5 | # ifndef metaStateConstraintLIST_H | |
6 | # define metaStateConstraintLIST_H | |
7 | ||
8 | typedef /*@observer@*/ metaStateConstraint b_metaStateConstraint; | |
9 | ||
10 | struct s_metaStateConstraintList | |
11 | { | |
12 | int nelements; | |
13 | int free; | |
14 | /*@reldef@*/ /*@relnull@*/ b_metaStateConstraint *elements; | |
15 | } ; | |
16 | ||
17 | extern /*@unused@*/ /*@truenull@*/ bool | |
18 | metaStateConstraintList_isUndefined (metaStateConstraintList p_f) /*@*/ ; | |
19 | extern /*@falsenull@*/ bool metaStateConstraintList_isDefined (metaStateConstraintList p_f) /*@*/ ; | |
20 | ||
21 | /*@constant null metaStateConstraintList metaStateConstraintList_undefined; @*/ | |
22 | # define metaStateConstraintList_undefined (NULL) | |
23 | # define metaStateConstraintList_isDefined(f) ((f) != metaStateConstraintList_undefined) | |
24 | # define metaStateConstraintList_isUndefined(f) ((f) == metaStateConstraintList_undefined) | |
25 | ||
26 | /*@iter metaStateConstraintList_elements (sef metaStateConstraintList x, yield exposed metaStateConstraint el); @*/ | |
27 | # define metaStateConstraintList_elements(x, m_el) \ | |
28 | { if (metaStateConstraintList_isDefined (x)) { \ | |
29 | int m_ind; metaStateConstraint *m_elements = &((x)->elements[0]); \ | |
30 | for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ | |
31 | { metaStateConstraint m_el = *(m_elements++); | |
32 | ||
33 | # define end_metaStateConstraintList_elements }}} | |
34 | ||
35 | extern int metaStateConstraintList_size (/*@sef@*/ metaStateConstraintList p_s) /*@*/ ; | |
36 | # define metaStateConstraintList_size(s) (metaStateConstraintList_isDefined (s) ? (s)->nelements : 0) | |
37 | ||
38 | extern bool metaStateConstraintList_isEmpty (/*@sef@*/ metaStateConstraintList p_s); | |
39 | # define metaStateConstraintList_isEmpty(s) (metaStateConstraintList_size(s) == 0) | |
40 | ||
41 | extern metaStateConstraintList | |
42 | metaStateConstraintList_append (/*@returned@*/ metaStateConstraintList p_s, /*@only@*/ metaStateConstraintList p_t); | |
43 | ||
44 | extern /*@observer@*/ metaStateConstraint metaStateConstraintList_getFirst (metaStateConstraintList p_s) /*@*/ ; | |
45 | ||
46 | extern /*@only@*/ metaStateConstraintList metaStateConstraintList_new (void) /*@*/ ; | |
47 | ||
48 | extern metaStateConstraintList | |
49 | metaStateConstraintList_add (/*@returned@*/ metaStateConstraintList p_s, /*@observer@*/ metaStateConstraint p_el) | |
50 | /*@modifies p_s@*/ ; | |
51 | ||
52 | extern metaStateConstraintList | |
53 | metaStateConstraintList_single (/*@observer@*/ metaStateConstraint p_el) /*@*/ ; | |
54 | ||
55 | extern /*@unused@*/ /*@only@*/ cstring metaStateConstraintList_unparse (metaStateConstraintList p_s) ; | |
56 | extern void metaStateConstraintList_free (/*@only@*/ metaStateConstraintList p_s) ; | |
57 | ||
58 | /*@constant int metaStateConstraintListBASESIZE;@*/ | |
59 | # define metaStateConstraintListBASESIZE MIDBASESIZE | |
60 | ||
61 | # endif | |
62 | ||
63 | ||
64 | ||
65 |