]> andersk Git - splint.git/blame - src/cttable.i
Added the code for setBufferSize and setStringLegnth annotations.
[splint.git] / src / cttable.i
CommitLineData
885824d3 1/* ;-*-C-*-;
2** Copyright (c) Massachusetts Institute of Technology 1994-1998.
3** All Rights Reserved.
4** Unpublished rights reserved under the copyright laws of
5** the United States.
6**
7** THIS MATERIAL IS PROVIDED AS IS, WITH ABSOLUTELY NO WARRANTY EXPRESSED
8** OR IMPLIED. ANY USE IS AT YOUR OWN RISK.
9**
10** This code is distributed freely and may be used freely under the
11** following conditions:
12**
13** 1. This notice may not be removed or altered.
14**
15** 2. Works derived from this code are not distributed for
16** commercial gain without explicit permission from MIT
17** (for permission contact lclint-request@sds.lcs.mit.edu).
18*/
19/*
20** cttable.i
21**
22** NOTE: This is not a stand-alone source file, but is included in ctype.c.
23** (This is necessary becuase there is no other way in C to have a
24** hidden scope, besides at the file level.)
25*/
26
27/*@access ctype@*/
28
29/*
30** type definitions and forward declarations in ctbase.i
31*/
32
33static void
34ctentry_free (/*@only@*/ ctentry c)
35{
36 ctbase_free (c->ctbase);
37 cstring_free (c->unparse);
38 sfree (c);
39}
40
41static void cttable_reset (void)
42 /*@globals cttab@*/
43 /*@modifies cttab@*/
44{
45 if (cttab.entries != NULL)
46 {
47 int i;
48
49 for (i = 0; i < cttab.size; i++)
50 {
51 ctentry_free (cttab.entries[i]);
52 }
53
54 /*@-compdestroy@*/
55 sfree (cttab.entries);
56 /*@=compdestroy@*/
57
58 cttab.entries = NULL;
59 }
60
61 cttab.size = 0 ;
62 cttab.nspace = 0 ;
63}
64
65static /*@observer@*/ ctbase ctype_getCtbase (ctype c)
66{
67 /*@+enumint@*/
68 if (c >= 0 && c < cttab.size)
69 {
70 return (cttab.entries[c]->ctbase);
71 }
72 else
73 {
74 if (c == CTK_UNKNOWN)
75 llbuglit ("ctype_getCtbase: ctype unknown");
76 if (c == CTK_INVALID)
77 llbuglit ("ctype_getCtbase: ctype invalid");
78 if (c == CTK_DNE)
79 llbuglit ("ctype_getCtbase: ctype dne");
80 if (c == CTK_ELIPS)
81 llbuglit ("ctype_getCtbase: elips marker");
82
83 llfatalbug (message ("ctype_getCtbase: ctype out of range: %d", c));
84 BADEXIT;
85 }
86
87 /*@=enumint@*/
88}
89
90static /*@notnull@*/ /*@observer@*/ ctbase
91ctype_getCtbaseSafe (ctype c)
92{
93 ctbase res = ctype_getCtbase (c);
94
95 llassert (ctbase_isDefined (res));
96 return res;
97}
98
99/*
100** ctentry
101*/
102
103static ctentry
104ctype_getCtentry (ctype c)
105{
106 static /*@only@*/ ctentry errorEntry = NULL;
107
108 if (cttab.size == 0)
109 {
110 if (errorEntry == NULL)
111 {
112 errorEntry = ctentry_makeNew (CTK_UNKNOWN, ctbase_undefined);
113 }
114
115 return errorEntry;
116 }
117
118 /*@+enumint@*/
119 if (c >= CTK_PLAIN && c < cttab.size)
120 {
121 return (cttab.entries[c]);
122 }
123 else if (c == CTK_UNKNOWN)
124 llcontbuglit ("ctype_getCtentry: ctype unknown");
125 else if (c == CTK_INVALID)
126 llcontbuglit ("ctype_getCtentry: ctype invalid (ctype_undefined)");
127 else if (c == CTK_DNE)
128 llcontbuglit ("ctype_getCtentry: ctype dne");
129 else
130 llbug (message ("ctype_getCtentry: ctype out of range: %d", c));
131
132 return (cttab.entries[ctype_unknown]);
133 /*@=enumint@*/
134}
135
136static ctentry
137ctentry_makeNew (ctkind ctk, /*@only@*/ ctbase c)
138{
139
140 return (ctentry_make (ctk, c, ctype_dne, ctype_dne, ctype_dne, cstring_undefined));
141}
142
143static /*@only@*/ ctentry
144ctentry_make (ctkind ctk,
145 /*@keep@*/ ctbase c, ctype base,
146 ctype ptr, ctype array,
147 /*@keep@*/ cstring unparse) /*@*/
148{
149 ctentry cte = (ctentry) dmalloc (sizeof (*cte));
150 cte->kind = ctk;
151 cte->ctbase = c;
152 cte->base = base;
153 cte->ptr = ptr;
154 cte->array = array;
155 cte->unparse = unparse;
156 return cte;
157}
158
159static cstring
160ctentry_unparse (ctentry c)
161{
162 return (message
163 ("%20s [%d] [%d] [%d]",
164 (cstring_isDefined (c->unparse) ? c->unparse : cstring_makeLiteral ("<no name>")),
165 c->base,
166 c->ptr,
167 c->array));
168}
169
170static bool
171ctentry_isInteresting (ctentry c)
172{
173 return (cstring_isNonEmpty (c->unparse));
174}
175
176static /*@only@*/ cstring
177ctentry_dump (ctentry c)
178{
179 if (c->ptr == ctype_dne
180 && c->array == ctype_dne
181 && c->base == ctype_dne)
182 {
183 return (message ("%d %q&",
184 ctkind_toInt (c->kind),
185 ctbase_dump (c->ctbase)));
186 }
187 else if (c->base == ctype_undefined
188 && c->array == ctype_dne)
189 {
190 if (c->ptr == ctype_dne)
191 {
192 return (message ("%d %q!",
193 ctkind_toInt (c->kind),
194 ctbase_dump (c->ctbase)));
195 }
196 else
197 {
198 return (message ("%d %q^%d",
199 ctkind_toInt (c->kind),
200 ctbase_dump (c->ctbase),
201 c->ptr));
202 }
203 }
204 else if (c->ptr == ctype_dne
205 && c->array == ctype_dne)
206 {
207 return (message ("%d %q%d&",
208 ctkind_toInt (c->kind),
209 ctbase_dump (c->ctbase),
210 c->base));
211 }
212 else
213 {
214 return (message ("%d %q%d %d %d",
215 ctkind_toInt (c->kind),
216 ctbase_dump (c->ctbase),
217 c->base, c->ptr, c->array));
218 }
219}
220
221
222static /*@only@*/ ctentry
223ctentry_undump (/*@dependent@*/ char *s)
224{
225 int base, ptr, array;
226 ctkind kind;
227 ctbase ct;
228
229 kind = ctkind_fromInt (getInt (&s));
230 ct = ctbase_undump (&s);
231
232 if (optCheckChar (&s, '&'))
233 {
234 base = ctype_dne;
235 ptr = ctype_dne;
236 array = ctype_dne;
237 }
238 else if (optCheckChar (&s, '!'))
239 {
240 base = ctype_undefined;
241 ptr = ctype_dne;
242 array = ctype_dne;
243 }
244 else if (optCheckChar (&s, '^'))
245 {
246 base = ctype_undefined;
247 ptr = getInt (&s);
248 array = ctype_dne;
249 }
250 else
251 {
252 base = getInt (&s);
253
254 if (optCheckChar (&s, '&'))
255 {
256 ptr = ctype_dne;
257 array = ctype_dne;
258 }
259 else
260 {
261 ptr = getInt (&s);
262 array = getInt (&s);
263 }
264 }
265
266 /* can't unparse w/o typeTable */
267 return (ctentry_make (kind, ct, base, ptr, array, cstring_undefined));
268}
269
270static /*@observer@*/ cstring
271ctentry_doUnparse (ctentry c) /*@modifies c@*/
272{
273 if (cstring_isDefined (c->unparse))
274 {
275 return (c->unparse);
276 }
277 else
278 {
279 cstring s = ctbase_unparse (c->ctbase);
280
281 if (!cstring_isEmpty (s) && !cstring_containsChar (s, '<'))
282 {
283 c->unparse = s;
284 }
285 else
286 {
287 cstring_markOwned (s);
288 }
289
290 return (s);
291 }
292}
293
294static /*@observer@*/ cstring
295ctentry_doUnparseDeep (ctentry c)
296{
297 if (cstring_isDefined (c->unparse))
298 {
299 return (c->unparse);
300 }
301 else
302 {
303 c->unparse = ctbase_unparseDeep (c->ctbase);
304 return (c->unparse);
305 }
306}
307
308/*
309** cttable operations
310*/
311
312static /*@only@*/ cstring
313cttable_unparse (void)
314{
315 int i;
316 cstring s = cstring_undefined;
317
318 /*@access ctbase@*/
319 for (i = 0; i < cttab.size; i++)
320 {
321 ctentry cte = cttab.entries[i];
322 if (ctentry_isInteresting (cte))
323 {
324 if (ctbase_isUA (cte->ctbase))
325 {
326 s = message ("%s%d\t%q [%d]\n", s, i, ctentry_unparse (cttab.entries[i]),
327 cte->ctbase->contents.tid);
328 }
329 else
330 {
331 s = message ("%s%d\t%q\n", s, i, ctentry_unparse (cttab.entries[i]));
332 }
333 }
334 }
335 /*@noaccess ctbase@*/
336 return (s);
337}
338
339void
340cttable_print (void)
341{
342 int i;
343
344 /*@access ctbase@*/
345 for (i = 0; i < cttab.size; i++)
346 {
347 ctentry cte = cttab.entries[i];
348
349 if (ctentry_isInteresting (cte))
350 {
351 if (ctbase_isUA (cte->ctbase))
352 {
353 fprintf (g_msgstream, "%3d: %s [%d]\n", i,
354 cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i])),
355 cte->ctbase->contents.tid);
356 }
357 else
358 {
359 fprintf (g_msgstream, "%3d: %s\n", i,
360 cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i])));
361 }
362 }
363 else
364 {
365 /* fprintf (g_msgstream, "%3d: <no name>\n", i); */
366 }
367 }
368 /*@noaccess ctbase@*/
369}
370
371/*
372** cttable_dump
373**
374** Output cttable for dump file
375*/
376
377static void
378cttable_dump (FILE *fout)
379{
380 bool showdots = FALSE;
381 int showdotstride = 0;
382 int i;
383
384 if (context_getFlag (FLG_SHOWSCAN) && cttab.size > 5000)
385 {
386 fprintf (g_msgstream, " >\n"); /* end dumping to */
387 fprintf (g_msgstream, "< Dumping type table (%d types) ", cttab.size);
388 showdotstride = cttab.size / 5;
389 showdots = TRUE;
390 }
391
392 for (i = 0; i < cttab.size; i++)
393 {
394 cstring s;
395
396 s = ctentry_dump (cttab.entries[i]);
397 llassert (cstring_length (s) < MAX_DUMP_LINE_LENGTH);
398 fputline (fout, cstring_toCharsSafe (s));
399 cstring_free (s);
400
401 if (showdots && (i != 0 && ((i - 1) % showdotstride == 0)))
402 {
403 (void) fflush (g_msgstream);
404 fprintf (stderr, ".");
405 (void) fflush (stderr);
406 }
407 }
408
409 if (showdots)
410 {
411 fprintf (stderr, " >\n< Continuing dump ");
412 }
413
414 }
415
416/*
417** load cttable from init file
418*/
419
420static void cttable_load (FILE *f)
421 /*@globals cttab @*/
422 /*@modifies cttab, f @*/
423{
424 char *s = mstring_create (MAX_DUMP_LINE_LENGTH);
425 ctentry cte;
426
427 cttable_reset ();
428
429 while (fgets (s, MAX_DUMP_LINE_LENGTH, f) != NULL && *s == ';')
430 {
431 ;
432 }
433
434 if (mstring_length (s) == (MAX_DUMP_LINE_LENGTH - 1))
435 {
436 llbug (message ("Library line too long: %s\n", cstring_fromChars (s)));
437 }
438
439 while (s != NULL && *s != ';' && *s != '\0')
440 {
441 ctype ct;
442
443 cte = ctentry_undump (s);
444 ct = cttable_addFull (cte);
445
446 if (ctbase_isConj (cte->ctbase)
447 && !(cte->ctbase->contents.conj->isExplicit))
448 {
449 ctype_recordConj (ct);
450 }
451
452 (void) fgets (s, MAX_DUMP_LINE_LENGTH, f);
453 }
454
455 sfree (s);
456 }
457
458/*
459** cttable_init
460**
461** fill up the cttable with basic types, and first order derivations.
462** this is done without using our constructors for efficiency reasons
463** (probably bogus)
464**
465*/
466
467/*@access cprim@*/
468static void cttable_init (void)
469 /*@globals cttab@*/ /*@modifies cttab@*/
470{
471 ctkind i;
472 cprim j;
473 ctbase ct = ctbase_undefined;
474
475 llassert (cttab.size == 0);
476
477 /* do for plain, pointer, arrayof */
478 for (i = CTK_PLAIN; i <= CTK_ARRAY; i++)
479 {
480 for (j = CTX_UNKNOWN; j <= CTX_LAST; j++)
481 {
482 if (i == CTK_PLAIN)
483 {
484 if (j == CTX_BOOL)
485 {
486 ct = ctbase_createBool (); /* why different? */
487 }
488 else if (j == CTX_UNKNOWN)
489 {
490 ct = ctbase_createUnknown ();
491 }
492 else
493 {
494 ct = ctbase_createPrim ((cprim)j);
495 }
496
497 (void) cttable_addFull
498 (ctentry_make (CTK_PLAIN,
499 ct, ctype_undefined,
500 j + CTK_PREDEFINED, j + CTK_PREDEFINED2,
501 ctbase_unparse (ct)));
502 }
503 else
504 {
505 switch (i)
506 {
507 case CTK_PTR:
508 ct = ctbase_makePointer (j);
509 /*@switchbreak@*/ break;
510 case CTK_ARRAY:
511 ct = ctbase_makeArray (j);
512 /*@switchbreak@*/ break;
513 default:
514 llbugexitlit ("cttable_init: base case");
515 }
516
517 (void) cttable_addDerived (i, ct, j);
518 }
519 }
520 }
521
522 /**** reserve a slot for userBool ****/
523 (void) cttable_addFull (ctentry_make (CTK_INVALID, ctbase_undefined,
524 ctype_undefined, ctype_dne, ctype_dne,
525 cstring_undefined));
526}
527
528/*@noaccess cprim@*/
529
530static void
531cttable_grow ()
532{
533 int i;
534 o_ctentry *newentries ;
535
536 cttab.nspace = CTK_BASESIZE;
537 newentries = (ctentry *) dmalloc (sizeof (*newentries) * (cttab.size + cttab.nspace));
538
539 if (newentries == NULL)
540 {
541 llfatalerror (message ("cttable_grow: out of memory. Size: %d",
542 cttab.size));
543 }
544
545 for (i = 0; i < cttab.size; i++)
546 {
547 newentries[i] = cttab.entries[i];
548 }
549
550 /*@-compdestroy@*/
551 sfree (cttab.entries);
552 /*@=compdestroy@*/
553
554 cttab.entries = newentries;
555/*@-compdef@*/
556} /*@=compdef@*/
557
558static ctype
559cttable_addDerived (ctkind ctk, /*@keep@*/ ctbase cnew, ctype base)
560{
561 if (cttab.nspace == 0)
562 cttable_grow ();
563
564 cttab.entries[cttab.size] =
565 ctentry_make (ctk, cnew, base, ctype_dne, ctype_dne, cstring_undefined);
566
567 cttab.nspace--;
568
569 return (cttab.size++);
570}
571
572static ctype
573cttable_addComplex (/*@only@*/ /*@notnull@*/ ctbase cnew)
574 /*@modifies cttab; @*/
575{
576 if (cnew->type != CT_FCN && cnew->type != CT_EXPFCN)
577 {
578 ctype i;
579 int ctstop = cttable_lastIndex () - DEFAULT_OPTLEVEL;
580
581 if (ctstop < LAST_PREDEFINED)
582 {
583 ctstop = LAST_PREDEFINED;
584 }
585
586 for (i = cttable_lastIndex (); i >= ctstop; i--) /* better to go from back... */
587 {
588 ctbase ctb;
589
590
591 ctb = ctype_getCtbase (i);
592
593 if (ctbase_isDefined (ctb) && ctbase_equivStrict (cnew, ctb))
594 {
595 ctbase_free (cnew);
596
597 return i;
598 }
599 }
600 }
601
602 if (cttab.nspace == 0)
603 cttable_grow ();
604
605 cttab.entries[cttab.size] = ctentry_make (CTK_COMPLEX, cnew, ctype_undefined,
606 ctype_dne, ctype_dne,
607 cstring_undefined);
608 cttab.nspace--;
609
610 return (cttab.size++);
611}
612
613static ctype
614cttable_addFull (ctentry cnew)
615{
616 if (cttab.nspace == 0)
617 {
618 cttable_grow ();
619 }
620
621 cttab.entries[cttab.size] = cnew;
622 cttab.nspace--;
623
624 return (cttab.size++);
625}
626
627static ctype
628cttable_addFullSafe (/*@only@*/ ctentry cnew)
629{
630 int i;
631 ctbase cnewbase = cnew->ctbase;
632
633 llassert (ctbase_isDefined (cnewbase));
634
635 for (i = cttable_lastIndex (); i >= CT_FIRST; i--)
636 {
637 ctbase ctb = ctype_getCtbase (i);
638
639 if (ctbase_isDefined (ctb)
640 && ctbase_equiv (cnewbase, ctype_getCtbaseSafe (i)))
641 {
642 ctentry_free (cnew);
643 return i;
644 }
645 }
646
647 if (cttab.nspace == 0)
648 cttable_grow ();
649
650 cttab.entries[cttab.size] = cnew;
651
652 cttab.nspace--;
653
654 return (cttab.size++);
655}
656
This page took 0.123879 seconds and 5 git commands to generate.