src/Headers/exprNodeList.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
   3 ** See ../LICENSE for license information.
   4 **
   5 */
   6 # ifndef exprNodeList_H
   7 # define exprNodeList_H
   8
   9 typedef /*@only@*/ exprNode o_exprNode;
  10
  11 abst_typedef struct
  12 {
  13   int nelements;
  14   int nspace;
  15   int current;
  16   /*@reldef@*/ /*@relnull@*/ o_exprNode *elements
  17   /*:invariant maxUse(elements) = nspace /\ maxDefined(elements) = nelements@*/;
  18 } *exprNodeList;
  19
  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++);
  25
  26 # define end_exprNodeList_elements }}
  27
  28 extern int exprNodeList_size (exprNodeList p_s) /*@*/ ;
  29 # define exprNodeList_size(s) ((s)->nelements)
  30
  31 extern bool exprNodeList_isEmpty (exprNodeList p_s) /*@*/ ;
  32 # define exprNodeList_isEmpty(s) (exprNodeList_size(s) == 0)
  33
  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) ;
  39
  40 extern void exprNodeList_addh (exprNodeList p_s, /*@only@*/ exprNode p_el) ;
  41
  42 extern void exprNodeList_reset (exprNodeList p_s) ;
  43 extern void exprNodeList_advance (exprNodeList p_s) ; /* was "list_pointToNext" */
  44
  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);
  48
  49 extern /*@observer@*/ exprNode exprNodeList_head (exprNodeList p_s) ;
  50 extern /*@observer@*/ exprNode exprNodeList_current (exprNodeList p_s) /*@*/ ;
  51
  52 extern /*@exposed@*/ exprNode exprNodeList_getN (exprNodeList p_s, int p_n) /*@*/ ;
  53
  54 /*@constant int exprNodeListBASESIZE;@*/
  55 # define exprNodeListBASESIZE SMALLBASESIZE
  56
  57 # endif
  58
  59
  60
  61