]>
Commit | Line | Data |
---|---|---|
28bf4b0b | 1 | /* |
c0de361f | 2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003. |
28bf4b0b | 3 | ** See ../LICENSE for license information. |
4 | */ | |
5 | /* | |
6 | ** stateClause.h | |
7 | */ | |
8 | ||
9 | # ifndef STATECLAUSE_H | |
10 | # define STATECLAUSE_H | |
11 | ||
12 | typedef enum | |
13 | { | |
14 | SP_USES, | |
15 | SP_DEFINES, | |
16 | SP_ALLOCATES, | |
17 | SP_RELEASES, | |
18 | SP_SETS, | |
19 | SP_QUAL, | |
20 | SP_GLOBAL | |
21 | } stateClauseKind ; | |
22 | ||
23 | typedef enum | |
24 | { | |
25 | TK_BEFORE, | |
26 | TK_AFTER, | |
27 | TK_BOTH | |
28 | } stateConstraint; | |
29 | ||
30 | struct s_stateClause | |
31 | { | |
32 | stateConstraint state; | |
33 | stateClauseKind kind; | |
34 | qual squal; /* only for SP_QUAL and SP_GLOBAL */ | |
35 | sRefSet refs; | |
36 | fileloc loc; | |
37 | } ; | |
38 | ||
39 | /* in forwardTypes.h: abst_typedef struct _stateClause *stateClause; */ | |
40 | ||
41 | typedef /*@only@*/ stateClause o_stateClause; | |
42 | ||
43 | extern /*@unused@*/ cstring stateClause_unparse (stateClause p_s) /*@*/ ; | |
44 | ||
45 | extern /*@null@*/ sRefMod | |
46 | stateClause_getEffectFunction (stateClause p_cl) /*@*/ ; | |
47 | ||
48 | extern /*@null@*/ sRefModVal | |
49 | stateClause_getEnsuresFunction (stateClause p_cl) /*@*/ ; | |
50 | ||
51 | extern /*@null@*/ sRefModVal | |
52 | stateClause_getRequiresBodyFunction (stateClause p_cl) /*@*/ ; | |
53 | ||
54 | extern int | |
55 | stateClause_getStateParameter (stateClause p_cl) /*@*/ ; | |
56 | ||
57 | extern /*@null@*/ sRefMod | |
58 | stateClause_getReturnEffectFunction (stateClause p_cl) /*@*/ ; | |
59 | ||
60 | extern /*@null@*/ sRefMod | |
61 | stateClause_getEntryFunction (stateClause p_cl) /*@*/ ; | |
62 | ||
63 | extern bool stateClause_isGlobal (stateClause p_cl) /*@*/ ; | |
64 | # define stateClause_isGlobal(cl) ((cl)->kind == SP_GLOBAL) | |
65 | ||
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) /*@*/ ; | |
70 | ||
71 | extern bool stateClause_sameKind (stateClause p_s1, stateClause p_s2) /*@*/ ; | |
72 | ||
73 | extern /*@observer@*/ sRefSet stateClause_getRefs (stateClause p_cl) /*@*/ ; | |
74 | # define stateClause_getRefs(cl) ((cl)->refs) | |
75 | ||
76 | extern flagcode stateClause_preErrorCode (stateClause p_cl) /*@*/ ; | |
77 | extern /*@observer@*/ cstring | |
78 | stateClause_preErrorString (stateClause p_cl, sRef p_sr) /*@*/ ; | |
79 | ||
80 | extern flagcode stateClause_postErrorCode (stateClause p_cl) /*@*/ ; | |
81 | extern /*@observer@*/ cstring | |
82 | stateClause_postErrorString (stateClause p_cl, sRef p_sr) /*@*/ ; | |
83 | ||
84 | extern sRefTest stateClause_getPreTestFunction (stateClause p_cl) /*@*/ ; | |
85 | extern sRefTest stateClause_getPostTestFunction (stateClause p_cl) /*@*/ ; | |
86 | extern sRefShower stateClause_getPostTestShower (stateClause p_cl) /*@*/ ; | |
87 | ||
88 | extern stateClause | |
89 | stateClause_create (lltok p_tok, qual p_q, /*@only@*/ sRefSet p_s) /*@*/ ; | |
90 | ||
91 | extern stateClause | |
92 | stateClause_createPlain (lltok p_tok, /*@only@*/ sRefSet p_s) /*@*/ ; | |
93 | ||
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) /*@*/ ; | |
99 | ||
100 | extern /*@observer@*/ fileloc stateClause_loc (stateClause) /*@*/ ; | |
101 | extern bool stateClause_isMemoryAllocation (stateClause p_cl) /*@*/ ; | |
3e3ec469 | 102 | extern bool stateClause_isQual (stateClause p_cl) /*@*/ ; |
103 | ||
28bf4b0b | 104 | extern void stateClause_free (/*@only@*/ stateClause p_s) ; |
105 | extern cstring stateClause_dump (stateClause p_s) /*@*/ ; | |
106 | extern stateClause stateClause_undump (char **p_s) /*@modifies *p_s@*/ ; | |
107 | extern stateClause stateClause_copy (stateClause p_s) /*@*/ ; | |
108 | extern bool stateClause_matchKind (stateClause p_s1, stateClause p_s2) /*@*/ ; | |
109 | ||
110 | extern bool stateClause_hasEnsures (stateClause p_cl) /*@*/ ; | |
111 | extern bool stateClause_hasRequires (stateClause p_cl) /*@*/ ; | |
112 | ||
113 | extern bool stateClause_setsMetaState (stateClause p_cl) /*@*/ ; | |
114 | extern qual stateClause_getMetaQual (stateClause p_cl) /*@*/ ; | |
115 | ||
116 | # else | |
117 | # error "Multiple include" | |
118 | # endif | |
119 | ||
120 |