]>
Commit | Line | Data |
---|---|---|
d1eb43aa | 1 | /* |
2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000. | |
3 | ** See ../LICENSE for license information. | |
4 | */ | |
5 | ||
6 | # ifndef constraintLIST_H | |
7 | # define constraintLIST_H | |
8 | ||
9 | typedef /*@only@*/ constraint o_constraint; | |
10 | ||
11 | struct _constraintList | |
12 | { | |
13 | int nelements; | |
14 | int nspacehigh; | |
15 | int nspacelow; | |
16 | int current; | |
17 | /*@dependent@*/ /*@reldef@*/ /*@relnull@*/ o_constraint *elements; | |
18 | /*@only@*/ /*@reldef@*/ /*@relnull@*/ o_constraint *elementsroot; | |
19 | } ; | |
20 | ||
21 | /*@iter constraintList_elements (sef constraintList x, yield exposed constraint el); @*/ | |
22 | # define constraintList_elements(x, m_el) \ | |
23 | { int m_ind; constraint *m_elements = &((x)->elements[0]); \ | |
24 | for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ | |
25 | { constraint m_el = *(m_elements++); | |
26 | ||
27 | # define end_constraintList_elements }} | |
28 | ||
29 | extern int constraintList_size (/*@sef@*/ constraintList); | |
30 | # define constraintList_size(s) (constraintList_isDefined (s) ? (s)->nelements : 0) | |
31 | ||
32 | extern bool constraintList_empty (/*@sef@*/ constraintList); | |
33 | # define constraintList_empty(s) (constraintList_size(s) == 0) | |
34 | ||
0e41eb0e | 35 | extern /*@falsewhennull@*/ bool constraintList_isDefined (constraintList p_t); |
d1eb43aa | 36 | # define constraintList_isDefined(s) ((s) != (constraintList) 0) |
37 | ||
6e88de2d | 38 | extern /*@only@*/ constraintList constraintList_makeNew(void); |
d1eb43aa | 39 | extern constraintList constraintList_push (/*@returned@*/ constraintList p_s, |
40 | /*@keep@*/ constraint p_el) ; | |
41 | ||
42 | extern void constraintList_addh (constraintList p_s, /*@keep@*/ constraint p_el) ; | |
43 | extern void constraintList_addl (constraintList p_s, /*@keep@*/ constraint p_el) ; | |
44 | ||
45 | extern void constraintList_reset (constraintList p_s) | |
46 | /*@modifies p_s@*/ ; | |
47 | extern void constraintList_finish (constraintList p_s) | |
48 | /*@modifies p_s@*/ ; | |
49 | extern void constraintList_advance (constraintList p_s) | |
50 | /*@modifies p_s@*/ ; | |
51 | ||
52 | extern /*@exposed@*/ constraint constraintList_getN (constraintList p_s, int p_n) /*@*/ ; | |
53 | ||
b7b694d6 | 54 | # if 0 |
55 | extern /*@only@*/ cstring constraintList_unparse (constraintList p_s) ; | |
56 | extern /*@only@*/ cstring constraintList_unparseTail (constraintList p_s); | |
57 | extern /*@only@*/ cstring constraintList_unparseToCurrent (constraintList p_s); | |
58 | extern /*@only@*/ cstring constraintList_unparseSecondToCurrent (constraintList p_s); | |
59 | # endif | |
d1eb43aa | 60 | |
61 | extern void constraintList_free (/*@only@*/ constraintList p_s) ; | |
62 | ||
63 | extern /*@exposed@*/ constraint constraintList_head (constraintList p_s) ; | |
64 | extern /*@exposed@*/ constraint constraintList_current (constraintList p_s) ; | |
65 | ||
66 | extern /*@only@*/ constraintList constraintList_copy (constraintList p_s) ; | |
67 | ||
68 | /*@constant int constraintListGROWLOW;@*/ | |
69 | # define constraintListGROWLOW 4 /* addl used in abstract.c */ | |
70 | ||
71 | /*@constant int constraintListGROWHI;@*/ | |
72 | # define constraintListGROWHI 4 | |
73 | ||
74 | /*@constant int constraintListBASESIZE;@*/ | |
75 | # define constraintListBASESIZE (constraintListGROWLOW + constraintListGROWHI) | |
76 | ||
77 | # else | |
78 | # error "Multiple include" | |
79 | # endif | |
80 | ||
81 | ||
82 | ||
83 |