Made allocations involving sizeof work correctly (test/malloc.c).

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

diff --git a/src/Headers/clabstract.h b/src/Headers/clabstract.h
index a07555b6ce87527848eadec090fbb90aa073da1d..afa1455c065b451eb81d8405e7d9d6b9dc0d929c 100644 (file)
--- 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-2003.
 ** 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,16 +37,20 @@ 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_declareType (/*@only@*/ exprNodeList, /*@only@*/ warnClause)
+   /*@modifies internalState@*/ ;
+ 
+extern void clabstract_declareFunction (/*@only@*/ idDecl p_tid) 
    /*@globals internalState@*/ ;
 extern void doVaDcl (void);
-extern void doneParams (void);
+extern void oldStyleDoneParams (void);
 
 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 +66,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 +87,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) ;
@@ -100,6 +95,23 @@ extern void checkValueConstant (qtype p_t, idDecl p_id, exprNode p_e) ;
 extern void declareStaticFunction (/*@only@*/ idDecl p_tid) 
    /*@globals internalState@*/ ;
 
+   /*drl
+     added to header 1/19/2001
+     (added to clabstract earilier
+   */
+   
+extern sRef checkbufferConstraintClausesId (uentry p_ue);
+extern void setImplicitfcnConstraints (void);
+
+/*@observer@*/ constraintList getImplicitFcnConstraints (void);
+
+/* end drl*/
+
+
+extern /*@dependent@*/ sRef clabstract_checkGlobal (/*@only@*/ exprNode) ;
+
+extern void clabstract_initMod (void) /*@modifies internalState@*/ ;
+
 # else
 # error "Multiple include"
 # endif