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
28 # include "splintMacros.nf"
31 /*@constant int TISTABLEBASESIZE;@*/
32 # define TISTABLEBASESIZE LARGEBASESIZE
34 static int tistableentries = 0;
35 static int tistablefree = 0;
36 typedef /*@only@*/ usymIdSet o_usymIdSet;
37 static /*@only@*/ o_usymIdSet *tistable;
38 static void tistable_addDirectEntry (/*@only@*/ usymIdSet p_s)
39 /*@modifies tistable, tistableentries, tistablefree@*/;
41 void typeIdSet_initMod (void)
42 /*@globals undef tistable;@*/
43 /*@modifies tistable, tistablefree;@*/
45 llassert (tistableentries == 0 && tistablefree == 0);
47 tistablefree = TISTABLEBASESIZE;
48 tistable = (usymIdSet *) dmalloc (sizeof (tistable) * tistablefree);
49 tistable[0] = usymIdSet_undefined;
54 void typeIdSet_destroyMod (void)
55 /*@globals killed tistable, tistableentries@*/
59 for (i = 0; i < tistableentries; i++)
61 usymIdSet_free (tistable[i]);
68 void typeIdSet_dumpTable (FILE *fout)
73 ** Don't dump 0th entry
76 for (i = 1; i < tistableentries; i++)
78 cstring s = usymIdSet_dump (tistable[i]);
80 fprintf (fout, "%s\n", cstring_toCharsSafe (s));
86 static /*@unused@*/ void tistable_printOut (void)
91 ** Don't dump 0th entry
94 for (i = 1; i < tistableentries; i++)
96 cstring s = usymIdSet_unparse (tistable[i]);
98 fprintf (g_warningstream, "%d: %s\n", i, cstring_toCharsSafe (s));
104 void typeIdSet_loadTable (FILE *fin)
106 char *s = mstring_create (MAX_DUMP_LINE_LENGTH);
109 llassert (tistableentries == 1);
111 s = reader_readLine (fin, s, MAX_DUMP_LINE_LENGTH);
113 while (s != NULL && *s != ';')
115 usymIdSet u = usymIdSet_undump (&s);
117 llassert (*s == '\0' || *s == '\n');
119 tistable_addDirectEntry (u);
120 s = reader_readLine (fin, os, MAX_DUMP_LINE_LENGTH);
126 static void tistable_grow (void)
128 o_usymIdSet *oldtable = tistable;
129 int newsize = tistableentries + TISTABLEBASESIZE;
132 llassert (tistablefree == 0);
134 tistable = (usymIdSet *) dmalloc (sizeof (tistable) * newsize);
136 for (i = 0; i < tistableentries; i++)
138 tistable[i] = oldtable[i];
141 tistablefree = TISTABLEBASESIZE;
145 static void tistable_addDirectEntry (/*@only@*/ usymIdSet s)
147 if (tistablefree == 0)
152 tistable[tistableentries] = s;
157 static int tistable_addEntry (/*@only@*/ usymIdSet s)
162 for (i = 0; i < tistableentries; i++)
164 if (usymIdSet_compare (tistable[i], s) == 0)
166 /*@access usymIdSet@*/
167 llassert (i == 0 || s != tistable[i]);
168 /*@noaccess usymIdSet@*/
175 tistable_addDirectEntry (s);
176 return (tistableentries - 1);
179 static /*@observer@*/ usymIdSet tistable_fetch (typeIdSet t)
180 /*@globals tistableentries, tistable@*/
181 /*@modifies nothing;@*/
183 llassert (t >= 0 && t < tistableentries);
188 typeIdSet typeIdSet_emptySet (void)
190 if (tistableentries == 0)
192 int val = tistable_addEntry (usymIdSet_new ());
197 llassert (usymIdSet_isUndefined (tistable[0]));
201 bool typeIdSet_member (typeIdSet t, typeId el)
203 usymIdSet u = tistable_fetch (t);
205 return usymIdSet_member (u, el);
208 bool typeIdSet_isEmpty (typeIdSet t)
213 typeIdSet typeIdSet_single (typeId t)
215 return (tistable_addEntry (usymIdSet_single (t)));
218 typeIdSet typeIdSet_singleOpt (typeId t)
220 if (typeId_isValid (t))
222 return (tistable_addEntry (usymIdSet_single (t)));
226 return typeIdSet_empty;
230 typeIdSet typeIdSet_insert (typeIdSet t, typeId el)
232 usymIdSet u = tistable_fetch (t);
234 if (usymIdSet_member (u, el))
240 return (tistable_addEntry (usymIdSet_add (u, el)));
244 typeIdSet typeIdSet_removeFresh (typeIdSet t, typeId el)
246 return (tistable_addEntry (usymIdSet_removeFresh (tistable_fetch (t), el)));
249 cstring typeIdSet_unparse (typeIdSet t)
251 return (usymIdSet_unparse (tistable_fetch (t)));
254 int typeIdSet_compare (typeIdSet t1, typeIdSet t2)
256 return (int_compare (t1, t2));
259 typeIdSet typeIdSet_subtract (typeIdSet s, typeIdSet t)
261 if (typeIdSet_isEmpty (t))
267 return (tistable_addEntry (usymIdSet_subtract (tistable_fetch (s),
268 tistable_fetch (t))));
272 cstring typeIdSet_dump (typeIdSet t)
274 return (message ("%d", t));
277 typeIdSet typeIdSet_undump (char **s)
282 i = reader_getInt (s);
284 llassert (i >= 0 && i < tistableentries);
285 return (typeIdSet) i;
288 typeIdSet typeIdSet_union (typeIdSet t1, typeIdSet t2)
290 if (t1 == typeIdSet_undefined)
294 else if (t2 == typeIdSet_undefined)
300 return (tistable_addEntry (usymIdSet_newUnion (tistable_fetch (t1),
301 tistable_fetch (t2))));