src/intSet.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 ** intSet.c
  26 **
  27 ** based on set_template.c
  28 **
  29 ** where T has T_equal (or change this) and T_unparse
  30 */
  31
  32 # include "splintMacros.nf"
  33 # include "basic.h"
  34 # include "intSet.h"
  35
  36 /*@only@*/ intSet
  37 intSet_new ()
  38 {
  39   intSet s = (intSet) dmalloc (sizeof (*s));
  40
  41   s->entries = 0;
  42   s->nspace = intSetBASESIZE;
  43   s->elements = (int *) dmalloc (sizeof (*s->elements) * intSetBASESIZE);
  44
  45   return (s);
  46 }
  47
  48 static void
  49 intSet_grow (intSet s)
  50 {
  51   int i;
  52   int *newelements;
  53
  54   s->nspace = intSetBASESIZE;
  55   newelements = (int *) dmalloc (sizeof (*newelements) * (s->entries + s->nspace));
  56
  57   for (i = 0; i < s->entries; i++)
  58     {
  59       newelements[i] = s->elements[i];
  60     }
  61
  62   sfree (s->elements);
  63   s->elements = newelements;
  64 }
  65
  66 /*
  67 ** Ensures: if *e \in *s
  68 **          then unchanged (*s) & result = false
  69 **          else *s' = insert (*s, *e) & result = true
  70 ** Modifies: *s
  71 */
  72
  73 bool
  74 intSet_insert (intSet s, int el)
  75 {
  76   int i;
  77
  78   for (i = 0; i < s->entries; i++)
  79     {
  80       if (s->elements[i] >= el)
  81         break;
  82     }
  83
  84   if (s->entries > 0 && s->elements[i] == el)
  85     {
  86       return FALSE;
  87     }
  88   else
  89     {
  90       if (s->nspace <= 0)
  91         intSet_grow (s);
  92
  93       s->nspace--;
  94
  95       if (i == (s->entries - 1))
  96         {
  97           s->elements[s->entries] = el;
  98         }
  99       else
 100         {
 101           int j;
 102
 103           for (j = s->entries; j > i; j--)
 104             {
 105               s->elements[j] = s->elements[j-1];
 106             }
 107           s->elements[i] = el;
 108         }
 109
 110       s->entries++;
 111       return TRUE;
 112     }
 113 }
 114
 115 bool
 116 intSet_member (intSet s, int el)
 117 {
 118   int i;
 119
 120   for (i = 0; i < s->entries; i++)
 121     {
 122       if (el == s->elements[i])
 123         {
 124           return TRUE;
 125         }
 126       if (el > s->elements[i])
 127         {
 128           return FALSE;
 129         }
 130     }
 131   return FALSE;
 132 }
 133
 134 /*@only@*/ cstring
 135 intSet_unparseText (intSet s)
 136 {
 137   int i;
 138   cstring st = cstring_undefined;
 139   int lastentry = s->entries - 1;
 140
 141   for (i = 0; i < s->entries; i++)
 142     {
 143       if (i == 0)
 144         st = message ("%d", s->elements[i]);
 145       else if (i == lastentry)
 146         st = message ("%q or %d", st, s->elements[i]);
 147       else
 148         st = message ("%q, %d", st, s->elements[i]);
 149     }
 150
 151   return st;
 152 }
 153
 154 /*@only@*/ cstring
 155 intSet_unparse (intSet s)
 156 {
 157   int i;
 158   cstring st = cstring_makeLiteral ("{");
 159
 160   for (i = 0; i < s->entries; i++)
 161     {
 162       st = message ("%q %d", st, s->elements[i]);
 163     }
 164
 165   st = message ("%q}", st);
 166   return st;
 167 }
 168
 169 void
 170 intSet_free (intSet s)
 171 {
 172   sfree (s->elements);
 173   sfree (s);
 174 }