]> andersk Git - splint.git/blob - src/Headers/varKinds.h
Changed checking of complete descruction so +strictdestroy is no
[splint.git] / src / Headers / varKinds.h
1 /*
2 ** varKinds.h
3 */
4
5 # ifndef VARKINDSH
6 # define VARKINDSH
7
8 /*
9 ** states of storage
10 */
11
12 typedef enum { 
13   SS_UNKNOWN, 
14   SS_UNUSEABLE, /* cannot use (unallocated pointer reference) */
15   SS_UNDEFINED, /* cannot use value (e.g., unbound variable) */
16   SS_MUNDEFINED,/* maybe undefined */
17   SS_ALLOCATED, /* allocated pointer */
18   SS_PDEFINED,  /* partially defined: must check reachable values */
19   SS_DEFINED,   /* completely defined: can use value and all reachable values */
20   SS_PARTIAL,   /* defined, but can be bashed without error (partial structure returned) */
21   SS_DEAD,      /* cannot use (after giving aways as only) 
22                  * same meaning as UNUSEABLE, except that we 
23                  * want to generate better error messages. */
24   SS_HOFFA,     /* "probably dead" */
25   SS_FIXED,     /* cannot modify */
26   SS_RELDEF,    /* a structure field that may or may not be defined (up to
27                  * programmer to worry about it. */
28
29   SS_UNDEFGLOB,   /* global only: undefined before call */ 
30   SS_KILLED,      /* global only: undefined after call */
31   SS_UNDEFKILLED, /* global only: undefined before and after call */
32
33   SS_SPECIAL,     /* marker for uses/defines/allocates/releases-specified */
34
35   SS_LAST
36 } sstate;
37
38 typedef enum { 
39   SCNONE, 
40   SCEXTERN, 
41   SCSTATIC 
42 } storageClassCode ;
43
44 typedef enum {
45   NS_ERROR = -1,     /* error (suppress messages) */
46   NS_UNKNOWN = 0,    /* no annotation */
47   NS_NOTNULL,        /* definitely not null */
48   NS_MNOTNULL,       /* marked with notnull */
49
50                      /* perhaps null */
51   NS_RELNULL,        /* relaxed null --- okay null for set, not null for checking */
52   NS_CONSTNULL,      /* null constant (for abstract types) */
53   
54   /* don't change the order! */             /* possibly null */
55   NS_POSNULL,        /* possibly null */
56   NS_DEFNULL,        /* definitely null */
57   NS_ABSNULL         /* null from abstract type definition (concrete type unknown) */
58 } nstate;
59
60 extern bool nstate_isKnown (nstate p_n) /*@*/ ;
61 # define nstate_isKnown(n) ((n) != NS_UNKNOWN)
62
63 extern bool nstate_isValid (/*@sef@*/ nstate p_n) /*@*/ ;
64 # define nstate_isValid(n) ((n) >= NS_ERROR && (n) <= NS_ABSNULL)
65
66 /*
67 ** aliasing states
68 */
69
70 /*
71 ** HEY STUPID!  Don't switch around the order!
72 **
73 ** These numbers are fixed into the library format.  If the order
74 ** changes, remember to remake all libraries!
75 */
76
77 typedef enum { 
78   AK_UNKNOWN = 0, /* AK_UNKNOWN must be first */
79   AK_ERROR,
80   AK_ONLY,        
81   AK_IMPONLY,
82   AK_KEEP,
83   AK_KEPT,
84   AK_TEMP,  /* 6 */
85   AK_IMPTEMP,
86   AK_SHARED, 
87   AK_UNIQUE,
88   AK_RETURNED, /* 10 */
89   AK_FRESH,        /* local only storage (may be shared) */
90   AK_STACK,        /* allocated on local stack */
91   AK_REFCOUNTED,
92   AK_REFS,
93   AK_KILLREF,
94   AK_NEWREF,
95   AK_OWNED,
96   AK_DEPENDENT, /* 18 */
97   AK_IMPDEPENDENT,
98   AK_STATIC,
99   AK_LOCAL        /* AK_LOCAL must be last */
100 } alkind;
101
102 typedef enum {
103   XO_UNKNOWN,
104   XO_NORMAL,
105   XO_EXPOSED,
106   XO_OBSERVER
107 } exkind;
108
109 extern bool sstate_isKnown (sstate p_s) /*@*/ ;
110 # define sstate_isKnown(s)      ((s) != SS_UNKNOWN)
111
112 extern bool sstate_isUnknown (sstate p_s) /*@*/ ;
113 # define sstate_isUnknown(s)      ((s) == SS_UNKNOWN)
114
115 extern bool exkind_isUnknown (exkind p_e) /*@*/ ;
116 # define exkind_isUnknown(e)    ((e) == XO_UNKNOWN)
117
118 extern bool exkind_isKnown (/*@sef@*/ exkind p_e) /*@*/ ;
119 # define exkind_isKnown(e)      ((e) != XO_UNKNOWN && (e) != XO_NORMAL)
120
121 extern bool alkind_isValid (/*@sef@*/ alkind p_a) /*@*/ ;
122 # define alkind_isValid(a) ((a) >= AK_UNKNOWN && (a) <= AK_LOCAL)
123
124 extern bool alkind_isImplicit (/*@sef@*/ alkind p_a) /*@*/ ;
125 extern bool alkind_isDependent (/*@sef@*/ alkind p_a) /*@*/ ; 
126 extern bool alkind_isOnly (/*@sef@*/ alkind p_a) /*@*/ ;       
127 extern bool alkind_isTemp (/*@sef@*/ alkind p_a) /*@*/ ;       
128
129 # define alkind_isImplicit(a)   (((a) == AK_IMPONLY || (a) == AK_IMPDEPENDENT \
130                                  || (a) == AK_IMPTEMP))
131 # define alkind_isDependent(a)  (((a) == AK_DEPENDENT || (a) == AK_IMPDEPENDENT))
132 # define alkind_isOnly(a)       ((a) == AK_ONLY || (a) == AK_IMPONLY)
133 # define alkind_isTemp(a)       (((a) == AK_TEMP || (a) == AK_IMPTEMP))
134
135 extern bool alkind_equal (alkind p_a1, alkind p_a2) /*@*/ ;
136
137 extern bool alkind_isOwned (alkind p_a) /*@*/ ;      
138 extern bool alkind_isStack (alkind p_a) /*@*/ ;      
139 extern bool alkind_isStatic (alkind p_a) /*@*/ ;     
140 extern bool alkind_isKeep (alkind p_a) /*@*/ ;       
141 extern bool alkind_isKept (alkind p_a) /*@*/ ;       
142 extern bool alkind_isUnique (alkind p_a) /*@*/ ;     
143 extern bool alkind_isError (alkind p_a) /*@*/ ;      
144 extern bool alkind_isFresh (alkind p_a) /*@*/ ;      
145 extern bool alkind_isShared (alkind p_a) /*@*/ ;     
146 extern bool alkind_isLocal (alkind p_a) /*@*/ ;      
147 extern bool alkind_isKnown (alkind p_a) /*@*/ ;      
148 extern bool alkind_isUnknown (alkind p_a) /*@*/ ;    
149 extern bool alkind_isRefCounted (alkind p_a) /*@*/ ; 
150 extern /*@unused@*/ bool alkind_isRefs (alkind p_a) /*@*/ ;       
151 extern bool alkind_isNewRef (alkind p_a) /*@*/ ;     
152 extern bool alkind_isKillRef (alkind p_a) /*@*/ ;    
153
154 extern alkind alkind_resolve (alkind p_a1, alkind p_a2) /*@*/ ;
155
156 # define alkind_isOwned(a)      ((a) == AK_OWNED)
157 # define alkind_isStack(a)      ((a) == AK_STACK)
158 # define alkind_isStatic(a)     ((a) == AK_STATIC)
159 # define alkind_isKeep(a)       ((a) == AK_KEEP)
160 # define alkind_isKept(a)       ((a) == AK_KEPT)
161 # define alkind_isUnique(a)     ((a) == AK_UNIQUE)
162 # define alkind_isError(a)      ((a) == AK_ERROR)
163 # define alkind_isFresh(a)      ((a) == AK_FRESH)
164 # define alkind_isShared(a)     ((a) == AK_SHARED)
165 # define alkind_isLocal(a)      ((a) == AK_LOCAL)
166 # define alkind_isKnown(a)      ((a) != AK_UNKNOWN)
167 # define alkind_isUnknown(a)    ((a) == AK_UNKNOWN)
168 # define alkind_isRefCounted(a) ((a) == AK_REFCOUNTED)
169 # define alkind_isRefs(a)       ((a) == AK_REFS)
170 # define alkind_isNewRef(a)     ((a) == AK_NEWREF)
171 # define alkind_isKillRef(a)    ((a) == AK_KILLREF)
172
173 extern /*@observer@*/ cstring sstate_unparse (sstate p_s) /*@*/ ;
174
175 extern alkind alkind_fromQual (qual p_q) /*@*/ ;
176 extern alkind alkind_derive (alkind p_outer, alkind p_inner) /*@*/ ;
177 extern /*@observer@*/ cstring alkind_unparse (alkind p_a) /*@*/ ;
178 extern /*@observer@*/ cstring alkind_capName (alkind p_a) /*@*/ ;
179 extern alkind alkind_fromInt (int p_n) /*@*/ ;
180 extern nstate nstate_fromInt (int p_n) /*@*/ ;
181 extern /*@observer@*/ cstring nstate_unparse (nstate p_n) /*@*/ ;
182 extern int nstate_compare (nstate p_n1, nstate p_n2) /*@*/ ;
183 extern bool nstate_possiblyNull (nstate p_n) /*@*/ ;
184 extern bool nstate_perhapsNull (nstate p_n) /*@*/ ;
185 extern sstate sstate_fromInt (int p_n) /*@*/ ;
186 extern exkind exkind_fromInt (int p_n) /*@*/ ;
187 extern exkind exkind_fromQual (qual p_q) /*@*/ ;
188 extern /*@observer@*/ cstring exkind_unparse (exkind p_a) /*@*/ ;
189 extern /*@observer@*/ cstring exkind_capName (exkind p_a) /*@*/ ;
190 extern /*@observer@*/ cstring exkind_unparseError (exkind p_a) /*@*/ ;
191 extern sstate sstate_fromQual (qual p_q) /*@*/ ;
192 extern bool alkind_compatible (alkind p_a1, alkind p_a2) /*@*/ ;
193 extern alkind alkind_fixImplicit (alkind p_a) /*@*/ ;
194
195 typedef enum 
196 {
197   XK_ERROR,
198   XK_UNKNOWN,      
199   XK_NEVERESCAPE,
200   XK_GOTO,
201   XK_MAYGOTO,
202   XK_MAYEXIT,
203   XK_MUSTEXIT,
204   XK_TRUEEXIT,
205   XK_FALSEEXIT,
206   XK_MUSTRETURN,
207   XK_MAYRETURN,
208   XK_MAYRETURNEXIT,
209   XK_MUSTRETURNEXIT /* must return or exit */
210 } exitkind;
211
212 /*@constant exitkind XK_LAST; @*/
213 # define XK_LAST XK_MUSTRETURNEXIT
214
215 extern exitkind exitkind_fromQual (qual p_q) /*@*/ ;
216 extern /*@unused@*/ bool exitkind_isMustExit (exitkind p_e) /*@*/ ;
217 # define exitkind_isMustExit(e) ((e) == XK_MUSTEXIT)
218
219 extern bool exitkind_equal (exitkind p_e1, exitkind p_e2) /*@*/ ;
220 # define exitkind_equal(e1,e2) ((e1) == (e2))
221
222 extern bool exitkind_couldExit (exitkind p_e) /*@*/ ;
223 extern bool exitkind_couldEscape (exitkind p_e) /*@*/ ;
224 extern exitkind exitkind_fromInt (int p_x) /*@*/ ;
225 extern /*@observer@*/ cstring exitkind_unparse (exitkind p_k) /*@*/ ;
226
227 extern bool exitkind_isKnown (exitkind p_e) /*@*/ ;
228 # define exitkind_isKnown(e) ((e) != XK_UNKNOWN)
229
230 extern bool exitkind_isTrueExit (exitkind p_e) /*@*/ ;
231 # define exitkind_isTrueExit(e) \
232   ((e) == XK_TRUEEXIT)
233
234 extern bool exitkind_isConditionalExit (/*@sef@*/ exitkind p_e) /*@*/ ;
235 # define exitkind_isConditionalExit(e) \
236   ((e) == XK_TRUEEXIT || (e) == XK_FALSEEXIT)
237
238 extern bool exitkind_isError (/*@sef@*/ exitkind p_e) /*@*/ ;
239 # define exitkind_isError(e) ((e) == XK_ERROR)
240
241 extern bool exitkind_mustExit (/*@sef@*/ exitkind p_e) /*@*/ ;
242 # define exitkind_mustExit(e) ((e) == XK_MUSTEXIT)
243
244 extern bool exitkind_mustEscape (/*@sef@*/ exitkind p_e) /*@*/ ;
245 # define exitkind_mustEscape(e) \
246   ((e) == XK_MUSTEXIT || (e) == XK_MUSTRETURN \
247    || (e) == XK_MUSTRETURNEXIT || (e) == XK_GOTO)
248
249 extern exitkind exitkind_makeConditional (exitkind p_k) /*@*/ ;
250 extern exitkind exitkind_combine (exitkind p_k1, exitkind p_k2) /*@*/ ;
251
252 /*
253 ** NOTE: combiners are in sRef
254 */
255
256 # else
257 # error "Multiple include"
258 # endif
This page took 0.095928 seconds and 5 git commands to generate.