/*
-** 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,
struct s_functionClause {
functionClauseKind kind;
union {
- globalsClause globals;
- modifiesClause modifies;
- warnClause warn;
- stateClause state;
- functionConstraint constraint;
+ /*@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 /*@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) /*@*/ ;