/*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
** See ../LICENSE for license information.
**
*/
# ifndef FUNCTIONCLAUSE_H
# define FUNCTIONCLAUSE_H
-/*@private@*/ typedef enum {
+/*:private:*/ typedef enum {
FCK_GLOBALS,
FCK_MODIFIES,
FCK_WARN,
FCK_STATE,
FCK_ENSURES,
FCK_REQUIRES,
- FCK_MTENSURES,
- FCK_MTREQUIRES,
FCK_DEAD
} functionClauseKind;
struct s_functionClause {
functionClauseKind kind;
union {
- globalsClause globals;
- modifiesClause modifies;
- warnClause warn;
- stateClause state;
- constraintList ensures;
- constraintList requires;
- metaStateConstraint mtconstraint;
+ /*@null@*/ globalsClause globals;
+ /*@null@*/ modifiesClause modifies;
+ /*@null@*/ warnClause warn;
+ /*@null@*/ stateClause state;
+ /*@null@*/ functionConstraint constraint;
} val;
} ;
/*@constant null functionClause functionClause_undefined; @*/
# define functionClause_undefined NULL
-extern /*@falsenull@*/ bool functionClause_isDefined(functionClause) /*@*/ ;
+extern /*@falsewhennull@*/ bool functionClause_isDefined(functionClause) /*@*/ ;
# define functionClause_isDefined(p_h) ((p_h) != functionClause_undefined)
extern bool functionClause_isGlobals (functionClause) /*@*/ ;
extern bool functionClause_isRequires (functionClause) /*@*/ ;
# define functionClause_isRequires(p_h) (functionClause_matchKind(p_h, FCK_REQUIRES))
-extern bool functionClause_isMetaRequires (functionClause) /*@*/ ;
-# define functionClause_isMetaRequires(p_h) (functionClause_matchKind(p_h, FCK_MTREQUIRES))
-
-extern bool functionClause_isMetaEnsures (functionClause) /*@*/ ;
-# define functionClause_isMetaEnsures(p_h) (functionClause_matchKind(p_h, FCK_MTENSURES))
-
-extern /*@truenull@*/ bool functionClause_isUndefined(functionClause) /*@*/ ;
+extern /*@nullwhentrue@*/ bool functionClause_isUndefined(functionClause) /*@*/ ;
# define functionClause_isUndefined(p_h) ((p_h) == functionClause_undefined)
extern functionClause functionClause_createGlobals (/*@only@*/ globalsClause) /*@*/ ;
extern functionClause functionClause_createModifies (/*@only@*/ modifiesClause) /*@*/ ;
extern functionClause functionClause_createWarn (/*@only@*/ warnClause) /*@*/ ;
extern functionClause functionClause_createState (/*@only@*/ stateClause) /*@*/ ;
-extern functionClause functionClause_createEnsures (/*@only@*/ constraintList) /*@*/ ;
-extern functionClause functionClause_createRequires (/*@only@*/ constraintList) /*@*/ ;
-extern functionClause functionClause_createMetaEnsures (/*@only@*/ metaStateConstraint) /*@*/ ;
-extern functionClause functionClause_createMetaRequires (/*@only@*/ metaStateConstraint) /*@*/ ;
+extern functionClause functionClause_createEnsures (/*@only@*/ functionConstraint) /*@*/ ;
+extern functionClause functionClause_createRequires (/*@only@*/ functionConstraint) /*@*/ ;
extern /*@exposed@*/ globalsClause functionClause_getGlobals (functionClause) /*@*/ ;
extern /*@exposed@*/ modifiesClause functionClause_getModifies (functionClause) /*@*/ ;
extern /*@exposed@*/ stateClause functionClause_getState (functionClause) /*@*/ ;
extern /*@exposed@*/ warnClause functionClause_getWarn (functionClause) /*@*/ ;
-extern /*@exposed@*/ constraintList functionClause_getEnsures (functionClause) /*@*/ ;
-extern /*@exposed@*/ constraintList functionClause_getRequires (functionClause) /*@*/ ;
-extern /*@exposed@*/ metaStateConstraint functionClause_getMetaConstraint (functionClause) /*@*/ ;
+extern /*@exposed@*/ functionConstraint functionClause_getEnsures (functionClause) /*@*/ ;
+extern /*@exposed@*/ functionConstraint functionClause_getRequires (functionClause) /*@*/ ;
extern /*@only@*/ stateClause functionClause_takeState (functionClause p_fc) /*@modifies p_fc@*/ ;
-extern /*@only@*/ constraintList functionClause_takeEnsures (functionClause p_fc) /*@modifies p_fc@*/ ;
-extern /*@only@*/ constraintList functionClause_takeRequires (functionClause p_fc) /*@modifies p_fc@*/ ;
-extern /*@only@*/ metaStateConstraint functionClause_takeMetaConstraint (functionClause p_fc) /*@modifies p_fc@*/ ;
+extern /*@only@*/ functionConstraint functionClause_takeEnsures (functionClause p_fc) /*@modifies p_fc@*/ ;
+extern /*@only@*/ functionConstraint functionClause_takeRequires (functionClause p_fc) /*@modifies p_fc@*/ ;
extern /*@only@*/ warnClause functionClause_takeWarn (functionClause p_fc) /*@modifies p_fc@*/ ;
extern bool functionClause_matchKind (functionClause p_p, functionClauseKind p_kind) /*@*/ ;