/*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2001 University of Virginia,
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
-** For information on lclint: lclint-request@cs.virginia.edu
-** To report a bug: lclint-bug@cs.virginia.edu
-** For more information: http://lclint.cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
*/
/*
** genericTable.c
** We sacrific type checking here for code reuse.
*/
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
# include "basic.h"
# include "randomNumbers.h"
/*@constant null ghbucket ghbucket_undefined; @*/
# define ghbucket_undefined 0
-static /*@truenull@*/ bool ghbucket_isNull (/*@null@*/ ghbucket h)
+static /*@nullwhentrue@*/ bool ghbucket_isNull (/*@null@*/ ghbucket h)
{
return (h == ghbucket_undefined);
}
return (h);
}
+static void
+ghentry_free (/*@only@*/ ghentry ghe)
+{
+ cstring_free (ghe->key);
+ /* can't free val contents */
+ sfree (ghe->val);
+ sfree (ghe);
+}
+
static bool
ghbucket_isEmpty (ghbucket h)
{
}
}
-static cstring
+# if 0
+static /*@unused@*/ cstring
ghbucket_unparse (ghbucket h)
{
cstring s = cstring_undefined;
return s;
}
+# endif
static ghbucket ghbucket_single (/*@keep@*/ ghentry e)
{
h->size = 1;
h->nspace = GHBUCKET_BASESIZE - 1;
h->entries = (ghentry *) dmalloc (GHBUCKET_BASESIZE * sizeof (*h->entries));
- /*@i23@*/ h->entries[0] = e;
+ h->entries[0] = e;
return (h);
}
newentries[i] = h->entries[i];
}
- /*@i32@*/ sfree (h->entries);
+ sfree (h->entries);
h->entries = newentries;
-/*@i32@*/ }
+ /*@-compmempass@*/
+} /*@=compmempass*/ /* Spurious warnings reported for h->entries */
static /*@null@*/ /*@exposed@*/ void *ghbucket_lookup (ghbucket p_h, cstring p_key);
static void
ghbucket_add (/*@notnull@*/ ghbucket h, /*@only@*/ ghentry e)
{
- void *exloc = ghbucket_lookup (h, e->key);
-
- if (exloc != NULL) {
- llassert (FALSE);
- }
-
- if (h->nspace == 0) {
- ghbucket_grow (h);
- }
-
- h->entries[h->size] = e;
- h->size++;
- h->nspace--;
-/*@i23@*/ }
+ void *exloc = ghbucket_lookup (h, e->key);
+
+ if (exloc != NULL) {
+ llcontbug (message ("ghbucket_add: adding duplicate entry: %s",
+ e->key));
+ ghentry_free (e);
+ return;
+ }
+
+ if (h->nspace == 0) {
+ ghbucket_grow (h);
+ }
+
+ h->entries[h->size] = e;
+ h->size++;
+ h->nspace--;
+}
static int
ghbucket_ncollisions (ghbucket h)
{
if (!ghbucket_isNull (h))
{
- /*@i32@*/ sfree (h->entries);
+ int i;
+
+ for (i = 0; i < h->size; i++)
+ {
+ ghentry_free (h->entries[i]);
+ }
+
+ sfree (h->entries);
sfree (h);
}
}
return h;
}
+# if 0
/*@-mustfree@*/
static /*@unused@*/ void
genericTable_print (genericTable h)
}
}
/*@=mustfree@*/
+# endif
/*@only@*/ cstring
genericTable_stats (genericTable h)
}
static void
-genericTable_addEntry (/*@notnull@*/ genericTable h, /*@keep@*/ ghentry e)
+genericTable_addEntry (/*@notnull@*/ genericTable h, /*@only@*/ ghentry e)
{
unsigned int hindex = genericTable_hashValue (h, e->key);
/*
}
else
{
- /*@i23@*/ ghbucket_add (h->buckets[hindex], e);
- /*@i23@*/ }
+ ghbucket_add (h->buckets[hindex], e);
+ }
}
void
genericTable_addEntry (h, bucket->entries[j]);
}
- sfree (bucket->entries); /* evans 2001-03-24: LCLint caught this */
+ sfree (bucket->entries); /* evans 2001-03-24: Splint caught this */
sfree (bucket);
}
}
if (ghbucket_isNull (hb))
{
- /*@i23@*/ h->buckets[hindex] = ghbucket_single (e);
+ h->buckets[hindex] = ghbucket_single (e);
}
else
{
- ghbucket_add (hb, e);
- /*@i23@*/ }
-/*@i23@*/ }
+ ghbucket_add (hb, e);
+ }
+}
/*@null@*/ /*@exposed@*/ void *
genericTable_lookup (genericTable h, cstring key)