2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
3 ** See ../LICENSE for license information.
6 ** sRefList.h (from slist_templace.h)
12 typedef /*@dependent@*/ sRef d_sRef ;
18 /*@reldef@*/ /*@relnull@*/ d_sRef *elements;
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++);
28 # define end_sRefList_elements }}}
30 extern int sRefList_size (sRefList p_s) /*@*/ ;
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) /*@*/ ;
36 # define sRefList_isEmpty(s) (sRefList_size(s) == 0)
38 /*@constant null sRefList sRefList_undefined; @*/
39 # define sRefList_undefined ((sRefList)0)
41 # define sRefList_isUndefined(c) ((c) == sRefList_undefined)
42 # define sRefList_isDefined(c) ((c) != sRefList_undefined)
44 extern /*@only@*/ sRefList sRefList_new (void);
45 extern /*@only@*/ sRefList sRefList_single (/*@dependent@*/ sRef p_el);
47 extern /*@notnull@*/ sRefList
48 sRefList_add (/*@returned@*/ sRefList p_s, /*@exposed@*/ sRef p_el) /*@modifies p_s@*/ ;
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) /*@*/ ;
54 /*@constant int sRefListBASESIZE;@*/
55 # define sRefListBASESIZE MIDBASESIZE
58 # error "Multiple include"