Fixes after removing -unrecogcomments flag for make splintme.

[splint.git] / src / Headers / functionClause.h

diff --git a/src/Headers/functionClause.h b/src/Headers/functionClause.h
index c0bc5d5b6d3778641c0d002eea222f8092a7511e..3b24bc72a83c48f6a52d6811cc48469f68a00c34 100644 (file)
--- a/src/Headers/functionClause.h
+++ b/src/Headers/functionClause.h
@@ -1,5 +1,5 @@
 /*
-** 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.
 **
 */
@@ -10,21 +10,24 @@
 # 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_DEAD
 } functionClauseKind;
 
 struct s_functionClause {
   functionClauseKind kind;
   union {
-    globalsClause globals;
-    modifiesClause modifies;
-    warnClause warn;
-    stateClause state;
+    /*@null@*/ globalsClause globals;
+    /*@null@*/ modifiesClause modifies;
+    /*@null@*/ warnClause warn;
+    /*@null@*/ stateClause state;
+    /*@null@*/ functionConstraint constraint;
   } val;
 } ;
 
@@ -33,7 +36,7 @@ struct s_functionClause {
 /*@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) /*@*/ ;
@@ -50,20 +53,32 @@ extern bool functionClause_isState (functionClause) /*@*/ ;
 extern bool functionClause_isWarn (functionClause) /*@*/ ;
 # define functionClause_isWarn(p_h) (functionClause_matchKind(p_h, FCK_WARN))
 
-extern /*@truenull@*/ bool functionClause_isUndefined(functionClause) /*@*/ ;
+extern bool functionClause_isEnsures (functionClause) /*@*/ ;
+# define functionClause_isEnsures(p_h) (functionClause_matchKind(p_h, FCK_ENSURES))
+
+extern bool functionClause_isRequires (functionClause) /*@*/ ;
+# define functionClause_isRequires(p_h) (functionClause_matchKind(p_h, FCK_REQUIRES))
+
+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@*/ 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@*/ functionConstraint functionClause_getEnsures (functionClause) /*@*/ ;
+extern /*@exposed@*/ functionConstraint functionClause_getRequires (functionClause) /*@*/ ;
 
 extern /*@only@*/ stateClause functionClause_takeState (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) /*@*/ ;