]>
Commit | Line | Data |
---|---|---|
616915dd | 1 | /* |
11db3170 | 2 | ** Splint - annotation-assisted static program checker |
c59f5181 | 3 | ** Copyright (C) 1994-2003 University of Virginia, |
616915dd | 4 | ** Massachusetts Institute of Technology |
5 | ** | |
6 | ** This program is free software; you can redistribute it and/or modify it | |
7 | ** under the terms of the GNU General Public License as published by the | |
8 | ** Free Software Foundation; either version 2 of the License, or (at your | |
9 | ** option) any later version. | |
10 | ** | |
11 | ** This program is distributed in the hope that it will be useful, but | |
12 | ** WITHOUT ANY WARRANTY; without even the implied warranty of | |
13 | ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU | |
14 | ** General Public License for more details. | |
15 | ** | |
16 | ** The GNU General Public License is available from http://www.gnu.org/ or | |
17 | ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, | |
18 | ** MA 02111-1307, USA. | |
19 | ** | |
155af98d | 20 | ** For information on splint: info@splint.org |
21 | ** To report a bug: splint-bug@splint.org | |
11db3170 | 22 | ** For more information: http://www.splint.org |
616915dd | 23 | */ |
24 | /* | |
25 | ** guardSet.c | |
26 | ** | |
27 | ** if x is in true guards, then x is not null on this branch, | |
28 | ** and x is "probably" null on the other branch. | |
29 | ** if x is in false guards, then x is "probably" null on this branch, | |
30 | ** and x is not null on the other branch. | |
31 | ** | |
32 | ** Either guards is obsolete and should be removed soon. | |
33 | */ | |
34 | ||
1b8ae690 | 35 | # include "splintMacros.nf" |
616915dd | 36 | # include "basic.h" |
37 | ||
38 | guardSet guardSet_new () | |
39 | { | |
40 | return guardSet_undefined; | |
41 | } | |
42 | ||
43 | static /*@notnull@*/ /*@special@*/ guardSet guardSet_newEmpty (void) | |
44 | /*@defines result@*/ | |
45 | /*@post:isnull result->tguard, result->fguard@*/ | |
46 | { | |
47 | guardSet g = (guardSet) dmalloc (sizeof (*g)); | |
48 | ||
49 | g->tguard = sRefSet_undefined; | |
50 | g->fguard = sRefSet_undefined; | |
51 | ||
52 | return g; | |
53 | } | |
54 | ||
55 | sRefSet guardSet_getTrueGuards (guardSet g) | |
56 | { | |
57 | ||
58 | if (guardSet_isDefined (g)) | |
59 | { | |
60 | return (g->tguard); | |
61 | } | |
62 | else | |
63 | { | |
64 | return (sRefSet_undefined); | |
65 | } | |
66 | } | |
67 | ||
68 | void guardSet_delete (guardSet g, sRef s) | |
69 | { | |
70 | bool res; | |
71 | llassert (guardSet_isDefined (g)); | |
72 | res = sRefSet_delete (g->tguard, s); | |
73 | ||
74 | /* | |
75 | ** This assertion is no longer always true: | |
76 | ** llassert (res); | |
77 | */ | |
78 | } | |
79 | ||
80 | /*@dependent@*/ /*@exposed@*/ sRefSet guardSet_getFalseGuards (guardSet g) | |
81 | { | |
82 | if (guardSet_isDefined (g)) | |
83 | { | |
84 | return (g->fguard); | |
85 | } | |
86 | else | |
87 | { | |
88 | return (sRefSet_undefined); | |
89 | } | |
90 | } | |
91 | ||
92 | guardSet guardSet_or (/*@returned@*/ /*@unique@*/ guardSet s, guardSet t) | |
93 | { | |
94 | ||
95 | llassert (NOALIAS (s, t)); | |
96 | ||
97 | if (s == guardSet_undefined) | |
98 | { | |
99 | if (t == guardSet_undefined) | |
100 | { | |
101 | return s; | |
102 | } | |
103 | ||
104 | s = guardSet_newEmpty (); | |
105 | } | |
106 | ||
107 | if (t == guardSet_undefined) | |
108 | { | |
109 | sRefSet_free (s->tguard); | |
110 | s->tguard = sRefSet_new (); | |
111 | } | |
112 | else | |
113 | { | |
114 | sRefSet last; | |
115 | ||
116 | s->tguard = sRefSet_intersect (last = s->tguard, t->tguard); | |
117 | sRefSet_free (last); | |
118 | s->fguard = sRefSet_union (s->fguard, t->fguard); | |
119 | } | |
120 | ||
121 | ||
122 | return s; | |
123 | } | |
124 | ||
125 | guardSet guardSet_and (/*@returned@*/ /*@unique@*/ guardSet s, guardSet t) | |
126 | { | |
127 | llassert (NOALIAS (s, t)); | |
128 | ||
129 | if (s == guardSet_undefined) | |
130 | { | |
131 | if (t == guardSet_undefined) | |
132 | { | |
133 | return s; | |
134 | } | |
135 | ||
136 | s = guardSet_newEmpty (); | |
137 | } | |
138 | ||
139 | if (t == guardSet_undefined) | |
140 | { | |
141 | sRefSet_free (s->fguard); | |
142 | s->fguard = sRefSet_new (); | |
143 | } | |
144 | else | |
145 | { | |
146 | sRefSet last; | |
147 | ||
148 | s->tguard = sRefSet_union (s->tguard, t->tguard); | |
149 | ||
150 | s->fguard = sRefSet_intersect (last = s->fguard, t->fguard); | |
151 | sRefSet_free (last); | |
152 | } | |
153 | ||
154 | return s; | |
155 | } | |
156 | ||
157 | /*@only@*/ guardSet guardSet_union (/*@only@*/ guardSet s, guardSet t) | |
158 | { | |
159 | if (t == guardSet_undefined) return s; | |
160 | ||
161 | llassert (NOALIAS (s, t)); | |
162 | ||
163 | if (guardSet_isDefined (s)) | |
164 | { | |
165 | s->tguard = sRefSet_union (s->tguard, t->tguard); | |
166 | s->fguard = sRefSet_union (s->fguard, t->fguard); | |
167 | } | |
168 | else | |
169 | { | |
170 | s = guardSet_newEmpty (); | |
171 | ||
172 | s->tguard = sRefSet_newCopy (t->tguard); | |
173 | s->fguard = sRefSet_newCopy (t->fguard); | |
174 | } | |
175 | ||
176 | return s; | |
177 | } | |
178 | ||
179 | guardSet guardSet_levelUnion (/*@only@*/ guardSet s, guardSet t, int lexlevel) | |
180 | { | |
181 | if (t == guardSet_undefined) return s; | |
182 | ||
183 | llassert (NOALIAS (s, t)); | |
184 | ||
185 | if (guardSet_isDefined (s)) | |
186 | { | |
187 | s->tguard = sRefSet_levelUnion (s->tguard, t->tguard, lexlevel); | |
188 | s->fguard = sRefSet_levelUnion (s->fguard, t->fguard, lexlevel); | |
189 | } | |
190 | else | |
191 | { | |
192 | s = guardSet_newEmpty (); | |
193 | ||
194 | /* should be necessary! */ | |
195 | ||
196 | sRefSet_free (s->tguard); | |
197 | sRefSet_free (s->fguard); | |
198 | ||
199 | s->tguard = sRefSet_levelCopy (t->tguard, lexlevel); | |
200 | s->fguard = sRefSet_levelCopy (t->fguard, lexlevel); | |
201 | } | |
202 | ||
203 | return s; | |
204 | } | |
205 | ||
206 | guardSet | |
207 | guardSet_levelUnionFree (/*@returned@*/ /*@unique@*/ guardSet s, | |
208 | /*@only@*/ guardSet t, int lexlevel) | |
209 | { | |
210 | if (t == guardSet_undefined) return s; | |
211 | ||
212 | if (guardSet_isDefined (s)) | |
213 | { | |
214 | s->tguard = sRefSet_levelUnion (s->tguard, t->tguard, lexlevel); | |
215 | s->fguard = sRefSet_levelUnion (s->fguard, t->fguard, lexlevel); | |
216 | } | |
217 | else | |
218 | { | |
219 | s = guardSet_newEmpty (); | |
220 | ||
221 | /* should be necessary! */ | |
222 | ||
223 | sRefSet_free (s->tguard); | |
224 | sRefSet_free (s->fguard); | |
225 | ||
226 | s->tguard = sRefSet_levelCopy (t->tguard, lexlevel); | |
227 | s->fguard = sRefSet_levelCopy (t->fguard, lexlevel); | |
228 | } | |
229 | ||
230 | guardSet_free (t); | |
231 | return s; | |
232 | } | |
233 | ||
234 | void guardSet_flip (guardSet g) | |
235 | { | |
236 | if (g != guardSet_undefined) | |
237 | { | |
238 | sRefSet tmp = g->tguard; | |
239 | ||
240 | g->tguard = g->fguard; | |
241 | g->fguard = tmp; | |
242 | } | |
243 | } | |
244 | ||
245 | /*@only@*/ guardSet guardSet_invert (/*@temp@*/ guardSet g) | |
246 | { | |
247 | if (g != guardSet_undefined) | |
248 | { | |
249 | guardSet ret = guardSet_newEmpty (); | |
250 | ||
251 | ret->tguard = sRefSet_newCopy (g->fguard); | |
252 | ret->fguard = sRefSet_newCopy (g->tguard); | |
253 | ||
254 | return ret; | |
255 | } | |
256 | return guardSet_undefined; | |
257 | } | |
258 | ||
259 | /*@only@*/ guardSet guardSet_copy (/*@temp@*/ guardSet g) | |
260 | { | |
261 | if (g != guardSet_undefined) | |
262 | { | |
263 | guardSet ret = guardSet_newEmpty (); | |
264 | ||
265 | ret->tguard = sRefSet_newCopy (g->tguard); | |
266 | ret->fguard = sRefSet_newCopy (g->fguard); | |
267 | ||
268 | return ret; | |
269 | } | |
270 | return guardSet_undefined; | |
271 | } | |
272 | ||
28bf4b0b | 273 | guardSet guardSet_addTrueGuard (/*@returned@*/ guardSet g, /*@exposed@*/ sRef s) |
616915dd | 274 | { |
275 | if (sRef_isMeaningful (s)) | |
276 | { | |
277 | if (g == guardSet_undefined) | |
278 | { | |
279 | g = guardSet_newEmpty (); | |
280 | } | |
281 | ||
282 | g->tguard = sRefSet_insert (g->tguard, s); | |
283 | } | |
284 | ||
285 | return g; | |
286 | } | |
287 | ||
28bf4b0b | 288 | guardSet guardSet_addFalseGuard (/*@returned@*/ guardSet g, /*@exposed@*/ sRef s) |
616915dd | 289 | { |
290 | if (sRef_isMeaningful (s)) | |
291 | { | |
292 | if (g == guardSet_undefined) | |
293 | { | |
294 | g = guardSet_newEmpty (); | |
295 | } | |
296 | ||
297 | g->fguard = sRefSet_insert (g->fguard, s); | |
298 | } | |
299 | ||
300 | return g; | |
301 | } | |
302 | ||
303 | /*@only@*/ cstring guardSet_unparse (guardSet g) | |
304 | { | |
305 | if (g == guardSet_undefined) | |
306 | { | |
307 | return (cstring_makeLiteral ("<no guards>")); | |
308 | } | |
309 | else | |
310 | { | |
311 | return (message ("not null: %q / prob null: %q", | |
312 | sRefSet_unparseDebug (g->tguard), | |
313 | sRefSet_unparseDebug (g->fguard))); | |
314 | } | |
315 | } | |
316 | ||
317 | void guardSet_free (/*@only@*/ guardSet g) | |
318 | { | |
319 | if (g == guardSet_undefined) return; | |
320 | ||
321 | sRefSet_free (g->tguard); | |
322 | sRefSet_free (g->fguard); | |
323 | ||
324 | sfree (g); | |
325 | } | |
326 | ||
327 | bool | |
328 | guardSet_isGuarded (guardSet g, sRef s) | |
329 | { | |
330 | if (g == guardSet_undefined) return FALSE; | |
331 | ||
332 | return (sRefSet_member (g->tguard, s)); | |
333 | } | |
334 | ||
335 | bool | |
28bf4b0b | 336 | guardSet_mustBeNull (guardSet g, sRef s) |
616915dd | 337 | { |
338 | bool ret; | |
339 | ||
340 | if (g == guardSet_undefined) return FALSE; | |
341 | ||
342 | ret = sRefSet_member (g->fguard, s); | |
343 | return ret; | |
344 | } | |
345 | ||
346 | bool guardSet_isEmpty (guardSet g) | |
347 | { | |
348 | if (guardSet_isDefined (g)) | |
349 | { | |
350 | return (sRefSet_isEmpty (g->tguard) && sRefSet_isEmpty (g->fguard)); | |
351 | } | |
352 | else | |
353 | { | |
354 | return TRUE; | |
355 | } | |
356 | } |