]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
28bf4b0b | 2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001. |
885824d3 | 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 | ||
885824d3 | 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); | |
28bf4b0b | 40 | extern void clabstract_declareFunction (/*@only@*/ idDecl p_tid) |
885824d3 | 41 | /*@globals internalState@*/ ; |
42 | extern void doVaDcl (void); | |
43 | extern void doneParams (void); | |
44 | ||
45 | extern void setCurrentParams (/*@dependent@*/ uentryList p_ue); | |
46 | extern void clearCurrentParams (void); | |
47 | ||
48 | extern /*@exposed@*/ sRef fixModifiesId (cstring p_s); | |
28bf4b0b | 49 | extern /*@exposed@*/ sRef fixStateClausesId (cstring p_s); |
885824d3 | 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 | ||
28bf4b0b | 65 | extern /*@exposed@*/ sRef modListArrayFetch (/*@exposed@*/ sRef p_s, sRef p_mexp); |
66 | extern /*@exposed@*/ sRef modListPointer (/*@exposed@*/ sRef p_s); | |
885824d3 | 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 | ||
28bf4b0b | 70 | extern /*@dependent@*/ sRef clabstract_unrecognizedGlobal (cstring p_s); |
71 | extern /*@dependent@*/ sRef clabstract_createGlobal (/*@temp@*/ sRef p_sr, /*@only@*/ qualList p_quals); | |
885824d3 | 72 | |
73 | extern void checkDoneParams (void); | |
885824d3 | 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); | |
28bf4b0b | 86 | extern /*@exposed@*/ sRef checkStateClausesId (uentry p_ue); |
885824d3 | 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 | ||
103db890 | 94 | /*drl |
95 | added to header 1/19/2001 | |
96 | (added to clabstract earilier | |
97 | */ | |
98 | ||
99 | constraintList getFunctionConstraints (void); | |
100 | ||
101 | constraintList getEnsuresConstraints (void); | |
102 | ||
28bf4b0b | 103 | void setEnsuresConstraints (constraintList p_c); |
103db890 | 104 | |
28bf4b0b | 105 | void setFunctionConstraints (constraintList p_c); |
106 | sRef checkbufferConstraintClausesId (uentry p_ue); | |
bb25bea6 | 107 | void setImplictfcnConstraints (void); |
108 | ||
2934b455 | 109 | /*@observer@*/ constraintList getImplicitFcnConstraints (void); |
110 | ||
103db890 | 111 | /* end drl*/ |
bb25bea6 | 112 | |
113 | ||
28bf4b0b | 114 | extern /*@dependent@*/ sRef clabstract_checkGlobal (/*@only@*/ exprNode) ; |
115 | ||
116 | extern void clabstract_initMod (void) /*@modifies internalState@*/ ; | |
117 | ||
885824d3 | 118 | # else |
119 | # error "Multiple include" | |
120 | # endif | |
121 | ||
122 | ||
123 | ||
124 | ||
125 | ||
126 | ||
127 | ||
128 |