2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
3 ** See ../LICENSE for license information.
9 # ifndef SPECIALCLAUSES_H
10 # define SPECIALCLAUSES_H
38 stateConstraint state;
39 specialClauseKind kind;
43 typedef /*@only@*/ specialClause o_specialClause;
45 extern /*@unused@*/ cstring specialClause_unparse (specialClause p_s) /*@*/ ;
47 extern /*@null@*/ sRefMod
48 specialClause_getEffectFunction (specialClause p_cl) /*@*/ ;
50 extern /*@null@*/ sRefMod
51 specialClause_getReturnEffectFunction (specialClause p_cl) /*@*/ ;
53 extern /*@null@*/ sRefMod
54 specialClause_getEntryFunction (specialClause p_cl) /*@*/ ;
56 extern bool specialClause_isBefore (specialClause p_cl) /*@*/ ;
57 extern bool specialClause_isAfter (specialClause p_cl) /*@*/ ;
59 extern /*@observer@*/ sRefSet specialClause_getRefs (specialClause p_cl) /*@*/ ;
60 # define specialClause_getRefs(cl) ((cl)->refs)
62 abst_typedef /*@null@*/ struct
66 /*@relnull@*/ /*@reldef@*/ o_specialClause *elements;
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++);
76 # define end_specialClauses_elements }}}
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)) { \
85 # define end_specialClauses_preElements }}}}
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)) { \
94 # define end_specialClauses_postElements }}}}
96 extern void specialClauses_checkAll (uentry p_ue)
97 /*@modifies p_ue, g_msgstream@*/ ;
99 extern flagcode specialClause_preErrorCode (specialClause p_cl) /*@*/ ;
100 extern /*@observer@*/ cstring
101 specialClause_preErrorString (specialClause p_cl, sRef p_sr) /*@*/ ;
103 extern flagcode specialClause_postErrorCode (specialClause p_cl) /*@*/ ;
104 extern /*@observer@*/ cstring
105 specialClause_postErrorString (specialClause p_cl, sRef p_sr) /*@*/ ;
107 extern sRefTest specialClause_getPreTestFunction (specialClause p_cl) /*@*/ ;
109 extern sRefTest specialClause_getPostTestFunction (specialClause p_cl) /*@*/ ;
110 extern sRefShower specialClause_getPostTestShower (specialClause p_cl) /*@*/ ;
113 specialClause_create (stateConstraint p_st, specialClauseKind p_k, /*@only@*/ sRefSet p_s)
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) /*@*/ ;
122 /*@constant null specialClauses specialClauses_undefined@*/
123 # define specialClauses_undefined ((specialClauses) 0)
125 extern /*@falsenull@*/ bool specialClauses_isDefined (specialClauses p_s) /*@*/ ;
126 # define specialClauses_isDefined(s) ((s) != specialClauses_undefined)
128 extern /*@truenull@*/ bool specialClauses_isUndefined (specialClauses p_s) /*@*/ ;
129 # define specialClauses_isUndefined(s) ((s) == specialClauses_undefined)
131 extern /*@unused@*/ int
132 specialClauses_size (/*@sef@*/ specialClauses p_s) /*@*/ ;
133 # define specialClauses_size(s) (specialClauses_isDefined (s) ? (s)->nelements : 0)
135 extern cstring specialClause_unparseKind (specialClause p_s) /*@*/ ;
137 extern specialClauses
138 specialClauses_add (/*@returned@*/ specialClauses p_s,
139 /*@only@*/ specialClause p_el)
142 extern /*@unused@*/ cstring specialClauses_unparse (specialClauses p_s) /*@*/ ;
143 extern void specialClauses_free (/*@only@*/ specialClauses p_s) ;
145 extern /*@only@*/ specialClauses specialClauses_copy (specialClauses p_s) /*@*/ ;
147 extern cstring specialClauses_dump (specialClauses p_s) /*@*/ ;
148 extern specialClauses specialClauses_undump (char **p_s) /*@modifies *p_s@*/ ;
150 /*@constant int specialClausesBASESIZE;@*/
151 # define specialClausesBASESIZE MIDBASESIZE
153 extern void specialClauses_checkEqual (uentry p_old, uentry p_unew)
154 /*@modifies g_msgstream@*/ ;
157 # error "Multiple include"