2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
3 ** See ../LICENSE for license information.
10 # ifndef FUNCTIONCLAUSE_H
11 # define FUNCTIONCLAUSE_H
13 /*@private@*/ typedef enum {
23 struct s_functionClause {
24 functionClauseKind kind;
26 globalsClause globals;
27 modifiesClause modifies;
30 constraintList ensures;
31 constraintList requires;
35 /* functionClause defined in forwardTypes.h */
37 /*@constant null functionClause functionClause_undefined; @*/
38 # define functionClause_undefined NULL
40 extern /*@falsenull@*/ bool functionClause_isDefined(functionClause) /*@*/ ;
41 # define functionClause_isDefined(p_h) ((p_h) != functionClause_undefined)
43 extern bool functionClause_isGlobals (functionClause) /*@*/ ;
44 # define functionClause_isGlobals(p_h) (functionClause_matchKind(p_h, FCK_GLOBALS))
46 extern bool functionClause_isNoMods (/*@sef@*/ functionClause) /*@*/ ;
47 # define functionClause_isNoMods(p_h) (functionClause_matchKind(p_h, FCK_MODIFIES) && modifiesClause_isNoMods (functionClause_getModifies (p_h)))
48 extern bool functionClause_isModifies (functionClause) /*@*/ ;
49 # define functionClause_isModifies(p_h) (functionClause_matchKind(p_h, FCK_MODIFIES))
51 extern bool functionClause_isState (functionClause) /*@*/ ;
52 # define functionClause_isState(p_h) (functionClause_matchKind(p_h, FCK_STATE))
54 extern bool functionClause_isWarn (functionClause) /*@*/ ;
55 # define functionClause_isWarn(p_h) (functionClause_matchKind(p_h, FCK_WARN))
57 extern bool functionClause_isEnsures (functionClause) /*@*/ ;
58 # define functionClause_isEnsures(p_h) (functionClause_matchKind(p_h, FCK_ENSURES))
60 extern bool functionClause_isRequires (functionClause) /*@*/ ;
61 # define functionClause_isRequires(p_h) (functionClause_matchKind(p_h, FCK_REQUIRES))
63 extern /*@truenull@*/ bool functionClause_isUndefined(functionClause) /*@*/ ;
64 # define functionClause_isUndefined(p_h) ((p_h) == functionClause_undefined)
66 extern functionClause functionClause_createGlobals (/*@only@*/ globalsClause) /*@*/ ;
67 extern functionClause functionClause_createModifies (/*@only@*/ modifiesClause) /*@*/ ;
68 extern functionClause functionClause_createWarn (/*@only@*/ warnClause) /*@*/ ;
69 extern functionClause functionClause_createState (/*@only@*/ stateClause) /*@*/ ;
70 extern functionClause functionClause_createEnsures (/*@only@*/ constraintList) /*@*/ ;
71 extern functionClause functionClause_createRequires (/*@only@*/ constraintList) /*@*/ ;
73 extern /*@exposed@*/ globalsClause functionClause_getGlobals (functionClause) /*@*/ ;
74 extern /*@exposed@*/ modifiesClause functionClause_getModifies (functionClause) /*@*/ ;
75 extern /*@exposed@*/ stateClause functionClause_getState (functionClause) /*@*/ ;
76 extern /*@exposed@*/ warnClause functionClause_getWarn (functionClause) /*@*/ ;
77 extern /*@exposed@*/ constraintList functionClause_getEnsures (functionClause) /*@*/ ;
78 extern /*@exposed@*/ constraintList functionClause_getRequires (functionClause) /*@*/ ;
80 extern /*@only@*/ stateClause functionClause_takeState (functionClause p_fc) /*@modifies p_fc@*/ ;
81 extern /*@only@*/ constraintList functionClause_takeEnsures (functionClause p_fc) /*@modifies p_fc@*/ ;
82 extern /*@only@*/ constraintList functionClause_takeRequires (functionClause p_fc) /*@modifies p_fc@*/ ;
83 extern /*@only@*/ warnClause functionClause_takeWarn (functionClause p_fc) /*@modifies p_fc@*/ ;
85 extern bool functionClause_matchKind (functionClause p_p, functionClauseKind p_kind) /*@*/ ;
87 extern void functionClause_free (/*@only@*/ functionClause p_node) ;
88 extern /*@only@*/ cstring functionClause_unparse (functionClause p_p) /*@*/ ;
91 # error "Multiple include"