2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
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 /*@null@*/ globalsClause globals
;
27 /*@null@*/ modifiesClause modifies
;
28 /*@null@*/ warnClause warn
;
29 /*@null@*/ stateClause state
;
30 /*@null@*/ functionConstraint constraint
;
34 /* functionClause defined in forwardTypes.h */
36 /*@constant null functionClause functionClause_undefined; @*/
37 # define functionClause_undefined NULL
39 extern /*@falsewhennull@*/ bool functionClause_isDefined(functionClause
) /*@*/ ;
40 # define functionClause_isDefined(p_h) ((p_h) != functionClause_undefined)
42 extern bool functionClause_isGlobals (functionClause
) /*@*/ ;
43 # define functionClause_isGlobals(p_h) (functionClause_matchKind(p_h, FCK_GLOBALS))
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))
50 extern bool functionClause_isState (functionClause
) /*@*/ ;
51 # define functionClause_isState(p_h) (functionClause_matchKind(p_h, FCK_STATE))
53 extern bool functionClause_isWarn (functionClause
) /*@*/ ;
54 # define functionClause_isWarn(p_h) (functionClause_matchKind(p_h, FCK_WARN))
56 extern bool functionClause_isEnsures (functionClause
) /*@*/ ;
57 # define functionClause_isEnsures(p_h) (functionClause_matchKind(p_h, FCK_ENSURES))
59 extern bool functionClause_isRequires (functionClause
) /*@*/ ;
60 # define functionClause_isRequires(p_h) (functionClause_matchKind(p_h, FCK_REQUIRES))
62 extern /*@nullwhentrue@*/ bool functionClause_isUndefined(functionClause
) /*@*/ ;
63 # define functionClause_isUndefined(p_h) ((p_h) == functionClause_undefined)
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
) /*@*/ ;
69 extern functionClause
functionClause_createEnsures (/*@only@*/ functionConstraint
) /*@*/ ;
70 extern functionClause
functionClause_createRequires (/*@only@*/ functionConstraint
) /*@*/ ;
72 extern /*@exposed@*/ globalsClause
functionClause_getGlobals (functionClause
) /*@*/ ;
73 extern /*@exposed@*/ modifiesClause
functionClause_getModifies (functionClause
) /*@*/ ;
74 extern /*@exposed@*/ functionConstraint
functionClause_getRequires (functionClause
) /*@*/ ;
76 extern /*@only@*/ stateClause
functionClause_takeState (functionClause p_fc
) /*@modifies p_fc@*/ ;
77 extern /*@only@*/ functionConstraint
functionClause_takeEnsures (functionClause p_fc
) /*@modifies p_fc@*/ ;
78 extern /*@only@*/ functionConstraint
functionClause_takeRequires (functionClause p_fc
) /*@modifies p_fc@*/ ;
79 extern /*@only@*/ warnClause
functionClause_takeWarn (functionClause p_fc
) /*@modifies p_fc@*/ ;
81 extern bool functionClause_matchKind (functionClause p_p
, functionClauseKind p_kind
) /*@*/ ;
83 extern void functionClause_free (/*@only@*/ functionClause p_node
) ;
84 extern /*@only@*/ cstring
functionClause_unparse (functionClause p_p
) /*@*/ ;
87 # error "Multiple include"