src/Headers/clabstract.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001.
   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 extern void clabstract_declareFunction (/*@only@*/ idDecl p_tid)
  41    /*@globals internalState@*/ ;
  42 extern void doVaDcl (void);
  43 extern void oldStyleDoneParams (void);
  44
  45 extern void setCurrentParams (/*@dependent@*/ uentryList p_ue);
  46 extern void clearCurrentParams (void);
  47
  48 extern /*@exposed@*/ sRef fixModifiesId (cstring p_s);
  49 extern /*@exposed@*/ sRef fixStateClausesId (cstring p_s);
  50
  51 extern void setFlipOldStyle(void);
  52 extern void setNewStyle(void);
  53 extern void unsetProcessingGlobals (void);
  54 extern void setProcessingIterVars (uentry p_iter);
  55 extern void setProcessingTypedef (/*@only@*/ qtype p_q);
  56 extern void setProcessingVars (/*@only@*/ qtype p_q);
  57 extern void setStorageClass (storageClassCode p_sc);
  58 extern void storeLoc (void);
  59 extern void unsetProcessingTypedef (void);
  60 extern void unsetProcessingVars (void);
  61
  62 extern /*@only@*/ uentry makeCurrentParam (idDecl p_t);
  63 extern void setProcessingGlobalsList (void);
  64
  65 extern /*@exposed@*/ sRef modListArrayFetch (/*@exposed@*/ sRef p_s, sRef p_mexp);
  66 extern /*@exposed@*/ sRef modListPointer (/*@exposed@*/ sRef p_s);
  67 extern /*@exposed@*/ sRef modListFieldAccess (sRef p_s, /*@only@*/ cstring p_f);
  68 extern /*@exposed@*/ sRef modListArrowAccess (sRef p_s, /*@only@*/ cstring p_f);
  69
  70 extern /*@dependent@*/ sRef clabstract_unrecognizedGlobal (cstring p_s);
  71 extern /*@dependent@*/ sRef clabstract_createGlobal (/*@temp@*/ sRef p_sr, /*@only@*/ qualList p_quals);
  72
  73 extern void checkDoneParams (void);
  74 extern void exitParamsTemp (void);
  75 extern void enterParamsTemp (void);
  76
  77 extern void clearProcessingGlobMods (void);
  78 extern bool isProcessingGlobMods (void);
  79 extern void setProcessingGlobMods (void);
  80
  81 extern void setFunctionNoGlobals (void);
  82 extern int iterParamNo (void);
  83 extern void nextIterParam (void);
  84 extern void declareCIter (cstring p_name, /*@owned@*/ uentryList p_params);
  85 extern void checkModifiesId (uentry p_ue);
  86 extern /*@exposed@*/ sRef checkStateClausesId (uentry p_ue);
  87
  88 extern void checkConstant (qtype p_t, idDecl p_id) ;
  89 extern void checkValueConstant (qtype p_t, idDecl p_id, exprNode p_e) ;
  90
  91 extern void declareStaticFunction (/*@only@*/ idDecl p_tid)
  92    /*@globals internalState@*/ ;
  93
  94    /*drl
  95      added to header 1/19/2001
  96      (added to clabstract earilier
  97    */
  98
  99 extern sRef checkbufferConstraintClausesId (uentry p_ue);
 100 extern void setImplictfcnConstraints (void);
 101
 102 /*@observer@*/ constraintList  getImplicitFcnConstraints (void);
 103
 104 /* end drl*/
 105
 106
 107 extern /*@dependent@*/ sRef clabstract_checkGlobal (/*@only@*/ exprNode) ;
 108
 109 extern void clabstract_initMod (void) /*@modifies internalState@*/ ;
 110
 111 # else
 112 # error "Multiple include"
 113 # endif
 114
 115
 116
 117
 118
 119
 120
 121