2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 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 ** NOTE: This is not a stand-alone source file, but is included in ctype.c.
28 ** (This is necessary becuase there is no other way in C to have a
29 ** hidden scope, besides at the file level.)
35 ** type definitions and forward declarations in ctbase.i
39 ctentry_free (/*@only@*/ ctentry c)
41 ctbase_free (c->ctbase);
42 cstring_free (c->unparse);
46 static void cttable_reset (void)
50 if (cttab.entries != NULL)
54 for (i = 0; i < cttab.size; i++)
56 /*drl bee: si*/ ctentry_free (cttab.entries[i]);
60 sfree (cttab.entries);
71 ctentry_makeNew (ctkind ctk, /*@only@*/ ctbase c)
74 return (ctentry_make (ctk, c, ctype_dne, ctype_dne, ctype_dne, cstring_undefined));
77 static /*@only@*/ ctentry
78 ctentry_make (ctkind ctk,
79 /*@keep@*/ ctbase c, ctype base,
80 ctype ptr, ctype array,
81 /*@keep@*/ cstring unparse) /*@*/
83 ctentry cte = (ctentry) dmalloc (sizeof (*cte));
89 cte->unparse = unparse;
94 ctentry_unparse (ctentry c)
97 ("%20s [%d] [%d] [%d]",
98 (cstring_isDefined (c->unparse) ? c->unparse : cstring_makeLiteral ("<no name>")),
105 ctentry_isInteresting (ctentry c)
107 return (cstring_isNonEmpty (c->unparse));
110 static /*@only@*/ cstring
111 ctentry_dump (ctentry c)
113 DPRINTF (("Dumping: %s", ctentry_unparse (c)));
115 if (c->ptr == ctype_dne
116 && c->array == ctype_dne
117 && c->base == ctype_dne)
119 return (message ("%d %q&",
120 ctkind_toInt (c->kind),
121 ctbase_dump (c->ctbase)));
123 else if (c->base == ctype_undefined
124 && c->array == ctype_dne)
126 if (c->ptr == ctype_dne)
128 return (message ("%d %q!",
129 ctkind_toInt (c->kind),
130 ctbase_dump (c->ctbase)));
134 return (message ("%d %q^%d",
135 ctkind_toInt (c->kind),
136 ctbase_dump (c->ctbase),
140 else if (c->ptr == ctype_dne
141 && c->array == ctype_dne)
143 return (message ("%d %q%d&",
144 ctkind_toInt (c->kind),
145 ctbase_dump (c->ctbase),
150 return (message ("%d %q%d %d %d",
151 ctkind_toInt (c->kind),
152 ctbase_dump (c->ctbase),
153 c->base, c->ptr, c->array));
158 static /*@only@*/ ctentry
159 ctentry_undump (/*@dependent@*/ char *s) /*@requires maxRead(s) >= 2 @*/
161 int base, ptr, array;
165 kind = ctkind_fromInt (reader_getInt (&s));
166 ct = ctbase_undump (&s);
168 if (reader_optCheckChar (&s, '&'))
174 else if (reader_optCheckChar (&s, '!'))
176 base = ctype_undefined;
180 else if (reader_optCheckChar (&s, '^'))
182 base = ctype_undefined;
183 ptr = reader_getInt (&s);
188 base = reader_getInt (&s);
190 if (reader_optCheckChar (&s, '&'))
197 ptr = reader_getInt (&s);
198 array = reader_getInt (&s);
202 /* can't unparse w/o typeTable */
203 return (ctentry_make (kind, ct, base, ptr, array, cstring_undefined));
206 static /*@observer@*/ cstring
207 ctentry_doUnparse (ctentry c) /*@modifies c@*/
209 if (cstring_isDefined (c->unparse))
215 cstring s = ctbase_unparse (c->ctbase);
217 if (!cstring_isEmpty (s) && !cstring_containsChar (s, '<'))
223 cstring_markOwned (s);
230 static /*@observer@*/ cstring
231 ctentry_doUnparseDeep (ctentry c)
233 if (cstring_isDefined (c->unparse))
239 c->unparse = ctbase_unparseDeep (c->ctbase);
245 ** cttable operations
248 static /*@only@*/ cstring
249 cttable_unparse (void)
252 cstring s = cstring_undefined;
255 for (i = 0; i < cttab.size; i++)
257 /*drl bee: si*/ ctentry cte = cttab.entries[i];
258 if (ctentry_isInteresting (cte))
260 if (ctbase_isUA (cte->ctbase))
262 s = message ("%s%d\t%q [%d]\n", s, i, ctentry_unparse (cttab.entries[i]),
263 cte->ctbase->contents.tid);
267 s = message ("%s%d\t%q\n", s, i, ctentry_unparse (cttab.entries[i]));
271 /*@noaccess ctbase@*/
281 for (i = 0; i < cttab.size; i++)
283 /*drl bee: si*/ ctentry cte = cttab.entries[i];
285 if (TRUE) /* ctentry_isInteresting (cte)) */
287 if (ctbase_isUA (cte->ctbase))
289 fprintf (g_warningstream, "%3d: %s [%d]\n", i,
290 cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i])),
291 cte->ctbase->contents.tid);
295 fprintf (g_warningstream, "%3d: %s\n", i,
296 cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i])));
301 /* fprintf (g_warningstream, "%3d: <no name>\n", i); */
304 /*@noaccess ctbase@*/
310 ** Output cttable for dump file
314 cttable_dump (FILE *fout)
316 bool showdots = FALSE;
317 int showdotstride = 0;
320 if (context_getFlag (FLG_SHOWSCAN) && cttab.size > 5000)
323 displayScanOpen (message ("Dumping type table (%d types)", cttab.size));
324 showdotstride = cttab.size / 5;
328 for (i = 0; i < cttab.size; i++)
332 /*drl bee: si*/ s = ctentry_dump (cttab.entries[i]);
333 DPRINTF (("[%d] = %s", i, ctentry_unparse (cttab.entries[i])));
334 llassert (cstring_length (s) < MAX_DUMP_LINE_LENGTH);
335 fputline (fout, cstring_toCharsSafe (s));
338 if (showdots && (i != 0 && ((i - 1) % showdotstride == 0)))
340 (void) fflush (g_warningstream);
341 displayScanContinue (cstring_makeLiteralTemp ("."));
342 (void) fflush (stderr);
349 displayScanOpen (cstring_makeLiteral ("Continuing dump "));
355 ** load cttable from init file
358 static void cttable_load (FILE *f)
360 /*@modifies cttab, f @*/
362 char *s = mstring_create (MAX_DUMP_LINE_LENGTH);
369 DPRINTF (("Loading cttable: "));
373 while (reader_readLine (f, s, MAX_DUMP_LINE_LENGTH) != NULL && *s == ';')
378 if (mstring_length (s) == (MAX_DUMP_LINE_LENGTH - 1))
380 llbug (message ("Library line too long: %s\n", cstring_fromChars (s)));
383 while (s != NULL && *s != ';' && *s != '\0')
387 /*drl bee: tcf*/ cte = ctentry_undump (s);
388 ct = cttable_addFull (cte);
390 DPRINTF (("Type: %d: %s", ct, ctype_unparse (ct)));
392 if (ctbase_isConj (cte->ctbase)
393 && !(ctbase_isExplicitConj (cte->ctbase)))
395 ctype_recordConj (ct);
398 s = reader_readLine (f, s, MAX_DUMP_LINE_LENGTH);
404 DPRINTF (("Done loading cttable: "));
412 ** fill up the cttable with basic types, and first order derivations.
413 ** this is done without using our constructors for efficiency reasons
419 static void cttable_init (void)
420 /*@globals cttab@*/ /*@modifies cttab@*/
424 ctbase ct = ctbase_undefined;
426 llassert (cttab.size == 0);
428 /* do for plain, pointer, arrayof */
429 for (i = CTK_PLAIN; i <= CTK_ARRAY; i++)
431 for (j = CTX_UNKNOWN; j <= CTX_LAST; j++)
437 ct = ctbase_createBool (); /* why different? */
439 else if (j == CTX_UNKNOWN)
441 ct = ctbase_createUnknown ();
445 ct = ctbase_createPrim ((cprim)j);
448 (void) cttable_addFull
449 (ctentry_make (CTK_PLAIN,
451 j + CTK_PREDEFINED, j + CTK_PREDEFINED2,
452 ctbase_unparse (ct)));
459 ct = ctbase_makePointer (j);
460 /*@switchbreak@*/ break;
462 ct = ctbase_makeArray (j);
463 /*@switchbreak@*/ break;
465 llbugexitlit ("cttable_init: base case");
468 (void) cttable_addDerived (i, ct, j);
473 /**** reserve a slot for userBool ****/
474 (void) cttable_addFull (ctentry_make (CTK_INVALID, ctbase_undefined,
475 ctype_undefined, ctype_dne, ctype_dne,
485 o_ctentry *newentries ;
487 cttab.nspace = CTK_BASESIZE;
488 newentries = (ctentry *) dmalloc (sizeof (*newentries) * (cttab.size + cttab.nspace));
490 if (newentries == NULL)
492 llfatalerror (message ("cttable_grow: out of memory. Size: %d",
496 for (i = 0; i < cttab.size; i++)
498 /*drl bee: dm*/ /*drl bee: si*/ newentries[i] = cttab.entries[i];
502 sfree (cttab.entries);
505 cttab.entries = newentries;
510 cttable_addDerived (ctkind ctk, /*@keep@*/ ctbase cnew, ctype base)
512 if (cttab.nspace == 0)
515 /*drl bee: si*/ cttab.entries[cttab.size] =
516 ctentry_make (ctk, cnew, base, ctype_dne, ctype_dne, cstring_undefined);
520 return (cttab.size++);
524 cttable_addComplex (/*@only@*/ ctbase cnew)
525 /*@modifies cttab; @*/
528 if (cnew->type != CT_FCN && cnew->type != CT_EXPFCN)
531 int ctstop = cttable_lastIndex () - DEFAULT_OPTLEVEL;
533 if (ctstop < LAST_PREDEFINED)
535 ctstop = LAST_PREDEFINED;
538 for (i = cttable_lastIndex (); i >= ctstop; i--) /* better to go from back... */
542 ctb = ctype_getCtbase (i);
544 /* is this optimization really worthwhile? */
546 if (ctbase_isDefined (ctb) && ctbase_equivStrict (cnew, ctb))
548 DPRINTF (("EQUIV!! %s / %s",
549 ctbase_unparse (cnew),
550 ctbase_unparse (ctb)));
558 if (cttab.nspace == 0)
561 /*drl bee: si*/ cttab.entries[cttab.size] = ctentry_make (CTK_COMPLEX, cnew, ctype_undefined,
562 ctype_dne, ctype_dne,
566 return (cttab.size++);
567 /*@noaccess ctbase@*/
571 cttable_addFull (ctentry cnew)
573 if (cttab.nspace == 0)
578 /*drl bee: si*/ cttab.entries[cttab.size] = cnew;
581 return (cttab.size++);
585 cttable_addFullSafe (/*@only@*/ ctentry cnew)
588 ctbase cnewbase = cnew->ctbase;
590 llassert (ctbase_isDefined (cnewbase));
592 for (i = cttable_lastIndex (); i >= CT_FIRST; i--)
594 ctbase ctb = ctype_getCtbase (i);
596 if (ctbase_isDefined (ctb)
597 && ctbase_equiv (cnewbase, ctype_getCtbaseSafe (i)))
604 if (cttab.nspace == 0)
607 /*drl bee: si*/ cttab.entries[cttab.size] = cnew;
611 return (cttab.size++);