1 /* 2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. 3 ** See ../LICENSE for license information. 4 ** 5 */ 6 # ifndef exprNodeSList_H 7 # define exprNodeSList_H 8 9 /* 10 ** like exprNodeList, except elements are dependent. 11 */ 12 13 typedef /*@dependent@*/ exprNode d_exprNode; 14 15 abst_typedef struct 16 { 17 int nelements; 18 int nspace; 19 /*@reldef@*/ /*@relnull@*/ d_exprNode *elements; 20 } *exprNodeSList; 21 22 /*@iter exprNodeSList_elements (sef exprNodeSList x, yield exposed exprNode el); @*/ 23 # define exprNodeSList_elements(x, m_el) \ 24 { int m_ind; exprNode *m_elements = &((x)->elements[0]); \ 25 for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ 26 { exprNode m_el = *(m_elements++); 27 28 # define end_exprNodeSList_elements }} 29 30 extern /*@only@*/ exprNodeSList exprNodeSList_new(void); 31 32 extern /*@only@*/ exprNodeSList exprNodeSList_singleton (/*@exposed@*/ /*@dependent@*/ exprNode p_e) ; 33 34 extern /*@unused@*/ void 35 exprNodeSList_addh (exprNodeSList p_s, /*@exposed@*/ /*@dependent@*/ exprNode p_el); 36 37 extern /*@only@*/ /*@unused@*/ cstring exprNodeSList_unparse (exprNodeSList p_s); 38 extern void exprNodeSList_free (/*@only@*/ exprNodeSList p_s) ; 39 40 extern exprNodeSList 41 exprNodeSList_append (/*@returned@*/ exprNodeSList p_s1, /*@only@*/ exprNodeSList p_s2) ; 42 43 /*@constant int exprNodeSListBASESIZE;@*/ 44 # define exprNodeSListBASESIZE SMALLBASESIZE 45 46 # endif 47 48 49 50 51