]>
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 | ** stateClauseList.h | |
7 | */ | |
8 | ||
9 | # ifndef STATECLAUSELIST_H | |
10 | # define STATECLAUSELIST_H | |
11 | ||
12 | struct s_stateClauseList | |
13 | { | |
14 | int nelements; | |
15 | int nspace; | |
16 | /*@relnull@*/ /*@reldef@*/ o_stateClause *elements; | |
17 | } ; | |
18 | ||
19 | extern void stateClauseList_checkAll (uentry p_ue) | |
20 | /*@modifies p_ue, g_msgstream@*/ ; | |
21 | ||
22 | /*@constant null stateClauseList stateClauseList_undefined@*/ | |
23 | # define stateClauseList_undefined ((stateClauseList) 0) | |
24 | ||
25 | extern /*@falsenull@*/ bool stateClauseList_isDefined (stateClauseList p_s) /*@*/ ; | |
26 | # define stateClauseList_isDefined(s) ((s) != stateClauseList_undefined) | |
27 | ||
28 | extern /*@truenull@*/ bool stateClauseList_isUndefined (stateClauseList p_s) /*@*/ ; | |
29 | # define stateClauseList_isUndefined(s) ((s) == stateClauseList_undefined) | |
30 | ||
31 | extern /*@unused@*/ int | |
32 | stateClauseList_size (/*@sef@*/ stateClauseList p_s) /*@*/ ; | |
33 | # define stateClauseList_size(s) (stateClauseList_isDefined (s) ? (s)->nelements : 0) | |
34 | ||
35 | extern cstring stateClause_unparseKind (stateClause p_s) /*@*/ ; | |
36 | ||
37 | extern stateClauseList | |
38 | stateClauseList_add (/*@returned@*/ stateClauseList p_s, | |
39 | /*@only@*/ stateClause p_el) | |
40 | /*@modifies p_s@*/ ; | |
41 | ||
42 | extern /*@unused@*/ cstring stateClauseList_unparse (stateClauseList p_s) /*@*/ ; | |
43 | extern void stateClauseList_free (/*@only@*/ stateClauseList p_s) ; | |
44 | ||
45 | extern /*@only@*/ stateClauseList stateClauseList_copy (stateClauseList p_s) /*@*/ ; | |
46 | ||
47 | extern cstring stateClauseList_dump (stateClauseList p_s) /*@*/ ; | |
48 | extern stateClauseList stateClauseList_undump (char **p_s) /*@modifies *p_s@*/ ; | |
49 | ||
50 | extern int stateClauseList_compare (stateClauseList p_s1, stateClauseList p_s2) /*@*/ ; | |
51 | ||
52 | /*@constant int stateClauseListBASESIZE;@*/ | |
53 | # define stateClauseListBASESIZE MIDBASESIZE | |
54 | ||
55 | extern void stateClauseList_checkEqual (uentry p_old, uentry p_unew) | |
56 | /*@modifies g_msgstream@*/ ; | |
57 | ||
58 | /*@iter stateClauseList_elements (sef stateClauseList x, yield exposed stateClause el); @*/ | |
59 | # define stateClauseList_elements(x, m_el) \ | |
60 | { if (!stateClauseList_isUndefined(x)) \ | |
61 | { int m_ind; stateClause *m_elements = &((x)->elements[0]); \ | |
62 | for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ | |
63 | { stateClause m_el = *(m_elements++); | |
64 | ||
65 | # define end_stateClauseList_elements }}} | |
66 | ||
67 | /*@iter stateClauseList_preElements (sef stateClauseList x, yield exposed stateClause el); @*/ | |
68 | # define stateClauseList_preElements(x, m_el) \ | |
69 | { if (!stateClauseList_isUndefined(x)) \ | |
70 | { int m_ind; stateClause *m_elements = &((x)->elements[0]); \ | |
71 | for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ | |
72 | { stateClause m_el = *(m_elements++); if (stateClause_isBefore (m_el)) { \ | |
73 | ||
74 | # define end_stateClauseList_preElements }}}} | |
75 | ||
76 | /*@iter stateClauseList_postElements (sef stateClauseList x, yield exposed stateClause el); @*/ | |
77 | # define stateClauseList_postElements(x, m_el) \ | |
78 | { if (!stateClauseList_isUndefined(x)) \ | |
79 | { int m_ind; stateClause *m_elements = &((x)->elements[0]); \ | |
80 | for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ | |
81 | { stateClause m_el = *(m_elements++); if (stateClause_isAfter (m_el)) { \ | |
82 | ||
83 | # define end_stateClauseList_postElements }}}} | |
84 | ||
85 | # else | |
86 | # error "Multiple include" | |
87 | # endif | |
88 | ||
89 |