src/metaStateConstraintList.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 ** metaStateConstraintList.c (from slist_template.c)
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30 # include "metaStateConstraintList.h"
  31
  32 /*
  33 ** Invariant:  If any member of the list is metaStateConstraint_undefined, then
  34 **             the 0th member is metaStateConstraint_undefined.
  35 */
  36
  37 metaStateConstraintList
  38 metaStateConstraintList_new ()
  39 {
  40   return (metaStateConstraintList_undefined);
  41 }
  42
  43 static /*@notnull@*/ /*@only@*/ metaStateConstraintList
  44 metaStateConstraintList_newEmpty (void)
  45 {
  46   metaStateConstraintList s = (metaStateConstraintList) dmalloc (sizeof (*s));
  47
  48   s->nelements = 0;
  49   s->free = metaStateConstraintListBASESIZE;
  50   s->elements = (metaStateConstraint *) dmalloc (sizeof (*s->elements) * metaStateConstraintListBASESIZE);
  51
  52   return (s);
  53 }
  54
  55 static void
  56 metaStateConstraintList_grow (/*@notnull@*/ metaStateConstraintList s)
  57 {
  58   int i;
  59   metaStateConstraint *oldelements = s->elements;
  60
  61   s->free += metaStateConstraintListBASESIZE;
  62   s->elements = (metaStateConstraint *) dmalloc (sizeof (*s->elements)
  63                                                  * (s->nelements + s->free));
  64
  65   for (i = 0; i < s->nelements; i++)
  66     {
  67       s->elements[i] = oldelements[i];
  68     }
  69
  70   sfree (oldelements);
  71 }
  72
  73 metaStateConstraintList
  74 metaStateConstraintList_append (/*@returned@*/ metaStateConstraintList s, /*@only@*/ metaStateConstraintList t)
  75 {
  76   llassert (NOALIAS (s, t));
  77
  78   if (metaStateConstraintList_isUndefined (t) || metaStateConstraintList_isEmpty (t)) return s;
  79
  80   if (metaStateConstraintList_isUndefined (s))
  81     {
  82       s = metaStateConstraintList_newEmpty ();
  83     }
  84
  85   metaStateConstraintList_elements (t, fl)
  86     {
  87       /* Okay to use exposed storage here, t is begin eaten. */
  88
  89       /*@-exposetrans@*/ /*@-dependenttrans@*/
  90       s = metaStateConstraintList_add (s, fl);
  91       /*@=exposetrans@*/ /*@=dependenttrans@*/
  92     } end_metaStateConstraintList_elements;
  93
  94   sfree (t->elements);
  95   sfree (t);
  96
  97   return s;
  98 }
  99
 100 metaStateConstraintList
 101 metaStateConstraintList_add (/*@returned@*/ metaStateConstraintList s, /*@observer@*/ metaStateConstraint el)
 102 {
 103   if (metaStateConstraintList_isUndefined (s))
 104     {
 105       s = metaStateConstraintList_newEmpty ();
 106     }
 107
 108   if (s->free <= 0)
 109     {
 110       metaStateConstraintList_grow (s);
 111     }
 112
 113   s->free--;
 114   s->elements[s->nelements] = el;
 115   s->nelements++;
 116
 117   return s;
 118 }
 119
 120 metaStateConstraintList
 121 metaStateConstraintList_single (metaStateConstraint el)
 122 {
 123   metaStateConstraintList res = metaStateConstraintList_newEmpty ();
 124   return metaStateConstraintList_add (res, el);
 125 }
 126
 127 metaStateConstraint
 128 metaStateConstraintList_getFirst (metaStateConstraintList s)
 129 {
 130   llassert (metaStateConstraintList_isDefined (s)
 131             && metaStateConstraintList_size (s) >= 1);
 132   return s->elements[0];
 133 }
 134
 135 /*@only@*/ cstring
 136 metaStateConstraintList_unparse (metaStateConstraintList s)
 137 {
 138    int i;
 139    cstring st = cstring_makeLiteral ("[");
 140
 141    if (metaStateConstraintList_isDefined (s))
 142      {
 143        for (i = 0; i < metaStateConstraintList_size (s); i++)
 144          {
 145            if (i == 0)
 146              {
 147                st = message ("%q %q", st, metaStateConstraint_unparse (s->elements[i]));
 148              }
 149            else
 150              st = message ("%q, %q", st, metaStateConstraint_unparse (s->elements[i]));
 151          }
 152      }
 153
 154    st = message ("%q ]", st);
 155    return st;
 156 }
 157
 158 void
 159 metaStateConstraintList_free (/*@only@*/ metaStateConstraintList s)
 160 {
 161   if (metaStateConstraintList_isDefined (s))
 162     {
 163       sfree (s->elements);
 164       sfree (s);
 165     }
 166 }
 167
 168
 169
 170
 171
 172