]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* ;-*-C-*-; |
1b8ae690 | 2 | ** Splint - annotation-assisted static program checker |
c59f5181 | 3 | ** Copyright (C) 1994-2003 University of Virginia, |
1b8ae690 | 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 (); |
ce7034f0 | 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); |
ce7034f0 | 341 | displayScanContinue (cstring_makeLiteralTemp (".")); |
885824d3 | 342 | (void) fflush (stderr); |
343 | } | |
344 | } | |
345 | ||
346 | if (showdots) | |
347 | { | |
ce7034f0 | 348 | displayScanClose (); |
349 | displayScanOpen (cstring_makeLiteral ("Continuing dump ")); | |
885824d3 | 350 | } |
351 | ||
a0a162cd | 352 | } |
885824d3 | 353 | |
354 | /* | |
355 | ** load cttable from init file | |
356 | */ | |
357 | ||
358 | static void cttable_load (FILE *f) | |
359 | /*@globals cttab @*/ | |
360 | /*@modifies cttab, f @*/ | |
361 | { | |
362 | char *s = mstring_create (MAX_DUMP_LINE_LENGTH); | |
6fcd0b1e | 363 | char *os = s; |
885824d3 | 364 | ctentry cte; |
365 | ||
366 | cttable_reset (); | |
367 | ||
28bf4b0b | 368 | /* |
369 | DPRINTF (("Loading cttable: ")); | |
370 | cttable_print (); | |
371 | */ | |
372 | ||
373 | while (reader_readLine (f, s, MAX_DUMP_LINE_LENGTH) != NULL && *s == ';') | |
885824d3 | 374 | { |
375 | ; | |
376 | } | |
377 | ||
378 | if (mstring_length (s) == (MAX_DUMP_LINE_LENGTH - 1)) | |
379 | { | |
380 | llbug (message ("Library line too long: %s\n", cstring_fromChars (s))); | |
381 | } | |
382 | ||
383 | while (s != NULL && *s != ';' && *s != '\0') | |
384 | { | |
385 | ctype ct; | |
386 | ||
6fcd0b1e | 387 | /*drl bee: tcf*/ cte = ctentry_undump (s); |
885824d3 | 388 | ct = cttable_addFull (cte); |
389 | ||
28bf4b0b | 390 | DPRINTF (("Type: %d: %s", ct, ctype_unparse (ct))); |
391 | ||
885824d3 | 392 | if (ctbase_isConj (cte->ctbase) |
28bf4b0b | 393 | && !(ctbase_isExplicitConj (cte->ctbase))) |
885824d3 | 394 | { |
395 | ctype_recordConj (ct); | |
396 | } | |
397 | ||
6fcd0b1e | 398 | s = reader_readLine (f, s, MAX_DUMP_LINE_LENGTH); |
885824d3 | 399 | } |
400 | ||
6fcd0b1e | 401 | sfree (os); |
28bf4b0b | 402 | |
403 | /* | |
404 | DPRINTF (("Done loading cttable: ")); | |
405 | cttable_print (); | |
406 | */ | |
407 | } | |
885824d3 | 408 | |
409 | /* | |
410 | ** cttable_init | |
411 | ** | |
412 | ** fill up the cttable with basic types, and first order derivations. | |
413 | ** this is done without using our constructors for efficiency reasons | |
414 | ** (probably bogus) | |
415 | ** | |
416 | */ | |
417 | ||
418 | /*@access cprim@*/ | |
419 | static void cttable_init (void) | |
420 | /*@globals cttab@*/ /*@modifies cttab@*/ | |
421 | { | |
422 | ctkind i; | |
423 | cprim j; | |
424 | ctbase ct = ctbase_undefined; | |
425 | ||
426 | llassert (cttab.size == 0); | |
427 | ||
428 | /* do for plain, pointer, arrayof */ | |
429 | for (i = CTK_PLAIN; i <= CTK_ARRAY; i++) | |
430 | { | |
431 | for (j = CTX_UNKNOWN; j <= CTX_LAST; j++) | |
432 | { | |
433 | if (i == CTK_PLAIN) | |
434 | { | |
435 | if (j == CTX_BOOL) | |
436 | { | |
437 | ct = ctbase_createBool (); /* why different? */ | |
438 | } | |
439 | else if (j == CTX_UNKNOWN) | |
440 | { | |
441 | ct = ctbase_createUnknown (); | |
442 | } | |
443 | else | |
444 | { | |
445 | ct = ctbase_createPrim ((cprim)j); | |
446 | } | |
447 | ||
448 | (void) cttable_addFull | |
449 | (ctentry_make (CTK_PLAIN, | |
450 | ct, ctype_undefined, | |
451 | j + CTK_PREDEFINED, j + CTK_PREDEFINED2, | |
452 | ctbase_unparse (ct))); | |
453 | } | |
454 | else | |
455 | { | |
456 | switch (i) | |
457 | { | |
458 | case CTK_PTR: | |
459 | ct = ctbase_makePointer (j); | |
460 | /*@switchbreak@*/ break; | |
461 | case CTK_ARRAY: | |
462 | ct = ctbase_makeArray (j); | |
463 | /*@switchbreak@*/ break; | |
464 | default: | |
465 | llbugexitlit ("cttable_init: base case"); | |
466 | } | |
467 | ||
468 | (void) cttable_addDerived (i, ct, j); | |
469 | } | |
470 | } | |
471 | } | |
472 | ||
473 | /**** reserve a slot for userBool ****/ | |
474 | (void) cttable_addFull (ctentry_make (CTK_INVALID, ctbase_undefined, | |
475 | ctype_undefined, ctype_dne, ctype_dne, | |
476 | cstring_undefined)); | |
477 | } | |
478 | ||
479 | /*@noaccess cprim@*/ | |
480 | ||
481 | static void | |
482 | cttable_grow () | |
483 | { | |
484 | int i; | |
485 | o_ctentry *newentries ; | |
486 | ||
487 | cttab.nspace = CTK_BASESIZE; | |
488 | newentries = (ctentry *) dmalloc (sizeof (*newentries) * (cttab.size + cttab.nspace)); | |
489 | ||
490 | if (newentries == NULL) | |
491 | { | |
492 | llfatalerror (message ("cttable_grow: out of memory. Size: %d", | |
493 | cttab.size)); | |
494 | } | |
495 | ||
496 | for (i = 0; i < cttab.size; i++) | |
497 | { | |
86d93ed3 | 498 | /*drl bee: dm*/ /*drl bee: si*/ newentries[i] = cttab.entries[i]; |
885824d3 | 499 | } |
500 | ||
501 | /*@-compdestroy@*/ | |
502 | sfree (cttab.entries); | |
503 | /*@=compdestroy@*/ | |
504 | ||
505 | cttab.entries = newentries; | |
506 | /*@-compdef@*/ | |
507 | } /*@=compdef@*/ | |
508 | ||
509 | static ctype | |
510 | cttable_addDerived (ctkind ctk, /*@keep@*/ ctbase cnew, ctype base) | |
511 | { | |
512 | if (cttab.nspace == 0) | |
513 | cttable_grow (); | |
514 | ||
86d93ed3 | 515 | /*drl bee: si*/ cttab.entries[cttab.size] = |
885824d3 | 516 | ctentry_make (ctk, cnew, base, ctype_dne, ctype_dne, cstring_undefined); |
517 | ||
518 | cttab.nspace--; | |
519 | ||
520 | return (cttab.size++); | |
521 | } | |
522 | ||
523 | static ctype | |
28bf4b0b | 524 | cttable_addComplex (/*@only@*/ ctbase cnew) |
885824d3 | 525 | /*@modifies cttab; @*/ |
526 | { | |
28bf4b0b | 527 | /*@access ctbase@*/ |
885824d3 | 528 | if (cnew->type != CT_FCN && cnew->type != CT_EXPFCN) |
529 | { | |
530 | ctype i; | |
531 | int ctstop = cttable_lastIndex () - DEFAULT_OPTLEVEL; | |
532 | ||
533 | if (ctstop < LAST_PREDEFINED) | |
534 | { | |
535 | ctstop = LAST_PREDEFINED; | |
536 | } | |
537 | ||
538 | for (i = cttable_lastIndex (); i >= ctstop; i--) /* better to go from back... */ | |
539 | { | |
540 | ctbase ctb; | |
541 | ||
885824d3 | 542 | ctb = ctype_getCtbase (i); |
28bf4b0b | 543 | |
b73d1009 | 544 | /* is this optimization really worthwhile? */ |
885824d3 | 545 | |
546 | if (ctbase_isDefined (ctb) && ctbase_equivStrict (cnew, ctb)) | |
547 | { | |
a0a162cd | 548 | DPRINTF (("EQUIV!! %s / %s", |
549 | ctbase_unparse (cnew), | |
550 | ctbase_unparse (ctb))); | |
28bf4b0b | 551 | |
885824d3 | 552 | ctbase_free (cnew); |
885824d3 | 553 | return i; |
554 | } | |
555 | } | |
556 | } | |
557 | ||
558 | if (cttab.nspace == 0) | |
559 | cttable_grow (); | |
560 | ||
86d93ed3 | 561 | /*drl bee: si*/ cttab.entries[cttab.size] = ctentry_make (CTK_COMPLEX, cnew, ctype_undefined, |
885824d3 | 562 | ctype_dne, ctype_dne, |
563 | cstring_undefined); | |
564 | cttab.nspace--; | |
565 | ||
566 | return (cttab.size++); | |
28bf4b0b | 567 | /*@noaccess ctbase@*/ |
885824d3 | 568 | } |
569 | ||
570 | static ctype | |
571 | cttable_addFull (ctentry cnew) | |
572 | { | |
573 | if (cttab.nspace == 0) | |
574 | { | |
575 | cttable_grow (); | |
576 | } | |
577 | ||
86d93ed3 | 578 | /*drl bee: si*/ cttab.entries[cttab.size] = cnew; |
885824d3 | 579 | cttab.nspace--; |
580 | ||
581 | return (cttab.size++); | |
582 | } | |
583 | ||
584 | static ctype | |
585 | cttable_addFullSafe (/*@only@*/ ctentry cnew) | |
586 | { | |
587 | int i; | |
588 | ctbase cnewbase = cnew->ctbase; | |
589 | ||
590 | llassert (ctbase_isDefined (cnewbase)); | |
591 | ||
592 | for (i = cttable_lastIndex (); i >= CT_FIRST; i--) | |
593 | { | |
594 | ctbase ctb = ctype_getCtbase (i); | |
595 | ||
596 | if (ctbase_isDefined (ctb) | |
597 | && ctbase_equiv (cnewbase, ctype_getCtbaseSafe (i))) | |
598 | { | |
599 | ctentry_free (cnew); | |
600 | return i; | |
601 | } | |
602 | } | |
603 | ||
604 | if (cttab.nspace == 0) | |
605 | cttable_grow (); | |
606 | ||
86d93ed3 | 607 | /*drl bee: si*/ cttab.entries[cttab.size] = cnew; |
885824d3 | 608 | |
609 | cttab.nspace--; | |
610 | ||
611 | return (cttab.size++); | |
612 | } | |
613 |