2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 University of Virginia,
4 ** Massachusetts Institute of Technology
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.
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.
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.
20 ** For information on splint: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
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.
32 ** Either guards is obsolete and should be removed soon.
35 # include "splintMacros.nf"
38 guardSet guardSet_new ()
40 return guardSet_undefined;
43 static /*@notnull@*/ /*@special@*/ guardSet guardSet_newEmpty (void)
45 /*@post:isnull result->tguard, result->fguard@*/
47 guardSet g = (guardSet) dmalloc (sizeof (*g));
49 g->tguard = sRefSet_undefined;
50 g->fguard = sRefSet_undefined;
55 sRefSet guardSet_getTrueGuards (guardSet g)
58 if (guardSet_isDefined (g))
64 return (sRefSet_undefined);
68 void guardSet_delete (guardSet g, sRef s)
71 llassert (guardSet_isDefined (g));
72 res = sRefSet_delete (g->tguard, s);
75 ** This assertion is no longer always true:
80 /*@dependent@*/ /*@exposed@*/ sRefSet guardSet_getFalseGuards (guardSet g)
82 if (guardSet_isDefined (g))
88 return (sRefSet_undefined);
92 guardSet guardSet_or (/*@returned@*/ /*@unique@*/ guardSet s, guardSet t)
95 llassert (NOALIAS (s, t));
97 if (s == guardSet_undefined)
99 if (t == guardSet_undefined)
104 s = guardSet_newEmpty ();
107 if (t == guardSet_undefined)
109 sRefSet_free (s->tguard);
110 s->tguard = sRefSet_new ();
116 s->tguard = sRefSet_intersect (last = s->tguard, t->tguard);
118 s->fguard = sRefSet_union (s->fguard, t->fguard);
125 guardSet guardSet_and (/*@returned@*/ /*@unique@*/ guardSet s, guardSet t)
127 llassert (NOALIAS (s, t));
129 if (s == guardSet_undefined)
131 if (t == guardSet_undefined)
136 s = guardSet_newEmpty ();
139 if (t == guardSet_undefined)
141 sRefSet_free (s->fguard);
142 s->fguard = sRefSet_new ();
148 s->tguard = sRefSet_union (s->tguard, t->tguard);
150 s->fguard = sRefSet_intersect (last = s->fguard, t->fguard);
157 /*@only@*/ guardSet guardSet_union (/*@only@*/ guardSet s, guardSet t)
159 if (t == guardSet_undefined) return s;
161 llassert (NOALIAS (s, t));
163 if (guardSet_isDefined (s))
165 s->tguard = sRefSet_union (s->tguard, t->tguard);
166 s->fguard = sRefSet_union (s->fguard, t->fguard);
170 s = guardSet_newEmpty ();
172 s->tguard = sRefSet_newCopy (t->tguard);
173 s->fguard = sRefSet_newCopy (t->fguard);
179 guardSet guardSet_levelUnion (/*@only@*/ guardSet s, guardSet t, int lexlevel)
181 if (t == guardSet_undefined) return s;
183 llassert (NOALIAS (s, t));
185 if (guardSet_isDefined (s))
187 s->tguard = sRefSet_levelUnion (s->tguard, t->tguard, lexlevel);
188 s->fguard = sRefSet_levelUnion (s->fguard, t->fguard, lexlevel);
192 s = guardSet_newEmpty ();
194 /* should be necessary! */
196 sRefSet_free (s->tguard);
197 sRefSet_free (s->fguard);
199 s->tguard = sRefSet_levelCopy (t->tguard, lexlevel);
200 s->fguard = sRefSet_levelCopy (t->fguard, lexlevel);
207 guardSet_levelUnionFree (/*@returned@*/ /*@unique@*/ guardSet s,
208 /*@only@*/ guardSet t, int lexlevel)
210 if (t == guardSet_undefined) return s;
212 if (guardSet_isDefined (s))
214 s->tguard = sRefSet_levelUnion (s->tguard, t->tguard, lexlevel);
215 s->fguard = sRefSet_levelUnion (s->fguard, t->fguard, lexlevel);
219 s = guardSet_newEmpty ();
221 /* should be necessary! */
223 sRefSet_free (s->tguard);
224 sRefSet_free (s->fguard);
226 s->tguard = sRefSet_levelCopy (t->tguard, lexlevel);
227 s->fguard = sRefSet_levelCopy (t->fguard, lexlevel);
234 void guardSet_flip (guardSet g)
236 if (g != guardSet_undefined)
238 sRefSet tmp = g->tguard;
240 g->tguard = g->fguard;
245 /*@only@*/ guardSet guardSet_invert (/*@temp@*/ guardSet g)
247 if (g != guardSet_undefined)
249 guardSet ret = guardSet_newEmpty ();
251 ret->tguard = sRefSet_newCopy (g->fguard);
252 ret->fguard = sRefSet_newCopy (g->tguard);
256 return guardSet_undefined;
259 /*@only@*/ guardSet guardSet_copy (/*@temp@*/ guardSet g)
261 if (g != guardSet_undefined)
263 guardSet ret = guardSet_newEmpty ();
265 ret->tguard = sRefSet_newCopy (g->tguard);
266 ret->fguard = sRefSet_newCopy (g->fguard);
270 return guardSet_undefined;
273 guardSet guardSet_addTrueGuard (/*@returned@*/ guardSet g, /*@exposed@*/ sRef s)
275 if (sRef_isMeaningful (s))
277 if (g == guardSet_undefined)
279 g = guardSet_newEmpty ();
282 g->tguard = sRefSet_insert (g->tguard, s);
288 guardSet guardSet_addFalseGuard (/*@returned@*/ guardSet g, /*@exposed@*/ sRef s)
290 if (sRef_isMeaningful (s))
292 if (g == guardSet_undefined)
294 g = guardSet_newEmpty ();
297 g->fguard = sRefSet_insert (g->fguard, s);
303 /*@only@*/ cstring guardSet_unparse (guardSet g)
305 if (g == guardSet_undefined)
307 return (cstring_makeLiteral ("<no guards>"));
311 return (message ("not null: %q / prob null: %q",
312 sRefSet_unparseDebug (g->tguard),
313 sRefSet_unparseDebug (g->fguard)));
317 void guardSet_free (/*@only@*/ guardSet g)
319 if (g == guardSet_undefined) return;
321 sRefSet_free (g->tguard);
322 sRefSet_free (g->fguard);
328 guardSet_isGuarded (guardSet g, sRef s)
330 if (g == guardSet_undefined) return FALSE;
332 return (sRefSet_member (g->tguard, s));
336 guardSet_mustBeNull (guardSet g, sRef s)
340 if (g == guardSet_undefined) return FALSE;
342 ret = sRefSet_member (g->fguard, s);
346 bool guardSet_isEmpty (guardSet g)
348 if (guardSet_isDefined (g))
350 return (sRefSet_isEmpty (g->tguard) && sRefSet_isEmpty (g->fguard));