/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** 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 splint: splint@cs.virginia.edu
-** To report a bug: splint-bug@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
*/
/*
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)
{
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);
}
}
}
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
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)