2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
3 ** See ../LICENSE for license information.
10 # define STATECLAUSE_H
32 stateConstraint state;
34 qual squal; /* only for SP_QUAL and SP_GLOBAL */
39 /* in forwardTypes.h: abst_typedef struct _stateClause *stateClause; */
41 typedef /*@only@*/ stateClause o_stateClause;
43 extern /*@unused@*/ cstring stateClause_unparse (stateClause p_s) /*@*/ ;
45 extern /*@null@*/ sRefMod
46 stateClause_getEffectFunction (stateClause p_cl) /*@*/ ;
48 extern /*@null@*/ sRefModVal
49 stateClause_getEnsuresFunction (stateClause p_cl) /*@*/ ;
51 extern /*@null@*/ sRefModVal
52 stateClause_getRequiresBodyFunction (stateClause p_cl) /*@*/ ;
55 stateClause_getStateParameter (stateClause p_cl) /*@*/ ;
57 extern /*@null@*/ sRefMod
58 stateClause_getReturnEffectFunction (stateClause p_cl) /*@*/ ;
60 extern /*@null@*/ sRefMod
61 stateClause_getEntryFunction (stateClause p_cl) /*@*/ ;
63 extern bool stateClause_isGlobal (stateClause p_cl) /*@*/ ;
64 # define stateClause_isGlobal(cl) ((cl)->kind == SP_GLOBAL)
66 extern bool stateClause_isBefore (stateClause p_cl) /*@*/ ;
67 extern bool stateClause_isBeforeOnly (stateClause p_cl) /*@*/ ;
68 extern bool stateClause_isAfter (stateClause p_cl) /*@*/ ;
69 extern bool stateClause_isEnsures (stateClause p_cl) /*@*/ ;
71 extern bool stateClause_sameKind (stateClause p_s1, stateClause p_s2) /*@*/ ;
73 extern /*@observer@*/ sRefSet stateClause_getRefs (stateClause p_cl) /*@*/ ;
74 # define stateClause_getRefs(cl) ((cl)->refs)
76 extern flagcode stateClause_preErrorCode (stateClause p_cl) /*@*/ ;
77 extern /*@observer@*/ cstring
78 stateClause_preErrorString (stateClause p_cl, sRef p_sr) /*@*/ ;
80 extern flagcode stateClause_postErrorCode (stateClause p_cl) /*@*/ ;
81 extern /*@observer@*/ cstring
82 stateClause_postErrorString (stateClause p_cl, sRef p_sr) /*@*/ ;
84 extern sRefTest stateClause_getPreTestFunction (stateClause p_cl) /*@*/ ;
85 extern sRefTest stateClause_getPostTestFunction (stateClause p_cl) /*@*/ ;
86 extern sRefShower stateClause_getPostTestShower (stateClause p_cl) /*@*/ ;
89 stateClause_create (lltok p_tok, qual p_q, /*@only@*/ sRefSet p_s) /*@*/ ;
92 stateClause_createPlain (lltok p_tok, /*@only@*/ sRefSet p_s) /*@*/ ;
94 extern stateClause stateClause_createDefines (/*@only@*/ sRefSet p_s) /*@*/ ;
95 extern stateClause stateClause_createUses (/*@only@*/ sRefSet p_s) /*@*/ ;
96 extern stateClause stateClause_createAllocates (/*@only@*/ sRefSet p_s) /*@*/ ;
97 extern stateClause stateClause_createReleases (/*@only@*/ sRefSet p_s) /*@*/ ;
98 extern stateClause stateClause_createSets (/*@only@*/ sRefSet p_s) /*@*/ ;
100 extern /*@observer@*/ fileloc stateClause_loc (stateClause) /*@*/ ;
101 extern bool stateClause_isMemoryAllocation (stateClause p_cl) /*@*/ ;
102 extern void stateClause_free (/*@only@*/ stateClause p_s) ;
103 extern cstring stateClause_dump (stateClause p_s) /*@*/ ;
104 extern stateClause stateClause_undump (char **p_s) /*@modifies *p_s@*/ ;
105 extern stateClause stateClause_copy (stateClause p_s) /*@*/ ;
106 extern bool stateClause_matchKind (stateClause p_s1, stateClause p_s2) /*@*/ ;
108 extern bool stateClause_hasEnsures (stateClause p_cl) /*@*/ ;
109 extern bool stateClause_hasRequires (stateClause p_cl) /*@*/ ;
111 extern bool stateClause_setsMetaState (stateClause p_cl) /*@*/ ;
112 extern qual stateClause_getMetaQual (stateClause p_cl) /*@*/ ;
115 # error "Multiple include"