]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* ;-*-C-*-; |
1b8ae690 | 2 | ** Splint - annotation-assisted static program checker |
3 | ** Copyright (C) 1994-2002 University of Virginia, | |
4 | ** Massachusetts Institute of Technology | |
885824d3 | 5 | ** |
1b8ae690 | 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. | |
885824d3 | 19 | ** |
155af98d | 20 | ** For information on splint: info@splint.org |
21 | ** To report a bug: splint-bug@splint.org | |
1b8ae690 | 22 | ** For more information: http://www.splint.org |
885824d3 | 23 | */ |
24 | /* | |
25 | ** cttable.i | |
26 | ** | |
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.) | |
30 | */ | |
31 | ||
32 | /*@access ctype@*/ | |
33 | ||
34 | /* | |
35 | ** type definitions and forward declarations in ctbase.i | |
36 | */ | |
37 | ||
38 | static void | |
39 | ctentry_free (/*@only@*/ ctentry c) | |
40 | { | |
41 | ctbase_free (c->ctbase); | |
42 | cstring_free (c->unparse); | |
43 | sfree (c); | |
44 | } | |
45 | ||
46 | static void cttable_reset (void) | |
47 | /*@globals cttab@*/ | |
48 | /*@modifies cttab@*/ | |
49 | { | |
50 | if (cttab.entries != NULL) | |
51 | { | |
52 | int i; | |
53 | ||
54 | for (i = 0; i < cttab.size; i++) | |
55 | { | |
86d93ed3 | 56 | /*drl bee: si*/ ctentry_free (cttab.entries[i]); |
885824d3 | 57 | } |
58 | ||
59 | /*@-compdestroy@*/ | |
60 | sfree (cttab.entries); | |
61 | /*@=compdestroy@*/ | |
62 | ||
63 | cttab.entries = NULL; | |
64 | } | |
65 | ||
66 | cttab.size = 0 ; | |
67 | cttab.nspace = 0 ; | |
68 | } | |
69 | ||
885824d3 | 70 | static ctentry |
71 | ctentry_makeNew (ctkind ctk, /*@only@*/ ctbase c) | |
72 | { | |
73 | ||
74 | return (ctentry_make (ctk, c, ctype_dne, ctype_dne, ctype_dne, cstring_undefined)); | |
75 | } | |
76 | ||
77 | static /*@only@*/ ctentry | |
78 | ctentry_make (ctkind ctk, | |
79 | /*@keep@*/ ctbase c, ctype base, | |
80 | ctype ptr, ctype array, | |
81 | /*@keep@*/ cstring unparse) /*@*/ | |
82 | { | |
83 | ctentry cte = (ctentry) dmalloc (sizeof (*cte)); | |
84 | cte->kind = ctk; | |
85 | cte->ctbase = c; | |
86 | cte->base = base; | |
87 | cte->ptr = ptr; | |
88 | cte->array = array; | |
89 | cte->unparse = unparse; | |
90 | return cte; | |
91 | } | |
92 | ||
93 | static cstring | |
94 | ctentry_unparse (ctentry c) | |
95 | { | |
96 | return (message | |
97 | ("%20s [%d] [%d] [%d]", | |
98 | (cstring_isDefined (c->unparse) ? c->unparse : cstring_makeLiteral ("<no name>")), | |
99 | c->base, | |
100 | c->ptr, | |
101 | c->array)); | |
102 | } | |
103 | ||
104 | static bool | |
105 | ctentry_isInteresting (ctentry c) | |
106 | { | |
107 | return (cstring_isNonEmpty (c->unparse)); | |
108 | } | |
109 | ||
110 | static /*@only@*/ cstring | |
111 | ctentry_dump (ctentry c) | |
112 | { | |
a0a162cd | 113 | DPRINTF (("Dumping: %s", ctentry_unparse (c))); |
114 | ||
885824d3 | 115 | if (c->ptr == ctype_dne |
116 | && c->array == ctype_dne | |
117 | && c->base == ctype_dne) | |
118 | { | |
119 | return (message ("%d %q&", | |
120 | ctkind_toInt (c->kind), | |
121 | ctbase_dump (c->ctbase))); | |
122 | } | |
123 | else if (c->base == ctype_undefined | |
124 | && c->array == ctype_dne) | |
125 | { | |
126 | if (c->ptr == ctype_dne) | |
127 | { | |
128 | return (message ("%d %q!", | |
129 | ctkind_toInt (c->kind), | |
130 | ctbase_dump (c->ctbase))); | |
131 | } | |
132 | else | |
133 | { | |
134 | return (message ("%d %q^%d", | |
135 | ctkind_toInt (c->kind), | |
136 | ctbase_dump (c->ctbase), | |
137 | c->ptr)); | |
138 | } | |
139 | } | |
140 | else if (c->ptr == ctype_dne | |
141 | && c->array == ctype_dne) | |
142 | { | |
143 | return (message ("%d %q%d&", | |
144 | ctkind_toInt (c->kind), | |
145 | ctbase_dump (c->ctbase), | |
146 | c->base)); | |
147 | } | |
148 | else | |
149 | { | |
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)); | |
154 | } | |
155 | } | |
156 | ||
157 | ||
158 | static /*@only@*/ ctentry | |
86d93ed3 | 159 | ctentry_undump (/*@dependent@*/ char *s) /*@requires maxRead(s) >= 2 @*/ |
885824d3 | 160 | { |
161 | int base, ptr, array; | |
162 | ctkind kind; | |
163 | ctbase ct; | |
164 | ||
28bf4b0b | 165 | kind = ctkind_fromInt (reader_getInt (&s)); |
885824d3 | 166 | ct = ctbase_undump (&s); |
167 | ||
28bf4b0b | 168 | if (reader_optCheckChar (&s, '&')) |
885824d3 | 169 | { |
170 | base = ctype_dne; | |
171 | ptr = ctype_dne; | |
172 | array = ctype_dne; | |
173 | } | |
28bf4b0b | 174 | else if (reader_optCheckChar (&s, '!')) |
885824d3 | 175 | { |
176 | base = ctype_undefined; | |
177 | ptr = ctype_dne; | |
178 | array = ctype_dne; | |
179 | } | |
28bf4b0b | 180 | else if (reader_optCheckChar (&s, '^')) |
885824d3 | 181 | { |
182 | base = ctype_undefined; | |
28bf4b0b | 183 | ptr = reader_getInt (&s); |
885824d3 | 184 | array = ctype_dne; |
185 | } | |
186 | else | |
187 | { | |
28bf4b0b | 188 | base = reader_getInt (&s); |
885824d3 | 189 | |
28bf4b0b | 190 | if (reader_optCheckChar (&s, '&')) |
885824d3 | 191 | { |
192 | ptr = ctype_dne; | |
193 | array = ctype_dne; | |
194 | } | |
195 | else | |
196 | { | |
28bf4b0b | 197 | ptr = reader_getInt (&s); |
198 | array = reader_getInt (&s); | |
885824d3 | 199 | } |
200 | } | |
201 | ||
202 | /* can't unparse w/o typeTable */ | |
203 | return (ctentry_make (kind, ct, base, ptr, array, cstring_undefined)); | |
204 | } | |
205 | ||
206 | static /*@observer@*/ cstring | |
207 | ctentry_doUnparse (ctentry c) /*@modifies c@*/ | |
208 | { | |
209 | if (cstring_isDefined (c->unparse)) | |
210 | { | |
211 | return (c->unparse); | |
212 | } | |
213 | else | |
214 | { | |
215 | cstring s = ctbase_unparse (c->ctbase); | |
216 | ||
217 | if (!cstring_isEmpty (s) && !cstring_containsChar (s, '<')) | |
218 | { | |
219 | c->unparse = s; | |
220 | } | |
221 | else | |
222 | { | |
223 | cstring_markOwned (s); | |
224 | } | |
225 | ||
226 | return (s); | |
227 | } | |
228 | } | |
229 | ||
230 | static /*@observer@*/ cstring | |
231 | ctentry_doUnparseDeep (ctentry c) | |
232 | { | |
233 | if (cstring_isDefined (c->unparse)) | |
234 | { | |
235 | return (c->unparse); | |
236 | } | |
237 | else | |
238 | { | |
239 | c->unparse = ctbase_unparseDeep (c->ctbase); | |
240 | return (c->unparse); | |
241 | } | |
242 | } | |
243 | ||
244 | /* | |
245 | ** cttable operations | |
246 | */ | |
247 | ||
248 | static /*@only@*/ cstring | |
249 | cttable_unparse (void) | |
250 | { | |
251 | int i; | |
252 | cstring s = cstring_undefined; | |
253 | ||
254 | /*@access ctbase@*/ | |
255 | for (i = 0; i < cttab.size; i++) | |
256 | { | |
86d93ed3 | 257 | /*drl bee: si*/ ctentry cte = cttab.entries[i]; |
885824d3 | 258 | if (ctentry_isInteresting (cte)) |
259 | { | |
260 | if (ctbase_isUA (cte->ctbase)) | |
261 | { | |
262 | s = message ("%s%d\t%q [%d]\n", s, i, ctentry_unparse (cttab.entries[i]), | |
263 | cte->ctbase->contents.tid); | |
264 | } | |
265 | else | |
266 | { | |
267 | s = message ("%s%d\t%q\n", s, i, ctentry_unparse (cttab.entries[i])); | |
268 | } | |
269 | } | |
270 | } | |
271 | /*@noaccess ctbase@*/ | |
272 | return (s); | |
273 | } | |
274 | ||
275 | void | |
276 | cttable_print (void) | |
277 | { | |
278 | int i; | |
279 | ||
280 | /*@access ctbase@*/ | |
281 | for (i = 0; i < cttab.size; i++) | |
282 | { | |
86d93ed3 | 283 | /*drl bee: si*/ ctentry cte = cttab.entries[i]; |
885824d3 | 284 | |
28bf4b0b | 285 | if (TRUE) /* ctentry_isInteresting (cte)) */ |
885824d3 | 286 | { |
287 | if (ctbase_isUA (cte->ctbase)) | |
288 | { | |
80489f0a | 289 | fprintf (g_warningstream, "%3d: %s [%d]\n", i, |
885824d3 | 290 | cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i])), |
291 | cte->ctbase->contents.tid); | |
292 | } | |
293 | else | |
294 | { | |
80489f0a | 295 | fprintf (g_warningstream, "%3d: %s\n", i, |
885824d3 | 296 | cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i]))); |
297 | } | |
298 | } | |
299 | else | |
300 | { | |
80489f0a | 301 | /* fprintf (g_warningstream, "%3d: <no name>\n", i); */ |
885824d3 | 302 | } |
303 | } | |
304 | /*@noaccess ctbase@*/ | |
305 | } | |
306 | ||
307 | /* | |
308 | ** cttable_dump | |
309 | ** | |
310 | ** Output cttable for dump file | |
311 | */ | |
312 | ||
313 | static void | |
314 | cttable_dump (FILE *fout) | |
315 | { | |
316 | bool showdots = FALSE; | |
317 | int showdotstride = 0; | |
318 | int i; | |
319 | ||
320 | if (context_getFlag (FLG_SHOWSCAN) && cttab.size > 5000) | |
321 | { | |
80489f0a | 322 | displayScanClose (); |
495af944 | 323 | displayScanOpen (message ("< Dumping type table (%d types) ", cttab.size)); |
885824d3 | 324 | showdotstride = cttab.size / 5; |
325 | showdots = TRUE; | |
326 | } | |
327 | ||
328 | for (i = 0; i < cttab.size; i++) | |
329 | { | |
330 | cstring s; | |
331 | ||
86d93ed3 | 332 | /*drl bee: si*/ s = ctentry_dump (cttab.entries[i]); |
28bf4b0b | 333 | DPRINTF (("[%d] = %s", i, ctentry_unparse (cttab.entries[i]))); |
885824d3 | 334 | llassert (cstring_length (s) < MAX_DUMP_LINE_LENGTH); |
335 | fputline (fout, cstring_toCharsSafe (s)); | |
336 | cstring_free (s); | |
337 | ||
338 | if (showdots && (i != 0 && ((i - 1) % showdotstride == 0))) | |
339 | { | |
80489f0a | 340 | (void) fflush (g_warningstream); |
495af944 | 341 | fprintf (stderr, "."); |
885824d3 | 342 | (void) fflush (stderr); |
343 | } | |
344 | } | |
345 | ||
346 | if (showdots) | |
347 | { | |
495af944 | 348 | fprintf (stderr, " >\n< Continuing dump "); |
885824d3 | 349 | } |
350 | ||
a0a162cd | 351 | } |
885824d3 | 352 | |
353 | /* | |
354 | ** load cttable from init file | |
355 | */ | |
356 | ||
357 | static void cttable_load (FILE *f) | |
358 | /*@globals cttab @*/ | |
359 | /*@modifies cttab, f @*/ | |
360 | { | |
361 | char *s = mstring_create (MAX_DUMP_LINE_LENGTH); | |
362 | ctentry cte; | |
363 | ||
364 | cttable_reset (); | |
365 | ||
28bf4b0b | 366 | /* |
367 | DPRINTF (("Loading cttable: ")); | |
368 | cttable_print (); | |
369 | */ | |
370 | ||
371 | while (reader_readLine (f, s, MAX_DUMP_LINE_LENGTH) != NULL && *s == ';') | |
885824d3 | 372 | { |
373 | ; | |
374 | } | |
375 | ||
376 | if (mstring_length (s) == (MAX_DUMP_LINE_LENGTH - 1)) | |
377 | { | |
378 | llbug (message ("Library line too long: %s\n", cstring_fromChars (s))); | |
379 | } | |
380 | ||
381 | while (s != NULL && *s != ';' && *s != '\0') | |
382 | { | |
383 | ctype ct; | |
384 | ||
86d93ed3 | 385 | /*drl bee: tcf*/ cte = ctentry_undump (s); |
885824d3 | 386 | ct = cttable_addFull (cte); |
387 | ||
28bf4b0b | 388 | DPRINTF (("Type: %d: %s", ct, ctype_unparse (ct))); |
389 | ||
885824d3 | 390 | if (ctbase_isConj (cte->ctbase) |
28bf4b0b | 391 | && !(ctbase_isExplicitConj (cte->ctbase))) |
885824d3 | 392 | { |
393 | ctype_recordConj (ct); | |
394 | } | |
395 | ||
28bf4b0b | 396 | (void) reader_readLine (f, s, MAX_DUMP_LINE_LENGTH); |
885824d3 | 397 | } |
398 | ||
399 | sfree (s); | |
28bf4b0b | 400 | |
401 | /* | |
402 | DPRINTF (("Done loading cttable: ")); | |
403 | cttable_print (); | |
404 | */ | |
405 | } | |
885824d3 | 406 | |
407 | /* | |
408 | ** cttable_init | |
409 | ** | |
410 | ** fill up the cttable with basic types, and first order derivations. | |
411 | ** this is done without using our constructors for efficiency reasons | |
412 | ** (probably bogus) | |
413 | ** | |
414 | */ | |
415 | ||
416 | /*@access cprim@*/ | |
417 | static void cttable_init (void) | |
418 | /*@globals cttab@*/ /*@modifies cttab@*/ | |
419 | { | |
420 | ctkind i; | |
421 | cprim j; | |
422 | ctbase ct = ctbase_undefined; | |
423 | ||
424 | llassert (cttab.size == 0); | |
425 | ||
426 | /* do for plain, pointer, arrayof */ | |
427 | for (i = CTK_PLAIN; i <= CTK_ARRAY; i++) | |
428 | { | |
429 | for (j = CTX_UNKNOWN; j <= CTX_LAST; j++) | |
430 | { | |
431 | if (i == CTK_PLAIN) | |
432 | { | |
433 | if (j == CTX_BOOL) | |
434 | { | |
435 | ct = ctbase_createBool (); /* why different? */ | |
436 | } | |
437 | else if (j == CTX_UNKNOWN) | |
438 | { | |
439 | ct = ctbase_createUnknown (); | |
440 | } | |
441 | else | |
442 | { | |
443 | ct = ctbase_createPrim ((cprim)j); | |
444 | } | |
445 | ||
446 | (void) cttable_addFull | |
447 | (ctentry_make (CTK_PLAIN, | |
448 | ct, ctype_undefined, | |
449 | j + CTK_PREDEFINED, j + CTK_PREDEFINED2, | |
450 | ctbase_unparse (ct))); | |
451 | } | |
452 | else | |
453 | { | |
454 | switch (i) | |
455 | { | |
456 | case CTK_PTR: | |
457 | ct = ctbase_makePointer (j); | |
458 | /*@switchbreak@*/ break; | |
459 | case CTK_ARRAY: | |
460 | ct = ctbase_makeArray (j); | |
461 | /*@switchbreak@*/ break; | |
462 | default: | |
463 | llbugexitlit ("cttable_init: base case"); | |
464 | } | |
465 | ||
466 | (void) cttable_addDerived (i, ct, j); | |
467 | } | |
468 | } | |
469 | } | |
470 | ||
471 | /**** reserve a slot for userBool ****/ | |
472 | (void) cttable_addFull (ctentry_make (CTK_INVALID, ctbase_undefined, | |
473 | ctype_undefined, ctype_dne, ctype_dne, | |
474 | cstring_undefined)); | |
475 | } | |
476 | ||
477 | /*@noaccess cprim@*/ | |
478 | ||
479 | static void | |
480 | cttable_grow () | |
481 | { | |
482 | int i; | |
483 | o_ctentry *newentries ; | |
484 | ||
485 | cttab.nspace = CTK_BASESIZE; | |
486 | newentries = (ctentry *) dmalloc (sizeof (*newentries) * (cttab.size + cttab.nspace)); | |
487 | ||
488 | if (newentries == NULL) | |
489 | { | |
490 | llfatalerror (message ("cttable_grow: out of memory. Size: %d", | |
491 | cttab.size)); | |
492 | } | |
493 | ||
494 | for (i = 0; i < cttab.size; i++) | |
495 | { | |
86d93ed3 | 496 | /*drl bee: dm*/ /*drl bee: si*/ newentries[i] = cttab.entries[i]; |
885824d3 | 497 | } |
498 | ||
499 | /*@-compdestroy@*/ | |
500 | sfree (cttab.entries); | |
501 | /*@=compdestroy@*/ | |
502 | ||
503 | cttab.entries = newentries; | |
504 | /*@-compdef@*/ | |
505 | } /*@=compdef@*/ | |
506 | ||
507 | static ctype | |
508 | cttable_addDerived (ctkind ctk, /*@keep@*/ ctbase cnew, ctype base) | |
509 | { | |
510 | if (cttab.nspace == 0) | |
511 | cttable_grow (); | |
512 | ||
86d93ed3 | 513 | /*drl bee: si*/ cttab.entries[cttab.size] = |
885824d3 | 514 | ctentry_make (ctk, cnew, base, ctype_dne, ctype_dne, cstring_undefined); |
515 | ||
516 | cttab.nspace--; | |
517 | ||
518 | return (cttab.size++); | |
519 | } | |
520 | ||
521 | static ctype | |
28bf4b0b | 522 | cttable_addComplex (/*@only@*/ ctbase cnew) |
885824d3 | 523 | /*@modifies cttab; @*/ |
524 | { | |
28bf4b0b | 525 | /*@access ctbase@*/ |
885824d3 | 526 | if (cnew->type != CT_FCN && cnew->type != CT_EXPFCN) |
527 | { | |
528 | ctype i; | |
529 | int ctstop = cttable_lastIndex () - DEFAULT_OPTLEVEL; | |
530 | ||
531 | if (ctstop < LAST_PREDEFINED) | |
532 | { | |
533 | ctstop = LAST_PREDEFINED; | |
534 | } | |
535 | ||
536 | for (i = cttable_lastIndex (); i >= ctstop; i--) /* better to go from back... */ | |
537 | { | |
538 | ctbase ctb; | |
539 | ||
885824d3 | 540 | ctb = ctype_getCtbase (i); |
28bf4b0b | 541 | |
542 | /*@i32 is this optimization really worthwhile??? */ | |
885824d3 | 543 | |
544 | if (ctbase_isDefined (ctb) && ctbase_equivStrict (cnew, ctb)) | |
545 | { | |
a0a162cd | 546 | DPRINTF (("EQUIV!! %s / %s", |
547 | ctbase_unparse (cnew), | |
548 | ctbase_unparse (ctb))); | |
28bf4b0b | 549 | |
885824d3 | 550 | ctbase_free (cnew); |
885824d3 | 551 | return i; |
552 | } | |
553 | } | |
554 | } | |
555 | ||
556 | if (cttab.nspace == 0) | |
557 | cttable_grow (); | |
558 | ||
86d93ed3 | 559 | /*drl bee: si*/ cttab.entries[cttab.size] = ctentry_make (CTK_COMPLEX, cnew, ctype_undefined, |
885824d3 | 560 | ctype_dne, ctype_dne, |
561 | cstring_undefined); | |
562 | cttab.nspace--; | |
563 | ||
564 | return (cttab.size++); | |
28bf4b0b | 565 | /*@noaccess ctbase@*/ |
885824d3 | 566 | } |
567 | ||
568 | static ctype | |
569 | cttable_addFull (ctentry cnew) | |
570 | { | |
571 | if (cttab.nspace == 0) | |
572 | { | |
573 | cttable_grow (); | |
574 | } | |
575 | ||
86d93ed3 | 576 | /*drl bee: si*/ cttab.entries[cttab.size] = cnew; |
885824d3 | 577 | cttab.nspace--; |
578 | ||
579 | return (cttab.size++); | |
580 | } | |
581 | ||
582 | static ctype | |
583 | cttable_addFullSafe (/*@only@*/ ctentry cnew) | |
584 | { | |
585 | int i; | |
586 | ctbase cnewbase = cnew->ctbase; | |
587 | ||
588 | llassert (ctbase_isDefined (cnewbase)); | |
589 | ||
590 | for (i = cttable_lastIndex (); i >= CT_FIRST; i--) | |
591 | { | |
592 | ctbase ctb = ctype_getCtbase (i); | |
593 | ||
594 | if (ctbase_isDefined (ctb) | |
595 | && ctbase_equiv (cnewbase, ctype_getCtbaseSafe (i))) | |
596 | { | |
597 | ctentry_free (cnew); | |
598 | return i; | |
599 | } | |
600 | } | |
601 | ||
602 | if (cttab.nspace == 0) | |
603 | cttable_grow (); | |
604 | ||
86d93ed3 | 605 | /*drl bee: si*/ cttab.entries[cttab.size] = cnew; |
885824d3 | 606 | |
607 | cttab.nspace--; | |
608 | ||
609 | return (cttab.size++); | |
610 | } | |
611 |