src/Headers/clabstract.h

   1 /*
   2 ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2000.
   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 void
  27   setFunctionSpecialClause (lltok p_stok, /*@only@*/ sRefSet p_s, lltok p_etok);
  28 extern void
  29   setFunctionStateSpecialClause (lltok p_stok, specialClauseKind p_kind,
  30                                  /*@only@*/ sRefSet p_s, lltok p_etok);
  31
  32 extern ctype declareUnnamedEnum (/*@only@*/ enumNameList p_el);
  33 extern ctype handleEnum (/*@only@*/ cstring p_id);
  34 extern ctype handleStruct (/*@only@*/ cstring p_id);
  35 extern ctype handleUnion (/*@only@*/ cstring p_id);
  36
  37 extern uentryList handleParamIdList (/*@returned@*/ /*@dependent@*/ uentryList p_params);
  38 extern uentryList handleParamTypeList (/*@dependent@*/ /*@returned@*/ uentryList p_params);
  39
  40 extern uentryList fixUentryList (/*@only@*/ idDeclList p_tl, qtype p_q);
  41 extern uentryList fixUnnamedDecl (qtype p_q) /*@*/ ;
  42
  43 extern /*@exposed@*/ uentry getCurrentIter(void);
  44
  45 extern void processNamedDecl (idDecl p_t);
  46 extern void declareFunction (/*@only@*/ idDecl p_tid)
  47    /*@globals internalState@*/ ;
  48 extern void doVaDcl (void);
  49 extern void doneParams (void);
  50
  51 extern void setCurrentParams (/*@dependent@*/ uentryList p_ue);
  52 extern void clearCurrentParams (void);
  53
  54 extern /*@exposed@*/ sRef fixModifiesId (cstring p_s);
  55 extern /*@exposed@*/ sRef fixSpecClausesId (cstring p_s);
  56
  57 extern void setFlipOldStyle(void);
  58 extern void setNewStyle(void);
  59 extern void unsetProcessingGlobals (void);
  60 extern void setProcessingIterVars (uentry p_iter);
  61 extern void setProcessingTypedef (/*@only@*/ qtype p_q);
  62 extern void setProcessingVars (/*@only@*/ qtype p_q);
  63 extern void setStorageClass (storageClassCode p_sc);
  64 extern void storeLoc (void);
  65 extern void unsetProcessingTypedef (void);
  66 extern void unsetProcessingVars (void);
  67
  68 extern /*@only@*/ uentry makeCurrentParam (idDecl p_t);
  69 extern void setProcessingGlobalsList (void);
  70
  71 extern /*@exposed@*/ sRef modListArrayFetch (sRef p_s, sRef p_mexp);
  72 extern /*@exposed@*/ sRef modListPointer (sRef p_s);
  73 extern /*@exposed@*/ sRef modListFieldAccess (sRef p_s, /*@only@*/ cstring p_f);
  74 extern /*@exposed@*/ sRef modListArrowAccess (sRef p_s, /*@only@*/ cstring p_f);
  75
  76 extern sRef globListUnrecognized (cstring p_s);
  77 extern void globListAdd (sRef p_sr, qualList p_quals);
  78
  79 extern void setFunctionModifies (/*@only@*/ sRefSet p_s);
  80
  81 extern void checkDoneParams (void);
  82
  83 extern void exitParamsTemp (void);
  84 extern void enterParamsTemp (void);
  85
  86 extern void clearProcessingGlobMods (void);
  87 extern bool isProcessingGlobMods (void);
  88 extern void setProcessingGlobMods (void);
  89
  90 extern void setFunctionNoGlobals (void);
  91 extern int iterParamNo (void);
  92 extern void nextIterParam (void);
  93 extern void declareCIter (cstring p_name, /*@owned@*/ uentryList p_params);
  94 extern void checkModifiesId (uentry p_ue);
  95 extern /*@exposed@*/ sRef checkSpecClausesId (uentry p_ue);
  96
  97 extern void checkConstant (qtype p_t, idDecl p_id) ;
  98 extern void checkValueConstant (qtype p_t, idDecl p_id, exprNode p_e) ;
  99
 100 extern void declareStaticFunction (/*@only@*/ idDecl p_tid)
 101    /*@globals internalState@*/ ;
 102
 103    /*drl
 104      added to header 1/19/2001
 105      (added to clabstract earilier
 106    */
 107
 108 constraintList getFunctionConstraints (void);
 109
 110 constraintList getEnsuresConstraints (void);
 111
 112 void setEnsuresConstraints (constraintList c);
 113
 114 void setFunctionConstraints (constraintList c);
 115 sRef checkbufferConstraintClausesId (uentry ue);
 116 /* end drl*/
 117 # else
 118 # error "Multiple include"
 119 # endif
 120
 121
 122
 123
 124
 125
 126
 127