X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/bb25bea60268559306e8a0fc4d44990ba3ebea32..b37cf05e81a9ef7fc429327a75dfad628f86c809:/src/Headers/clabstract.h

diff --git a/src/Headers/clabstract.h b/src/Headers/clabstract.h
index 7a26ee2..2ca1633 100644
--- a/src/Headers/clabstract.h
+++ b/src/Headers/clabstract.h
@@ -1,5 +1,5 @@
 /*
-** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
+** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
 ** See ../LICENSE for license information.
 **
 */
@@ -23,12 +23,6 @@ extern ctype declareUnnamedStruct (/*@only@*/ uentryList p_f);
 extern ctype declareUnion (/*@temp@*/ cstring p_id, /*@only@*/ uentryList p_f);
 extern ctype declareUnnamedUnion (/*@only@*/ uentryList p_f);
 
-extern void 
-  setFunctionSpecialClause (lltok p_stok, /*@only@*/ sRefSet p_s, lltok p_etok);
-extern void
-  setFunctionStateSpecialClause (lltok p_stok, specialClauseKind p_kind, 
-				 /*@only@*/ sRefSet p_s, lltok p_etok);
-
 extern ctype declareUnnamedEnum (/*@only@*/ enumNameList p_el);
 extern ctype handleEnum (/*@only@*/ cstring p_id);
 extern ctype handleStruct (/*@only@*/ cstring p_id);
@@ -43,7 +37,7 @@ extern uentryList fixUnnamedDecl (qtype p_q) /*@*/ ;
 extern /*@exposed@*/ uentry getCurrentIter(void);
 
 extern void processNamedDecl (idDecl p_t);
-extern void declareFunction (/*@only@*/ idDecl p_tid) 
+extern void clabstract_declareFunction (/*@only@*/ idDecl p_tid) 
    /*@globals internalState@*/ ;
 extern void doVaDcl (void);
 extern void doneParams (void);
@@ -52,7 +46,7 @@ extern void setCurrentParams (/*@dependent@*/ uentryList p_ue);
 extern void clearCurrentParams (void);
 
 extern /*@exposed@*/ sRef fixModifiesId (cstring p_s);
-extern /*@exposed@*/ sRef fixSpecClausesId (cstring p_s);
+extern /*@exposed@*/ sRef fixStateClausesId (cstring p_s);
 
 extern void setFlipOldStyle(void);
 extern void setNewStyle(void);
@@ -68,18 +62,15 @@ extern void unsetProcessingVars (void);
 extern /*@only@*/ uentry makeCurrentParam (idDecl p_t);
 extern void setProcessingGlobalsList (void);
 
-extern /*@exposed@*/ sRef modListArrayFetch (sRef p_s, sRef p_mexp);
-extern /*@exposed@*/ sRef modListPointer (sRef p_s);
+extern /*@exposed@*/ sRef modListArrayFetch (/*@exposed@*/ sRef p_s, sRef p_mexp);
+extern /*@exposed@*/ sRef modListPointer (/*@exposed@*/ sRef p_s);
 extern /*@exposed@*/ sRef modListFieldAccess (sRef p_s, /*@only@*/ cstring p_f);
 extern /*@exposed@*/ sRef modListArrowAccess (sRef p_s, /*@only@*/ cstring p_f);
 
-extern sRef globListUnrecognized (cstring p_s);
-extern void globListAdd (sRef p_sr, qualList p_quals);
-
-extern void setFunctionModifies (/*@only@*/ sRefSet p_s);
+extern /*@dependent@*/ sRef clabstract_unrecognizedGlobal (cstring p_s);
+extern /*@dependent@*/ sRef clabstract_createGlobal (/*@temp@*/ sRef p_sr, /*@only@*/ qualList p_quals);
 
 extern void checkDoneParams (void);
-
 extern void exitParamsTemp (void);
 extern void enterParamsTemp (void);
 
@@ -92,7 +83,7 @@ extern int iterParamNo (void);
 extern void nextIterParam (void);
 extern void declareCIter (cstring p_name, /*@owned@*/ uentryList p_params);
 extern void checkModifiesId (uentry p_ue);
-extern /*@exposed@*/ sRef checkSpecClausesId (uentry p_ue);
+extern /*@exposed@*/ sRef checkStateClausesId (uentry p_ue);
 
 extern void checkConstant (qtype p_t, idDecl p_id) ;
 extern void checkValueConstant (qtype p_t, idDecl p_id, exprNode p_e) ;
@@ -105,18 +96,21 @@ extern void declareStaticFunction (/*@only@*/ idDecl p_tid)
      (added to clabstract earilier
    */
    
-constraintList getFunctionConstraints (void);
+extern constraintList getFunctionConstraints (void);
+extern constraintList getEnsuresConstraints (void);
+extern void setEnsuresConstraints (constraintList p_c);
+extern void setFunctionConstraints (constraintList p_c);
+extern sRef checkbufferConstraintClausesId (uentry p_ue);
+extern void setImplictfcnConstraints (void);
 
-constraintList getEnsuresConstraints (void);
+/*@observer@*/ constraintList  getImplicitFcnConstraints (void);
 
-void setEnsuresConstraints (constraintList c);
+/* end drl*/
 
-void setFunctionConstraints (constraintList c);
-sRef checkbufferConstraintClausesId (uentry ue);
-void  setImplictfcnConstraints (void);
 
-/* end drl*/
+extern /*@dependent@*/ sRef clabstract_checkGlobal (/*@only@*/ exprNode) ;
 
+extern void clabstract_initMod (void) /*@modifies internalState@*/ ;
 
 # else
 # error "Multiple include"