/* ;-*-C-*-;
-** Copyright (c) Massachusetts Institute of Technology 1994-1998.
-** All Rights Reserved.
-** Unpublished rights reserved under the copyright laws of
-** the United States.
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2003 University of Virginia,
+** Massachusetts Institute of Technology
**
-** THIS MATERIAL IS PROVIDED AS IS, WITH ABSOLUTELY NO WARRANTY EXPRESSED
-** OR IMPLIED. ANY USE IS AT YOUR OWN RISK.
+** This program is free software; you can redistribute it and/or modify it
+** under the terms of the GNU General Public License as published by the
+** Free Software Foundation; either version 2 of the License, or (at your
+** option) any later version.
+**
+** This program is distributed in the hope that it will be useful, but
+** WITHOUT ANY WARRANTY; without even the implied warranty of
+** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+** General Public License for more details.
+**
+** The GNU General Public License is available from http://www.gnu.org/ or
+** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+** MA 02111-1307, USA.
**
-** This code is distributed freely and may be used freely under the
-** following conditions:
-**
-** 1. This notice may not be removed or altered.
-**
-** 2. Works derived from this code are not distributed for
-** commercial gain without explicit permission from MIT
-** (for permission contact lclint-request@sds.lcs.mit.edu).
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
*/
/*
** cttable.i
for (i = 0; i < cttab.size; i++)
{
- ctentry_free (cttab.entries[i]);
+ /*drl bee: si*/ ctentry_free (cttab.entries[i]);
}
/*@-compdestroy@*/
cttab.nspace = 0 ;
}
-static /*@observer@*/ ctbase ctype_getCtbase (ctype c)
-{
- /*@+enumint@*/
- if (c >= 0 && c < cttab.size)
- {
- return (cttab.entries[c]->ctbase);
- }
- else
- {
- if (c == CTK_UNKNOWN)
- llbuglit ("ctype_getCtbase: ctype unknown");
- if (c == CTK_INVALID)
- llbuglit ("ctype_getCtbase: ctype invalid");
- if (c == CTK_DNE)
- llbuglit ("ctype_getCtbase: ctype dne");
- if (c == CTK_ELIPS)
- llbuglit ("ctype_getCtbase: elips marker");
-
- llfatalbug (message ("ctype_getCtbase: ctype out of range: %d", c));
- BADEXIT;
- }
-
- /*@=enumint@*/
-}
-
-static /*@notnull@*/ /*@observer@*/ ctbase
-ctype_getCtbaseSafe (ctype c)
-{
- ctbase res = ctype_getCtbase (c);
-
- llassert (ctbase_isDefined (res));
- return res;
-}
-
-/*
-** ctentry
-*/
-
-static ctentry
-ctype_getCtentry (ctype c)
-{
- static /*@only@*/ ctentry errorEntry = NULL;
-
- if (cttab.size == 0)
- {
- if (errorEntry == NULL)
- {
- errorEntry = ctentry_makeNew (CTK_UNKNOWN, ctbase_undefined);
- }
-
- return errorEntry;
- }
-
- /*@+enumint@*/
- if (c >= CTK_PLAIN && c < cttab.size)
- {
- return (cttab.entries[c]);
- }
- else if (c == CTK_UNKNOWN)
- llcontbuglit ("ctype_getCtentry: ctype unknown");
- else if (c == CTK_INVALID)
- llcontbuglit ("ctype_getCtentry: ctype invalid (ctype_undefined)");
- else if (c == CTK_DNE)
- llcontbuglit ("ctype_getCtentry: ctype dne");
- else if (c == CTK_ELIPS)
- llcontbuglit ("ctype_getCtentry: ctype elipsis");
- else if (c == CTK_MISSINGPARAMS)
- llcontbuglit ("ctype_getCtentry: ctype missing params");
- else
- llbug (message ("ctype_getCtentry: ctype out of range: %d", c));
-
- return (cttab.entries[ctype_unknown]);
- /*@=enumint@*/
-}
-
static ctentry
ctentry_makeNew (ctkind ctk, /*@only@*/ ctbase c)
{
static /*@only@*/ ctentry
-ctentry_undump (/*@dependent@*/ char *s)
+ctentry_undump (/*@dependent@*/ char *s) /*@requires maxRead(s) >= 2 @*/
{
int base, ptr, array;
ctkind kind;
ctbase ct;
- kind = ctkind_fromInt (getInt (&s));
+ kind = ctkind_fromInt (reader_getInt (&s));
ct = ctbase_undump (&s);
- if (optCheckChar (&s, '&'))
+ if (reader_optCheckChar (&s, '&'))
{
base = ctype_dne;
ptr = ctype_dne;
array = ctype_dne;
}
- else if (optCheckChar (&s, '!'))
+ else if (reader_optCheckChar (&s, '!'))
{
base = ctype_undefined;
ptr = ctype_dne;
array = ctype_dne;
}
- else if (optCheckChar (&s, '^'))
+ else if (reader_optCheckChar (&s, '^'))
{
base = ctype_undefined;
- ptr = getInt (&s);
+ ptr = reader_getInt (&s);
array = ctype_dne;
}
else
{
- base = getInt (&s);
+ base = reader_getInt (&s);
- if (optCheckChar (&s, '&'))
+ if (reader_optCheckChar (&s, '&'))
{
ptr = ctype_dne;
array = ctype_dne;
}
else
{
- ptr = getInt (&s);
- array = getInt (&s);
+ ptr = reader_getInt (&s);
+ array = reader_getInt (&s);
}
}
/*@access ctbase@*/
for (i = 0; i < cttab.size; i++)
{
- ctentry cte = cttab.entries[i];
+ /*drl bee: si*/ ctentry cte = cttab.entries[i];
if (ctentry_isInteresting (cte))
{
if (ctbase_isUA (cte->ctbase))
/*@access ctbase@*/
for (i = 0; i < cttab.size; i++)
{
- ctentry cte = cttab.entries[i];
+ /*drl bee: si*/ ctentry cte = cttab.entries[i];
- if (ctentry_isInteresting (cte))
+ if (TRUE) /* ctentry_isInteresting (cte)) */
{
if (ctbase_isUA (cte->ctbase))
{
- fprintf (g_msgstream, "%3d: %s [%d]\n", i,
+ fprintf (g_warningstream, "%3d: %s [%d]\n", i,
cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i])),
cte->ctbase->contents.tid);
}
else
{
- fprintf (g_msgstream, "%3d: %s\n", i,
+ fprintf (g_warningstream, "%3d: %s\n", i,
cstring_toCharsSafe (ctentry_doUnparse (cttab.entries[i])));
}
}
else
{
- /* fprintf (g_msgstream, "%3d: <no name>\n", i); */
+ /* fprintf (g_warningstream, "%3d: <no name>\n", i); */
}
}
/*@noaccess ctbase@*/
if (context_getFlag (FLG_SHOWSCAN) && cttab.size > 5000)
{
- fprintf (g_msgstream, " >\n"); /* end dumping to */
- fprintf (g_msgstream, "< Dumping type table (%d types) ", cttab.size);
+ displayScanClose ();
+ displayScanOpen (message ("Dumping type table (%d types)", cttab.size));
showdotstride = cttab.size / 5;
showdots = TRUE;
}
{
cstring s;
- s = ctentry_dump (cttab.entries[i]);
+ /*drl bee: si*/ s = ctentry_dump (cttab.entries[i]);
+ DPRINTF (("[%d] = %s", i, ctentry_unparse (cttab.entries[i])));
llassert (cstring_length (s) < MAX_DUMP_LINE_LENGTH);
fputline (fout, cstring_toCharsSafe (s));
cstring_free (s);
if (showdots && (i != 0 && ((i - 1) % showdotstride == 0)))
{
- (void) fflush (g_msgstream);
- fprintf (stderr, ".");
+ (void) fflush (g_warningstream);
+ displayScanContinue (cstring_makeLiteralTemp ("."));
(void) fflush (stderr);
}
}
if (showdots)
{
- fprintf (stderr, " >\n< Continuing dump ");
+ displayScanClose ();
+ displayScanOpen (cstring_makeLiteral ("Continuing dump "));
}
}
/*@modifies cttab, f @*/
{
char *s = mstring_create (MAX_DUMP_LINE_LENGTH);
+ char *os = s;
ctentry cte;
cttable_reset ();
- while (fgets (s, MAX_DUMP_LINE_LENGTH, f) != NULL && *s == ';')
+ /*
+ DPRINTF (("Loading cttable: "));
+ cttable_print ();
+ */
+
+ while (reader_readLine (f, s, MAX_DUMP_LINE_LENGTH) != NULL && *s == ';')
{
;
}
{
ctype ct;
- cte = ctentry_undump (s);
+ /*drl bee: tcf*/ cte = ctentry_undump (s);
ct = cttable_addFull (cte);
+ DPRINTF (("Type: %d: %s", ct, ctype_unparse (ct)));
+
if (ctbase_isConj (cte->ctbase)
- && !(cte->ctbase->contents.conj->isExplicit))
+ && !(ctbase_isExplicitConj (cte->ctbase)))
{
ctype_recordConj (ct);
}
- (void) fgets (s, MAX_DUMP_LINE_LENGTH, f);
+ s = reader_readLine (f, s, MAX_DUMP_LINE_LENGTH);
}
- sfree (s);
- }
+ sfree (os);
+
+ /*
+ DPRINTF (("Done loading cttable: "));
+ cttable_print ();
+ */
+}
/*
** cttable_init
for (i = 0; i < cttab.size; i++)
{
- newentries[i] = cttab.entries[i];
+ /*drl bee: dm*/ /*drl bee: si*/ newentries[i] = cttab.entries[i];
}
/*@-compdestroy@*/
if (cttab.nspace == 0)
cttable_grow ();
- cttab.entries[cttab.size] =
+ /*drl bee: si*/ cttab.entries[cttab.size] =
ctentry_make (ctk, cnew, base, ctype_dne, ctype_dne, cstring_undefined);
cttab.nspace--;
}
static ctype
-cttable_addComplex (/*@only@*/ /*@notnull@*/ ctbase cnew)
+cttable_addComplex (/*@only@*/ ctbase cnew)
/*@modifies cttab; @*/
{
+ /*@access ctbase@*/
if (cnew->type != CT_FCN && cnew->type != CT_EXPFCN)
{
ctype i;
ctbase ctb;
ctb = ctype_getCtbase (i);
+
+ /* is this optimization really worthwhile? */
if (ctbase_isDefined (ctb) && ctbase_equivStrict (cnew, ctb))
{
DPRINTF (("EQUIV!! %s / %s",
ctbase_unparse (cnew),
ctbase_unparse (ctb)));
+
ctbase_free (cnew);
return i;
}
if (cttab.nspace == 0)
cttable_grow ();
- cttab.entries[cttab.size] = ctentry_make (CTK_COMPLEX, cnew, ctype_undefined,
+ /*drl bee: si*/ cttab.entries[cttab.size] = ctentry_make (CTK_COMPLEX, cnew, ctype_undefined,
ctype_dne, ctype_dne,
cstring_undefined);
cttab.nspace--;
return (cttab.size++);
+ /*@noaccess ctbase@*/
}
static ctype
cttable_grow ();
}
- cttab.entries[cttab.size] = cnew;
+ /*drl bee: si*/ cttab.entries[cttab.size] = cnew;
cttab.nspace--;
return (cttab.size++);
if (cttab.nspace == 0)
cttable_grow ();
- cttab.entries[cttab.size] = cnew;
+ /*drl bee: si*/ cttab.entries[cttab.size] = cnew;
cttab.nspace--;
andersk / splint.git / blobdiff