| 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 | |
| 0e41eb0e |
17 | extern /*@unused@*/ /*@nullwhentrue@*/ bool |
| ccf0a4a8 |
18 | metaStateConstraintList_isUndefined (metaStateConstraintList p_f) /*@*/ ; |
| 0e41eb0e |
19 | extern /*@falsewhennull@*/ bool metaStateConstraintList_isDefined (metaStateConstraintList p_f) /*@*/ ; |
| ccf0a4a8 |
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 | |
andersk / splint.git / blame