2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 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
25 ** stateCombinationTable.c
27 ** A stateCombinationTable is a mapping from keys to value tables.
30 # include "splintMacros.nf"
34 ** (key, value, value) => value
37 static stateEntry stateEntry_create (void)
39 stateEntry res = (stateEntry) dmalloc (sizeof (*res));
41 res->msg = cstring_undefined;
45 static cstring stateEntry_unparse (stateEntry e)
47 if (cstring_isDefined (e->msg))
49 return message ("[%d: %s]", e->value, e->msg);
53 return message ("%d", e->value);
57 stateCombinationTable stateCombinationTable_create (int size)
59 stateCombinationTable res = (stateCombinationTable) dmalloc (sizeof (*res));
63 res->rows = (stateRow *) dmalloc (sizeof (*(res->rows)) * size);
65 for (i = 0; i < size; i++)
69 res->rows[i] = (stateRow) dmalloc (sizeof (*res->rows[i]));
70 res->rows[i]->size = size;
72 /* Rows have an extra entry (for lose ref transfers) */
73 res->rows[i]->entries = (stateEntry *)
74 dmalloc (sizeof (*res->rows[i]->entries) * (size + 1));
76 for (j = 0; j < size + 1; j++)
78 stateEntry s = stateEntry_create ();
80 /* Default transfer changes no state and is permitted without error. */
83 llassert (cstring_isUndefined (s->msg));
85 /*@-usedef@*/ /*@i534 why necessary? */
86 res->rows[i]->entries[j] = s;
94 cstring stateCombinationTable_unparse (stateCombinationTable t)
97 cstring res = cstring_newEmpty ();
99 for (i = 0; i < t->size; i++)
103 for (j = 0; j < (t->size + 1); j++)
107 res = message ("%q[%d: ] %q", res, i,
108 stateEntry_unparse (t->rows[i]->entries[j]));
112 res = message ("%q . %q", res,
113 stateEntry_unparse (t->rows[i]->entries[j]));
117 res = cstring_appendChar (res, '\n');
123 static void stateEntry_free (/*@only@*/ stateEntry s)
125 cstring_free (s->msg);
129 static void stateRow_free (/*@only@*/ stateRow r)
133 for (i = 0; i < r->size + 1; i++) {
134 /*@i32@*/ stateEntry_free (r->entries[i]);
141 void stateCombinationTable_free (/*@only@*/ stateCombinationTable t)
145 for (i = 0; i < t->size; i++) {
146 /*@i32@*/ stateRow_free (t->rows[i]);
153 static /*@exposed@*/ stateEntry
154 stateCombintationTable_getEntry (stateCombinationTable h,
157 llassert (rkey < h->size);
158 llassert (ckey < h->size + 1);
160 return h->rows[rkey]->entries[ckey];
163 void stateCombinationTable_set (stateCombinationTable h,
164 int p_from, int p_to,
165 int value, cstring msg)
167 stateEntry entry = stateCombintationTable_getEntry (h, p_from, p_to);
169 llassert (entry != NULL);
171 entry->value = value;
172 llassert (cstring_isUndefined (entry->msg));
175 DPRINTF (("Set entry: [%p] %d / %d => %s", entry,
176 p_from, p_to, cstring_toCharsSafe (msg)));
181 ** Like set, but may already have value.
182 ** (Only different is error checking.)
185 void stateCombinationTable_update (stateCombinationTable h,
186 int p_from, int p_to,
187 int value, cstring msg)
189 stateEntry entry = stateCombintationTable_getEntry (h, p_from, p_to);
191 llassert (entry != NULL);
193 entry->value = value;
194 cstring_free (entry->msg);
197 DPRINTF (("Update entry: [%p] %d / %d => %s", entry,
198 p_from, p_to, cstring_toCharsSafe (msg)));
201 int stateCombinationTable_lookup (stateCombinationTable h, int p_from, int p_to, /*@out@*/ cstring *msg)
204 llassert (p_from != stateValue_error);
205 llassert (p_to != stateValue_error);
207 entry = stateCombintationTable_getEntry (h, p_from, p_to);
208 llassert (entry != NULL);
210 DPRINTF (("Lookup: %d / %d => %s [%p]",
211 p_from, p_to, cstring_toCharsSafe (entry->msg), entry));
213 /*@i32@*/ *msg = entry->msg;
218 stateCombinationTable_lookupLoseReference (stateCombinationTable h, int from,
219 /*@out@*/ /*@observer@*/ cstring *msg)
221 return stateCombinationTable_lookup (h, from, h->size, msg);