src/stateCombinationTable.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2003 University of Virginia,
   4 **         Massachusetts Institute of Technology
   5 **
   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.
  10 **
  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.
  15 **
  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.
  19 **
  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
  23 */
  24 /*
  25 ** stateCombinationTable.c
  26 **
  27 ** A stateCombinationTable is a mapping from keys to value tables.
  28 */
  29
  30 # include "splintMacros.nf"
  31 # include "basic.h"
  32
  33 /*
  34 ** (key, value, value) => value
  35 */
  36
  37 static stateEntry stateEntry_create (void)
  38 {
  39   stateEntry res = (stateEntry) dmalloc (sizeof (*res));
  40   res->value = 0;
  41   res->msg = cstring_undefined;
  42   return res;
  43 }
  44
  45 static cstring stateEntry_unparse (stateEntry e)
  46 {
  47   if (cstring_isDefined (e->msg))
  48     {
  49       return message ("[%d: %s]", e->value, e->msg);
  50     }
  51   else
  52     {
  53       return message ("%d", e->value);
  54     }
  55 }
  56
  57 stateCombinationTable stateCombinationTable_create (int size)
  58 {
  59   stateCombinationTable res = (stateCombinationTable) dmalloc (sizeof (*res));
  60   int i;
  61
  62   res->size = size;
  63   res->rows = (stateRow *) dmalloc (sizeof (*(res->rows)) * size);
  64
  65   for (i = 0; i < size; i++)
  66     {
  67       int j;
  68
  69       res->rows[i] = (stateRow) dmalloc (sizeof (*res->rows[i]));
  70       res->rows[i]->size = size;
  71
  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));
  75
  76       for (j = 0; j < size + 1; j++)
  77         {
  78           stateEntry s = stateEntry_create ();
  79
  80           /* Default transfer changes no state and is permitted without error. */
  81
  82           s->value = i;
  83           llassert (cstring_isUndefined (s->msg));
  84
  85           /*@-usedef@*/
  86           res->rows[i]->entries[j] = s;
  87           /*@=usedef@*/
  88         }
  89     }
  90
  91   /*@-compmempass@*/ /*@-compdef@*/
  92   return res;
  93   /*@=compmempass@*/ /*@=compdef@*/
  94 }
  95
  96 cstring stateCombinationTable_unparse (stateCombinationTable t)
  97 {
  98   int i;
  99   cstring res = cstring_newEmpty ();
 100
 101   for (i = 0; i < t->size; i++)
 102     {
 103       int j;
 104
 105       for (j = 0; j < (t->size + 1); j++)
 106         {
 107           if (j == 0)
 108             {
 109               res = message ("%q[%d: ] %q", res, i,
 110                              stateEntry_unparse (t->rows[i]->entries[j]));
 111             }
 112           else
 113             {
 114               res = message ("%q . %q", res,
 115                              stateEntry_unparse (t->rows[i]->entries[j]));
 116             }
 117         }
 118
 119       res = cstring_appendChar (res, '\n');
 120     }
 121
 122   return res;
 123 }
 124
 125 static void stateEntry_free (/*@only@*/ stateEntry s)
 126 {
 127   cstring_free (s->msg);
 128   sfree (s);
 129 }
 130
 131 static void stateRow_free (/*@only@*/ stateRow r)
 132 {
 133   int i;
 134
 135   for (i = 0; i < r->size + 1; i++)
 136     {
 137       stateEntry_free (r->entries[i]);
 138     }
 139
 140   sfree (r->entries);
 141   sfree (r);
 142 }
 143
 144 void stateCombinationTable_free (/*@only@*/ stateCombinationTable t)
 145 {
 146   int i;
 147
 148   for (i = 0; i < t->size; i++) {
 149     stateRow_free (t->rows[i]);
 150   }
 151
 152   sfree (t->rows);
 153   sfree (t);
 154 }
 155
 156 static /*@exposed@*/ stateEntry
 157 stateCombintationTable_getEntry (stateCombinationTable h,
 158                                  int rkey, int ckey)
 159 {
 160   llassert (rkey < h->size);
 161   llassert (ckey < h->size + 1);
 162
 163   return h->rows[rkey]->entries[ckey];
 164 }
 165
 166 void stateCombinationTable_set (stateCombinationTable h,
 167                                 int p_from, int p_to,
 168                                 int value, cstring msg)
 169 {
 170   stateEntry entry = stateCombintationTable_getEntry (h, p_from, p_to);
 171
 172   llassert (entry != NULL);
 173
 174   entry->value = value;
 175   llassert (cstring_isUndefined (entry->msg));
 176   entry->msg = msg;
 177
 178   DPRINTF (("Set entry: [%p] %d / %d => %s", entry,
 179             p_from, p_to, cstring_toCharsSafe (msg)));
 180
 181 }
 182
 183 /*
 184 ** Like set, but may already have value.
 185 ** (Only different is error checking.)
 186 */
 187
 188 void stateCombinationTable_update (stateCombinationTable h,
 189                                    int p_from, int p_to,
 190                                    int value, cstring msg)
 191 {
 192   stateEntry entry = stateCombintationTable_getEntry (h, p_from, p_to);
 193
 194   llassert (entry != NULL);
 195
 196   entry->value = value;
 197   cstring_free (entry->msg);
 198   entry->msg = msg;
 199
 200   DPRINTF (("Update entry: [%p] %d / %d => %s", entry,
 201             p_from, p_to, cstring_toCharsSafe (msg)));
 202 }
 203
 204 int stateCombinationTable_lookup (stateCombinationTable h, int p_from, int p_to, /*@out@*/ ob_cstring *msg)
 205 {
 206   stateEntry entry;
 207   llassert (p_from != stateValue_error);
 208   llassert (p_to != stateValue_error);
 209
 210   entry = stateCombintationTable_getEntry (h, p_from, p_to);
 211   llassert (entry != NULL);
 212
 213   *msg = entry->msg;
 214   return entry->value;
 215 }
 216
 217 extern int
 218 stateCombinationTable_lookupLoseReference (stateCombinationTable h, int from,
 219                                            /*@out@*/ /*@observer@*/ cstring *msg)
 220 {
 221   return stateCombinationTable_lookup (h, from, h->size, msg);
 222 }
 223
 224
 225
 226
 227
 228