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
++);