src/Headers/clabstract.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2003.
   3 ** See ../LICENSE for license information.
   4 **
   5 */
   6 /*
   7 ** clabstract.h
   8 */
   9
  10 # ifndef CLABSTRACT_H
  11 # define CLABSTRACT_H
  12
  13 extern void setArgsUsed (void) /*@modifies internalState@*/ ;
  14 extern void setSpecialFunction (qual p_qu) /*@modifies internalState@*/ ;
  15 extern bool isFlipOldStyle(void) /*@*/ ;
  16 extern bool isNewStyle(void) /*@*/ ;
  17 extern bool processingIterVars(void) /*@*/ ;
  18
  19 extern ctype declareEnum (/*@only@*/ cstring p_ename, /*@only@*/ enumNameList p_el);
  20 extern ctype declareStruct (/*@temp@*/ cstring p_id, /*@only@*/ uentryList p_f);
  21 extern ctype declareUnnamedStruct (/*@only@*/ uentryList p_f);
  22
  23 extern ctype declareUnion (/*@temp@*/ cstring p_id, /*@only@*/ uentryList p_f);
  24 extern ctype declareUnnamedUnion (/*@only@*/ uentryList p_f);
  25
  26 extern ctype declareUnnamedEnum (/*@only@*/ enumNameList p_el);
  27 extern ctype handleEnum (/*@only@*/ cstring p_id);
  28 extern ctype handleStruct (/*@only@*/ cstring p_id);
  29 extern ctype handleUnion (/*@only@*/ cstring p_id);
  30
  31 extern uentryList handleParamIdList (/*@returned@*/ /*@dependent@*/ uentryList p_params);
  32 extern uentryList handleParamTypeList (/*@dependent@*/ /*@returned@*/ uentryList p_params);
  33
  34 extern uentryList fixUentryList (/*@only@*/ idDeclList p_tl, qtype p_q);
  35 extern uentryList fixUnnamedDecl (qtype p_q) /*@*/ ;
  36
  37 extern /*@exposed@*/ uentry getCurrentIter(void);
  38
  39 extern void processNamedDecl (idDecl p_t);
  40
  41 extern void clabstract_declareType (/*@only@*/ exprNodeList, /*@only@*/ warnClause)
  42    /*@modifies internalState@*/ ;
  43
  44 extern void clabstract_declareFunction (/*@only@*/ idDecl p_tid)
  45    /*@globals internalState@*/ ;
  46 extern void doVaDcl (void);
  47 extern void oldStyleDoneParams (void);
  48
  49 extern void setCurrentParams (/*@dependent@*/ uentryList p_ue);
  50 extern void clearCurrentParams (void);
  51
  52 extern /*@exposed@*/ sRef fixModifiesId (cstring p_s);
  53 extern /*@exposed@*/ sRef fixStateClausesId (cstring p_s);
  54
  55 extern void setFlipOldStyle(void);
  56 extern void setNewStyle(void);
  57 extern void unsetProcessingGlobals (void);
  58 extern void setProcessingIterVars (uentry p_iter);
  59 extern void setProcessingTypedef (/*@only@*/ qtype p_q);
  60 extern void setProcessingVars (/*@only@*/ qtype p_q);
  61 extern void setStorageClass (storageClassCode p_sc);
  62 extern void storeLoc (void);
  63 extern void unsetProcessingTypedef (void);
  64 extern void unsetProcessingVars (void);
  65
  66 extern /*@only@*/ uentry makeCurrentParam (idDecl p_t);
  67 extern void setProcessingGlobalsList (void);
  68
  69 extern /*@exposed@*/ sRef modListArrayFetch (/*@exposed@*/ sRef p_s, sRef p_mexp);
  70 extern /*@exposed@*/ sRef modListPointer (/*@exposed@*/ sRef p_s);
  71 extern /*@exposed@*/ sRef modListFieldAccess (sRef p_s, /*@only@*/ cstring p_f);
  72 extern /*@exposed@*/ sRef modListArrowAccess (sRef p_s, /*@only@*/ cstring p_f);
  73
  74 extern /*@dependent@*/ sRef clabstract_unrecognizedGlobal (cstring p_s);
  75 extern /*@dependent@*/ sRef clabstract_createGlobal (/*@temp@*/ sRef p_sr, /*@only@*/ qualList p_quals);
  76
  77 extern void checkDoneParams (void);
  78 extern void exitParamsTemp (void);
  79 extern void enterParamsTemp (void);
  80
  81 extern void clearProcessingGlobMods (void);
  82 extern bool isProcessingGlobMods (void);
  83 extern void setProcessingGlobMods (void);
  84
  85 extern void setFunctionNoGlobals (void);
  86 extern int iterParamNo (void);
  87 extern void nextIterParam (void);
  88 extern void declareCIter (cstring p_name, /*@owned@*/ uentryList p_params);
  89 extern void checkModifiesId (uentry p_ue);
  90 extern /*@exposed@*/ sRef checkStateClausesId (uentry p_ue);
  91
  92 extern void checkConstant (qtype p_t, idDecl p_id) ;
  93 extern void checkValueConstant (qtype p_t, idDecl p_id, exprNode p_e) ;
  94
  95 extern void declareStaticFunction (/*@only@*/ idDecl p_tid)
  96    /*@globals internalState@*/ ;
  97
  98    /*drl
  99      added to header 1/19/2001
 100      (added to clabstract earilier
 101    */
 102
 103 extern sRef checkbufferConstraintClausesId (uentry p_ue);
 104 extern void setImplictfcnConstraints (void);
 105
 106 /*@observer@*/ constraintList  getImplicitFcnConstraints (void);
 107
 108 /* end drl*/
 109
 110
 111 extern /*@dependent@*/ sRef clabstract_checkGlobal (/*@only@*/ exprNode) ;
 112
 113 extern void clabstract_initMod (void) /*@modifies internalState@*/ ;
 114
 115 # else
 116 # error "Multiple include"
 117 # endif
 118
 119
 120
 121
 122
 123
 124
 125