]> andersk Git - splint.git/blame - src/Headers/varKinds.h
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
Changed checking of complete descruction so +strictdestroy is no
[splint.git] / src / Headers / varKinds.h
CommitLineData
885824d3 1/*
2** varKinds.h
3*/
4
5# ifndef VARKINDSH
6# define VARKINDSH
7
8/*
9** states of storage
10*/
11
12typedef 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
38typedef enum {
39 SCNONE,
40 SCEXTERN,
41 SCSTATIC
42} storageClassCode ;
43
28bf4b0b 44typedef enum {
885824d3 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
60extern bool nstate_isKnown (nstate p_n) /*@*/ ;
61# define nstate_isKnown(n) ((n) != NS_UNKNOWN)
62
28bf4b0b 63extern bool nstate_isValid (/*@sef@*/ nstate p_n) /*@*/ ;
64# define nstate_isValid(n) ((n) >= NS_ERROR && (n) <= NS_ABSNULL)
65
885824d3 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
77typedef 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,
28bf4b0b 84 AK_TEMP, /* 6 */
885824d3 85 AK_IMPTEMP,
86 AK_SHARED,
87 AK_UNIQUE,
28bf4b0b 88 AK_RETURNED, /* 10 */
885824d3 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,
28bf4b0b 96 AK_DEPENDENT, /* 18 */
885824d3 97 AK_IMPDEPENDENT,
98 AK_STATIC,
99 AK_LOCAL /* AK_LOCAL must be last */
100} alkind;
101
102typedef enum {
103 XO_UNKNOWN,
104 XO_NORMAL,
105 XO_EXPOSED,
106 XO_OBSERVER
107} exkind;
108
109extern bool sstate_isKnown (sstate p_s) /*@*/ ;
110# define sstate_isKnown(s) ((s) != SS_UNKNOWN)
111
112extern bool sstate_isUnknown (sstate p_s) /*@*/ ;
113# define sstate_isUnknown(s) ((s) == SS_UNKNOWN)
114
115extern bool exkind_isUnknown (exkind p_e) /*@*/ ;
116# define exkind_isUnknown(e) ((e) == XO_UNKNOWN)
117
118extern bool exkind_isKnown (/*@sef@*/ exkind p_e) /*@*/ ;
119# define exkind_isKnown(e) ((e) != XO_UNKNOWN && (e) != XO_NORMAL)
120
28bf4b0b 121extern bool alkind_isValid (/*@sef@*/ alkind p_a) /*@*/ ;
122# define alkind_isValid(a) ((a) >= AK_UNKNOWN && (a) <= AK_LOCAL)
123
885824d3 124extern bool alkind_isImplicit (/*@sef@*/ alkind p_a) /*@*/ ;
125extern bool alkind_isDependent (/*@sef@*/ alkind p_a) /*@*/ ;
126extern bool alkind_isOnly (/*@sef@*/ alkind p_a) /*@*/ ;
127extern 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
135extern bool alkind_equal (alkind p_a1, alkind p_a2) /*@*/ ;
136
137extern bool alkind_isOwned (alkind p_a) /*@*/ ;
138extern bool alkind_isStack (alkind p_a) /*@*/ ;
139extern bool alkind_isStatic (alkind p_a) /*@*/ ;
140extern bool alkind_isKeep (alkind p_a) /*@*/ ;
141extern bool alkind_isKept (alkind p_a) /*@*/ ;
142extern bool alkind_isUnique (alkind p_a) /*@*/ ;
143extern bool alkind_isError (alkind p_a) /*@*/ ;
144extern bool alkind_isFresh (alkind p_a) /*@*/ ;
145extern bool alkind_isShared (alkind p_a) /*@*/ ;
146extern bool alkind_isLocal (alkind p_a) /*@*/ ;
147extern bool alkind_isKnown (alkind p_a) /*@*/ ;
148extern bool alkind_isUnknown (alkind p_a) /*@*/ ;
149extern bool alkind_isRefCounted (alkind p_a) /*@*/ ;
150extern /*@unused@*/ bool alkind_isRefs (alkind p_a) /*@*/ ;
151extern bool alkind_isNewRef (alkind p_a) /*@*/ ;
152extern bool alkind_isKillRef (alkind p_a) /*@*/ ;
153
2e127cb8 154extern alkind alkind_resolve (alkind p_a1, alkind p_a2) /*@*/ ;
155
885824d3 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
173extern /*@observer@*/ cstring sstate_unparse (sstate p_s) /*@*/ ;
174
175extern alkind alkind_fromQual (qual p_q) /*@*/ ;
176extern alkind alkind_derive (alkind p_outer, alkind p_inner) /*@*/ ;
177extern /*@observer@*/ cstring alkind_unparse (alkind p_a) /*@*/ ;
178extern /*@observer@*/ cstring alkind_capName (alkind p_a) /*@*/ ;
179extern alkind alkind_fromInt (int p_n) /*@*/ ;
180extern nstate nstate_fromInt (int p_n) /*@*/ ;
181extern /*@observer@*/ cstring nstate_unparse (nstate p_n) /*@*/ ;
182extern int nstate_compare (nstate p_n1, nstate p_n2) /*@*/ ;
183extern bool nstate_possiblyNull (nstate p_n) /*@*/ ;
184extern bool nstate_perhapsNull (nstate p_n) /*@*/ ;
185extern sstate sstate_fromInt (int p_n) /*@*/ ;
186extern exkind exkind_fromInt (int p_n) /*@*/ ;
187extern exkind exkind_fromQual (qual p_q) /*@*/ ;
188extern /*@observer@*/ cstring exkind_unparse (exkind p_a) /*@*/ ;
189extern /*@observer@*/ cstring exkind_capName (exkind p_a) /*@*/ ;
190extern /*@observer@*/ cstring exkind_unparseError (exkind p_a) /*@*/ ;
191extern sstate sstate_fromQual (qual p_q) /*@*/ ;
192extern bool alkind_compatible (alkind p_a1, alkind p_a2) /*@*/ ;
193extern alkind alkind_fixImplicit (alkind p_a) /*@*/ ;
194
28bf4b0b 195typedef enum
885824d3 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
215extern exitkind exitkind_fromQual (qual p_q) /*@*/ ;
216extern /*@unused@*/ bool exitkind_isMustExit (exitkind p_e) /*@*/ ;
217# define exitkind_isMustExit(e) ((e) == XK_MUSTEXIT)
218
219extern bool exitkind_equal (exitkind p_e1, exitkind p_e2) /*@*/ ;
220# define exitkind_equal(e1,e2) ((e1) == (e2))
221
222extern bool exitkind_couldExit (exitkind p_e) /*@*/ ;
223extern bool exitkind_couldEscape (exitkind p_e) /*@*/ ;
224extern exitkind exitkind_fromInt (int p_x) /*@*/ ;
225extern /*@observer@*/ cstring exitkind_unparse (exitkind p_k) /*@*/ ;
226
227extern bool exitkind_isKnown (exitkind p_e) /*@*/ ;
228# define exitkind_isKnown(e) ((e) != XK_UNKNOWN)
229
230extern bool exitkind_isTrueExit (exitkind p_e) /*@*/ ;
231# define exitkind_isTrueExit(e) \
232 ((e) == XK_TRUEEXIT)
233
234extern bool exitkind_isConditionalExit (/*@sef@*/ exitkind p_e) /*@*/ ;
235# define exitkind_isConditionalExit(e) \
236 ((e) == XK_TRUEEXIT || (e) == XK_FALSEEXIT)
237
238extern bool exitkind_isError (/*@sef@*/ exitkind p_e) /*@*/ ;
239# define exitkind_isError(e) ((e) == XK_ERROR)
240
241extern bool exitkind_mustExit (/*@sef@*/ exitkind p_e) /*@*/ ;
242# define exitkind_mustExit(e) ((e) == XK_MUSTEXIT)
243
244extern 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
249extern exitkind exitkind_makeConditional (exitkind p_k) /*@*/ ;
250extern 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
git-cvsimport mirror of splint
This page took 0.104573 seconds and 5 git commands to generate.