]>
Commit | Line | Data |
---|---|---|
1 | /* | |
2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001. | |
3 | ** See ../LICENSE for license information. | |
4 | ** | |
5 | */ | |
6 | /* | |
7 | ** functionClause.h | |
8 | */ | |
9 | ||
10 | # ifndef FUNCTIONCLAUSE_H | |
11 | # define FUNCTIONCLAUSE_H | |
12 | ||
13 | /*@private@*/ typedef enum { | |
14 | FCK_GLOBALS, | |
15 | FCK_MODIFIES, | |
16 | FCK_WARN, | |
17 | FCK_STATE, | |
18 | FCK_DEAD | |
19 | } functionClauseKind; | |
20 | ||
21 | struct s_functionClause { | |
22 | functionClauseKind kind; | |
23 | union { | |
24 | globalsClause globals; | |
25 | modifiesClause modifies; | |
26 | warnClause warn; | |
27 | stateClause state; | |
28 | } val; | |
29 | } ; | |
30 | ||
31 | /* functionClause defined in forwardTypes.h */ | |
32 | ||
33 | /*@constant null functionClause functionClause_undefined; @*/ | |
34 | # define functionClause_undefined NULL | |
35 | ||
36 | extern /*@falsenull@*/ bool functionClause_isDefined(functionClause) /*@*/ ; | |
37 | # define functionClause_isDefined(p_h) ((p_h) != functionClause_undefined) | |
38 | ||
39 | extern bool functionClause_isGlobals (functionClause) /*@*/ ; | |
40 | # define functionClause_isGlobals(p_h) (functionClause_matchKind(p_h, FCK_GLOBALS)) | |
41 | ||
42 | extern bool functionClause_isNoMods (/*@sef@*/ functionClause) /*@*/ ; | |
43 | # define functionClause_isNoMods(p_h) (functionClause_matchKind(p_h, FCK_MODIFIES) && modifiesClause_isNoMods (functionClause_getModifies (p_h))) | |
44 | extern bool functionClause_isModifies (functionClause) /*@*/ ; | |
45 | # define functionClause_isModifies(p_h) (functionClause_matchKind(p_h, FCK_MODIFIES)) | |
46 | ||
47 | extern bool functionClause_isState (functionClause) /*@*/ ; | |
48 | # define functionClause_isState(p_h) (functionClause_matchKind(p_h, FCK_STATE)) | |
49 | ||
50 | extern bool functionClause_isWarn (functionClause) /*@*/ ; | |
51 | # define functionClause_isWarn(p_h) (functionClause_matchKind(p_h, FCK_WARN)) | |
52 | ||
53 | extern /*@truenull@*/ bool functionClause_isUndefined(functionClause) /*@*/ ; | |
54 | # define functionClause_isUndefined(p_h) ((p_h) == functionClause_undefined) | |
55 | ||
56 | extern functionClause functionClause_createGlobals (/*@only@*/ globalsClause) /*@*/ ; | |
57 | extern functionClause functionClause_createModifies (/*@only@*/ modifiesClause) /*@*/ ; | |
58 | extern functionClause functionClause_createWarn (/*@only@*/ warnClause) /*@*/ ; | |
59 | extern functionClause functionClause_createState (/*@only@*/ stateClause) /*@*/ ; | |
60 | ||
61 | extern /*@exposed@*/ globalsClause functionClause_getGlobals (functionClause) /*@*/ ; | |
62 | extern /*@exposed@*/ modifiesClause functionClause_getModifies (functionClause) /*@*/ ; | |
63 | extern /*@exposed@*/ stateClause functionClause_getState (functionClause) /*@*/ ; | |
64 | extern /*@exposed@*/ warnClause functionClause_getWarn (functionClause) /*@*/ ; | |
65 | ||
66 | extern /*@only@*/ stateClause functionClause_takeState (functionClause p_fc) /*@modifies p_fc@*/ ; | |
67 | extern /*@only@*/ warnClause functionClause_takeWarn (functionClause p_fc) /*@modifies p_fc@*/ ; | |
68 | ||
69 | extern bool functionClause_matchKind (functionClause p_p, functionClauseKind p_kind) /*@*/ ; | |
70 | ||
71 | extern void functionClause_free (/*@only@*/ functionClause p_node) ; | |
72 | extern /*@only@*/ cstring functionClause_unparse (functionClause p_p) /*@*/ ; | |
73 | ||
74 | # else | |
75 | # error "Multiple include" | |
76 | # endif |