src/Headers/metaStateConstraintList.h

   1 /*
   2 ** metaStateConstraintList.h (from slist_templace.h)
   3 */
   4
   5 # ifndef metaStateConstraintLIST_H
   6 # define metaStateConstraintLIST_H
   7
   8 typedef /*@observer@*/ metaStateConstraint b_metaStateConstraint;
   9
  10 struct s_metaStateConstraintList
  11 {
  12   int nelements;
  13   int free;
  14   /*@reldef@*/ /*@relnull@*/ b_metaStateConstraint *elements;
  15 } ;
  16
  17 extern /*@unused@*/ /*@nullwhentrue@*/ bool
  18   metaStateConstraintList_isUndefined (metaStateConstraintList p_f) /*@*/ ;
  19 extern /*@falsewhennull@*/ bool metaStateConstraintList_isDefined (metaStateConstraintList p_f) /*@*/ ;
  20
  21 /*@constant null metaStateConstraintList metaStateConstraintList_undefined; @*/
  22 # define metaStateConstraintList_undefined (NULL)
  23 # define metaStateConstraintList_isDefined(f)   ((f) != metaStateConstraintList_undefined)
  24 # define metaStateConstraintList_isUndefined(f) ((f) == metaStateConstraintList_undefined)
  25
  26 /*@iter metaStateConstraintList_elements (sef metaStateConstraintList x, yield exposed metaStateConstraint el); @*/
  27 # define metaStateConstraintList_elements(x, m_el) \
  28    { if (metaStateConstraintList_isDefined (x)) { \
  29       int m_ind; metaStateConstraint *m_elements = &((x)->elements[0]); \
  30       for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
  31          { metaStateConstraint m_el = *(m_elements++);
  32
  33 # define end_metaStateConstraintList_elements }}}
  34
  35 extern int metaStateConstraintList_size (/*@sef@*/ metaStateConstraintList p_s) /*@*/ ;
  36 # define metaStateConstraintList_size(s)    (metaStateConstraintList_isDefined (s) ? (s)->nelements : 0)
  37
  38 extern bool metaStateConstraintList_isEmpty (/*@sef@*/ metaStateConstraintList p_s);
  39 # define metaStateConstraintList_isEmpty(s) (metaStateConstraintList_size(s) == 0)
  40
  41 extern metaStateConstraintList
  42   metaStateConstraintList_append (/*@returned@*/ metaStateConstraintList p_s, /*@only@*/ metaStateConstraintList p_t);
  43
  44 extern /*@observer@*/ metaStateConstraint metaStateConstraintList_getFirst (metaStateConstraintList p_s) /*@*/ ;
  45
  46 extern /*@only@*/ metaStateConstraintList metaStateConstraintList_new (void) /*@*/ ;
  47
  48 extern metaStateConstraintList
  49 metaStateConstraintList_add (/*@returned@*/ metaStateConstraintList p_s, /*@observer@*/ metaStateConstraint p_el)
  50      /*@modifies p_s@*/ ;
  51
  52 extern metaStateConstraintList
  53 metaStateConstraintList_single (/*@observer@*/ metaStateConstraint p_el) /*@*/ ;
  54
  55 extern /*@unused@*/ /*@only@*/ cstring metaStateConstraintList_unparse (metaStateConstraintList p_s) ;
  56 extern void metaStateConstraintList_free (/*@only@*/ metaStateConstraintList p_s) ;
  57
  58 /*@constant int metaStateConstraintListBASESIZE;@*/
  59 # define metaStateConstraintListBASESIZE MIDBASESIZE
  60
  61 # endif
  62
  63
  64
  65