2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
3 ** See ../LICENSE for license information.
6 # ifndef exprNodeList_H
7 # define exprNodeList_H
9 typedef /*@only@*/ exprNode o_exprNode;
16 /*@reldef@*/ /*@relnull@*/ o_exprNode *elements
17 /*:invariant maxUse(elements) = nspace /\ maxDefined(elements) = nelements@*/;
20 /*@iter exprNodeList_elements (sef exprNodeList s, yield exposed exprNode el); @*/
21 # define exprNodeList_elements(x, m_el) \
22 { int m_ind; exprNode *m_elements = &((x)->elements[0]); \
23 for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
24 { exprNode m_el = *(m_elements++);
26 # define end_exprNodeList_elements }}
28 extern int exprNodeList_size (exprNodeList p_s) /*@*/ ;
29 # define exprNodeList_size(s) ((s)->nelements)
31 extern bool exprNodeList_isEmpty (exprNodeList p_s) /*@*/ ;
32 # define exprNodeList_isEmpty(s) (exprNodeList_size(s) == 0)
34 extern /*@only@*/ exprNodeList exprNodeList_new(void);
35 extern /*@exposed@*/ exprNode exprNodeList_nth (exprNodeList p_args, int p_n) /*@*/ ;
36 extern exprNodeList exprNodeList_push (/*@returned@*/ exprNodeList p_args,
37 /*@only@*/ exprNode p_e) ;
38 extern /*@only@*/ exprNodeList exprNodeList_singleton (/*@only@*/ exprNode p_e) ;
40 extern void exprNodeList_addh (exprNodeList p_s, /*@only@*/ exprNode p_el) ;
42 extern void exprNodeList_reset (exprNodeList p_s) ;
43 extern void exprNodeList_advance (exprNodeList p_s) ; /* was "list_pointToNext" */
45 extern /*@only@*/ cstring exprNodeList_unparse (exprNodeList p_s) /*@*/ ;
46 extern void exprNodeList_free (/*@only@*/ exprNodeList p_s) ;
47 extern void exprNodeList_freeShallow (/*@only@*/ exprNodeList p_s);
49 extern /*@observer@*/ exprNode exprNodeList_head (exprNodeList p_s) ;
50 extern /*@observer@*/ exprNode exprNodeList_current (exprNodeList p_s) /*@*/ ;
52 extern /*@exposed@*/ exprNode exprNodeList_getN (exprNodeList p_s, int p_n) /*@*/ ;
54 /*@constant int exprNodeListBASESIZE;@*/
55 # define exprNodeListBASESIZE SMALLBASESIZE