src/Headers/sRefList.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
   3 ** See ../LICENSE for license information.
   4 */
   5 /*
   6 ** sRefList.h (from slist_templace.h)
   7 */
   8
   9 # ifndef sRefLIST_H
  10 # define sRefLIST_H
  11
  12 typedef /*@dependent@*/ sRef d_sRef ;
  13
  14 struct s_sRefList
  15 {
  16   int nelements;
  17   int nspace;
  18   /*@reldef@*/ /*@relnull@*/ d_sRef  *elements;
  19 } ;
  20
  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++);
  27
  28 # define end_sRefList_elements }}}
  29
  30 extern int sRefList_size (sRefList p_s) /*@*/ ;
  31
  32 extern /*@nullwhentrue@*/ bool sRefList_isUndefined (sRefList p_s) /*@*/ ;
  33 extern /*@unused@*/ /*@nullwhentrue@*/ bool sRefList_isEmpty (sRefList p_s) /*@*/ ;
  34 extern /*@unused@*/ /*@falsewhennull@*/ bool sRefList_isDefined (sRefList p_s) /*@*/ ;
  35
  36 # define sRefList_isEmpty(s) (sRefList_size(s) == 0)
  37
  38 /*@constant null sRefList sRefList_undefined; @*/
  39 # define sRefList_undefined      ((sRefList)0)
  40
  41 # define sRefList_isUndefined(c) ((c) == sRefList_undefined)
  42 # define sRefList_isDefined(c)   ((c) != sRefList_undefined)
  43
  44 extern /*@only@*/ sRefList sRefList_new (void);
  45 extern /*@only@*/ sRefList sRefList_single (/*@dependent@*/ sRef p_el);
  46
  47 extern /*@notnull@*/ sRefList
  48    sRefList_add (/*@returned@*/ sRefList p_s, /*@exposed@*/ sRef p_el)  /*@modifies p_s@*/ ;
  49
  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) /*@*/ ;
  53
  54 /*@constant int sRefListBASESIZE;@*/
  55 # define sRefListBASESIZE MIDBASESIZE
  56
  57 # else
  58 # error "Multiple include"
  59 # endif
  60
  61
  62
  63