]>
Commit | Line | Data |
---|---|---|
28bf4b0b | 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, | |
d9a28762 | 18 | FCK_ENSURES, |
19 | FCK_REQUIRES, | |
28bf4b0b | 20 | FCK_DEAD |
21 | } functionClauseKind; | |
22 | ||
23 | struct s_functionClause { | |
24 | functionClauseKind kind; | |
25 | union { | |
26 | globalsClause globals; | |
27 | modifiesClause modifies; | |
28 | warnClause warn; | |
29 | stateClause state; | |
3814599d | 30 | functionConstraint constraint; |
28bf4b0b | 31 | } val; |
32 | } ; | |
33 | ||
34 | /* functionClause defined in forwardTypes.h */ | |
35 | ||
36 | /*@constant null functionClause functionClause_undefined; @*/ | |
37 | # define functionClause_undefined NULL | |
38 | ||
39 | extern /*@falsenull@*/ bool functionClause_isDefined(functionClause) /*@*/ ; | |
40 | # define functionClause_isDefined(p_h) ((p_h) != functionClause_undefined) | |
41 | ||
42 | extern bool functionClause_isGlobals (functionClause) /*@*/ ; | |
43 | # define functionClause_isGlobals(p_h) (functionClause_matchKind(p_h, FCK_GLOBALS)) | |
44 | ||
45 | extern bool functionClause_isNoMods (/*@sef@*/ functionClause) /*@*/ ; | |
46 | # define functionClause_isNoMods(p_h) (functionClause_matchKind(p_h, FCK_MODIFIES) && modifiesClause_isNoMods (functionClause_getModifies (p_h))) | |
47 | extern bool functionClause_isModifies (functionClause) /*@*/ ; | |
48 | # define functionClause_isModifies(p_h) (functionClause_matchKind(p_h, FCK_MODIFIES)) | |
49 | ||
50 | extern bool functionClause_isState (functionClause) /*@*/ ; | |
51 | # define functionClause_isState(p_h) (functionClause_matchKind(p_h, FCK_STATE)) | |
52 | ||
53 | extern bool functionClause_isWarn (functionClause) /*@*/ ; | |
54 | # define functionClause_isWarn(p_h) (functionClause_matchKind(p_h, FCK_WARN)) | |
55 | ||
d9a28762 | 56 | extern bool functionClause_isEnsures (functionClause) /*@*/ ; |
57 | # define functionClause_isEnsures(p_h) (functionClause_matchKind(p_h, FCK_ENSURES)) | |
58 | ||
59 | extern bool functionClause_isRequires (functionClause) /*@*/ ; | |
60 | # define functionClause_isRequires(p_h) (functionClause_matchKind(p_h, FCK_REQUIRES)) | |
61 | ||
28bf4b0b | 62 | extern /*@truenull@*/ bool functionClause_isUndefined(functionClause) /*@*/ ; |
63 | # define functionClause_isUndefined(p_h) ((p_h) == functionClause_undefined) | |
64 | ||
65 | extern functionClause functionClause_createGlobals (/*@only@*/ globalsClause) /*@*/ ; | |
66 | extern functionClause functionClause_createModifies (/*@only@*/ modifiesClause) /*@*/ ; | |
67 | extern functionClause functionClause_createWarn (/*@only@*/ warnClause) /*@*/ ; | |
68 | extern functionClause functionClause_createState (/*@only@*/ stateClause) /*@*/ ; | |
3814599d | 69 | extern functionClause functionClause_createEnsures (/*@only@*/ functionConstraint) /*@*/ ; |
70 | extern functionClause functionClause_createRequires (/*@only@*/ functionConstraint) /*@*/ ; | |
28bf4b0b | 71 | |
72 | extern /*@exposed@*/ globalsClause functionClause_getGlobals (functionClause) /*@*/ ; | |
73 | extern /*@exposed@*/ modifiesClause functionClause_getModifies (functionClause) /*@*/ ; | |
74 | extern /*@exposed@*/ stateClause functionClause_getState (functionClause) /*@*/ ; | |
75 | extern /*@exposed@*/ warnClause functionClause_getWarn (functionClause) /*@*/ ; | |
3814599d | 76 | extern /*@exposed@*/ functionConstraint functionClause_getEnsures (functionClause) /*@*/ ; |
77 | extern /*@exposed@*/ functionConstraint functionClause_getRequires (functionClause) /*@*/ ; | |
28bf4b0b | 78 | |
79 | extern /*@only@*/ stateClause functionClause_takeState (functionClause p_fc) /*@modifies p_fc@*/ ; | |
3814599d | 80 | extern /*@only@*/ functionConstraint functionClause_takeEnsures (functionClause p_fc) /*@modifies p_fc@*/ ; |
81 | extern /*@only@*/ functionConstraint functionClause_takeRequires (functionClause p_fc) /*@modifies p_fc@*/ ; | |
28bf4b0b | 82 | extern /*@only@*/ warnClause functionClause_takeWarn (functionClause p_fc) /*@modifies p_fc@*/ ; |
83 | ||
84 | extern bool functionClause_matchKind (functionClause p_p, functionClauseKind p_kind) /*@*/ ; | |
85 | ||
86 | extern void functionClause_free (/*@only@*/ functionClause p_node) ; | |
87 | extern /*@only@*/ cstring functionClause_unparse (functionClause p_p) /*@*/ ; | |
88 | ||
89 | # else | |
90 | # error "Multiple include" | |
91 | # endif |