src/Headers/specialClauses.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
   3 ** See ../LICENSE for license information.
   4 */
   5 /*
   6 ** specialClauses.h
   7 */
   8
   9 # ifndef SPECIALCLAUSES_H
  10 # define SPECIALCLAUSES_H
  11
  12 typedef enum
  13 {
  14   SP_USES,
  15   SP_DEFINES,
  16   SP_ALLOCATES,
  17   SP_RELEASES,
  18   SP_SETS,
  19   SP_ISNULL,
  20   SP_ISNOTNULL,
  21   SP_ISONLY,
  22   SP_ISSHARED,
  23   SP_ISDEPENDENT,
  24   SP_ISOWNED,
  25   SP_ISOBSERVER,
  26   SP_ISEXPOSED
  27 } specialClauseKind ;
  28
  29 typedef enum
  30 {
  31   TK_BEFORE,
  32   TK_AFTER,
  33   TK_BOTH
  34 } stateConstraint;
  35
  36 abst_typedef struct
  37 {
  38   stateConstraint state;
  39   specialClauseKind kind;
  40   sRefSet refs;
  41 } *specialClause ;
  42
  43 typedef /*@only@*/ specialClause o_specialClause;
  44
  45 extern /*@unused@*/ cstring specialClause_unparse (specialClause p_s) /*@*/ ;
  46
  47 extern /*@null@*/ sRefMod
  48   specialClause_getEffectFunction (specialClause p_cl) /*@*/ ;
  49
  50 extern /*@null@*/ sRefMod
  51   specialClause_getReturnEffectFunction (specialClause p_cl) /*@*/ ;
  52
  53 extern /*@null@*/ sRefMod
  54   specialClause_getEntryFunction (specialClause p_cl) /*@*/ ;
  55
  56 extern bool specialClause_isBefore (specialClause p_cl) /*@*/ ;
  57 extern bool specialClause_isAfter (specialClause p_cl) /*@*/ ;
  58
  59 extern /*@observer@*/ sRefSet specialClause_getRefs (specialClause p_cl) /*@*/ ;
  60 # define specialClause_getRefs(cl) ((cl)->refs)
  61
  62 abst_typedef /*@null@*/ struct
  63 {
  64   int nelements;
  65   int nspace;
  66   /*@relnull@*/ /*@reldef@*/ o_specialClause *elements;
  67 } *specialClauses ;
  68
  69 /*@iter specialClauses_elements (sef specialClauses x, yield exposed specialClause el); @*/
  70 # define specialClauses_elements(x, m_el) \
  71    { if (!specialClauses_isUndefined(x)) \
  72        { int m_ind; specialClause *m_elements = &((x)->elements[0]); \
  73           for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
  74            { specialClause m_el = *(m_elements++);
  75
  76 # define end_specialClauses_elements }}}
  77
  78 /*@iter specialClauses_preElements (sef specialClauses x, yield exposed specialClause el); @*/
  79 # define specialClauses_preElements(x, m_el) \
  80    { if (!specialClauses_isUndefined(x)) \
  81        { int m_ind; specialClause *m_elements = &((x)->elements[0]); \
  82           for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
  83            { specialClause m_el = *(m_elements++); if (specialClause_isBefore (m_el)) { \
  84
  85 # define end_specialClauses_preElements }}}}
  86
  87 /*@iter specialClauses_postElements (sef specialClauses x, yield exposed specialClause el); @*/
  88 # define specialClauses_postElements(x, m_el) \
  89    { if (!specialClauses_isUndefined(x)) \
  90        { int m_ind; specialClause *m_elements = &((x)->elements[0]); \
  91           for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
  92            { specialClause m_el = *(m_elements++); if (specialClause_isAfter (m_el)) { \
  93
  94 # define end_specialClauses_postElements }}}}
  95
  96 extern void specialClauses_checkAll (uentry p_ue)
  97    /*@modifies p_ue, g_msgstream@*/ ;
  98
  99 extern flagcode specialClause_preErrorCode (specialClause p_cl) /*@*/ ;
 100 extern /*@observer@*/ cstring
 101   specialClause_preErrorString (specialClause p_cl, sRef p_sr) /*@*/ ;
 102
 103 extern flagcode specialClause_postErrorCode (specialClause p_cl) /*@*/ ;
 104 extern /*@observer@*/ cstring
 105   specialClause_postErrorString (specialClause p_cl, sRef p_sr) /*@*/ ;
 106
 107 extern sRefTest specialClause_getPreTestFunction (specialClause p_cl) /*@*/ ;
 108
 109 extern sRefTest specialClause_getPostTestFunction (specialClause p_cl) /*@*/ ;
 110 extern sRefShower specialClause_getPostTestShower (specialClause p_cl) /*@*/ ;
 111
 112 extern specialClause
 113   specialClause_create (stateConstraint p_st, specialClauseKind p_k, /*@only@*/ sRefSet p_s)
 114   /*@*/ ;
 115
 116 extern specialClause specialClause_createDefines (/*@only@*/ sRefSet p_s) /*@*/ ;
 117 extern specialClause specialClause_createUses (/*@only@*/ sRefSet p_s) /*@*/ ;
 118 extern specialClause specialClause_createAllocates (/*@only@*/ sRefSet p_s) /*@*/ ;
 119 extern specialClause specialClause_createReleases (/*@only@*/ sRefSet p_s) /*@*/ ;
 120 extern specialClause specialClause_createSets (/*@only@*/ sRefSet p_s) /*@*/ ;
 121
 122 /*@constant null specialClauses specialClauses_undefined@*/
 123 # define specialClauses_undefined ((specialClauses) 0)
 124
 125 extern /*@falsenull@*/ bool specialClauses_isDefined (specialClauses p_s) /*@*/ ;
 126 # define specialClauses_isDefined(s) ((s) != specialClauses_undefined)
 127
 128 extern /*@truenull@*/ bool specialClauses_isUndefined (specialClauses p_s) /*@*/ ;
 129 # define specialClauses_isUndefined(s) ((s) == specialClauses_undefined)
 130
 131 extern /*@unused@*/ int
 132   specialClauses_size (/*@sef@*/ specialClauses p_s) /*@*/ ;
 133 # define specialClauses_size(s) (specialClauses_isDefined (s) ? (s)->nelements : 0)
 134
 135 extern cstring specialClause_unparseKind (specialClause p_s) /*@*/ ;
 136
 137 extern specialClauses
 138   specialClauses_add (/*@returned@*/ specialClauses p_s,
 139                       /*@only@*/ specialClause p_el)
 140   /*@modifies p_s@*/ ;
 141
 142 extern /*@unused@*/ cstring specialClauses_unparse (specialClauses p_s) /*@*/ ;
 143 extern void specialClauses_free (/*@only@*/ specialClauses p_s) ;
 144
 145 extern /*@only@*/ specialClauses specialClauses_copy (specialClauses p_s) /*@*/ ;
 146
 147 extern cstring specialClauses_dump (specialClauses p_s) /*@*/ ;
 148 extern specialClauses specialClauses_undump (char **p_s) /*@modifies *p_s@*/ ;
 149
 150 /*@constant int specialClausesBASESIZE;@*/
 151 # define specialClausesBASESIZE MIDBASESIZE
 152
 153 extern void specialClauses_checkEqual (uentry p_old, uentry p_unew)
 154   /*@modifies g_msgstream@*/ ;
 155
 156 # else
 157 # error "Multiple include"
 158 # endif
 159
 160