*** empty log message ***

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

diff --git a/src/Headers/functionClause.h b/src/Headers/functionClause.h
index 8fe5eb0c9b13de9637804935b96b04b4a02b544a..cb57af88311c30f772836fea37f396478af7dd0e 100644 (file)
--- a/src/Headers/functionClause.h
+++ b/src/Headers/functionClause.h
@@ -17,8 +17,6 @@
   FCK_STATE,
   FCK_ENSURES,
   FCK_REQUIRES,
-  FCK_MTENSURES,
-  FCK_MTREQUIRES,
   FCK_DEAD
 } functionClauseKind;
 
@@ -29,9 +27,7 @@ struct s_functionClause {
     modifiesClause modifies;
     warnClause warn;
     stateClause state;
-    constraintList ensures;
-    constraintList requires;
-    metaStateConstraint mtconstraint;
+    functionConstraint constraint;
   } val;
 } ;
 
@@ -63,12 +59,6 @@ extern bool functionClause_isEnsures (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) /*@*/ ;
 # define functionClause_isUndefined(p_h) ((p_h) == functionClause_undefined)
 
@@ -76,23 +66,19 @@ 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) /*@*/ ;