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 "llbasic.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@*/ /*@i534 why necessary? */
  86           res->rows[i]->entries[j] = s;
  87           /*@=usedef@*/
  88         }
  89     }
  90
  91   /*@i32@*/ return res;
  92 }
  93
  94 cstring stateCombinationTable_unparse (stateCombinationTable t)
  95 {
  96   int i;
  97   cstring res = cstring_newEmpty ();
  98
  99   for (i = 0; i < t->size; i++)
 100     {
 101       int j;
 102
 103       for (j = 0; j < (t->size + 1); j++)
 104         {
 105           if (j == 0)
 106             {
 107               res = message ("%q[%d: ] %q", res, i,
 108                              stateEntry_unparse (t->rows[i]->entries[j]));
 109             }
 110           else
 111             {
 112               res = message ("%q . %q", res,
 113                              stateEntry_unparse (t->rows[i]->entries[j]));
 114             }
 115         }
 116
 117       res = cstring_appendChar (res, '\n');
 118     }
 119
 120   return res;
 121 }
 122
 123 static void stateEntry_free (/*@only@*/ stateEntry s)
 124 {
 125   cstring_free (s->msg);
 126   sfree (s);
 127 }
 128
 129 static void stateRow_free (/*@only@*/ stateRow r)
 130 {
 131   int i;
 132
 133   for (i = 0; i < r->size + 1; i++) {
 134     /*@i32@*/ stateEntry_free (r->entries[i]);
 135   }
 136
 137   sfree (r->entries);
 138   sfree (r);
 139 }
 140
 141 void stateCombinationTable_free (/*@only@*/ stateCombinationTable t)
 142 {
 143   int i;
 144
 145   for (i = 0; i < t->size; i++) {
 146     /*@i32@*/ stateRow_free (t->rows[i]);
 147   }
 148
 149   sfree (t->rows);
 150   sfree (t);
 151 }
 152
 153 static /*@exposed@*/ stateEntry
 154 stateCombintationTable_getEntry (stateCombinationTable h,
 155                                  int rkey, int ckey)
 156 {
 157   llassert (rkey < h->size);
 158   llassert (ckey < h->size + 1);
 159
 160   return h->rows[rkey]->entries[ckey];
 161 }
 162
 163 void stateCombinationTable_set (stateCombinationTable h,
 164                                 int p_from, int p_to,
 165                                 int value, cstring msg)
 166 {
 167   stateEntry entry = stateCombintationTable_getEntry (h, p_from, p_to);
 168
 169   llassert (entry != NULL);
 170
 171   entry->value = value;
 172   llassert (cstring_isUndefined (entry->msg));
 173   entry->msg = msg;
 174
 175   DPRINTF (("Set entry: [%p] %d / %d => %s", entry,
 176             p_from, p_to, cstring_toCharsSafe (msg)));
 177
 178 }
 179
 180 /*
 181 ** Like set, but may already have value.
 182 ** (Only different is error checking.)
 183 */
 184
 185 void stateCombinationTable_update (stateCombinationTable h,
 186                                    int p_from, int p_to,
 187                                    int value, cstring msg)
 188 {
 189   stateEntry entry = stateCombintationTable_getEntry (h, p_from, p_to);
 190
 191   llassert (entry != NULL);
 192
 193   entry->value = value;
 194   cstring_free (entry->msg);
 195   entry->msg = msg;
 196
 197   DPRINTF (("Update entry: [%p] %d / %d => %s", entry,
 198             p_from, p_to, cstring_toCharsSafe (msg)));
 199 }
 200
 201 int stateCombinationTable_lookup (stateCombinationTable h, int p_from, int p_to, /*@out@*/ cstring *msg)
 202 {
 203   stateEntry entry;
 204   llassert (p_from != stateValue_error);
 205   llassert (p_to != stateValue_error);
 206
 207   entry = stateCombintationTable_getEntry (h, p_from, p_to);
 208   llassert (entry != NULL);
 209
 210   DPRINTF (("Lookup: %d / %d => %s [%p]",
 211             p_from, p_to, cstring_toCharsSafe (entry->msg), entry));
 212
 213   /*@i32@*/ *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