src/functionClauseList.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 ** functionClauseList.c
  26 **
  27 ** based on list_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
  35 /*@constant int functionClauseListBASESIZE;@*/
  36 # define functionClauseListBASESIZE MIDBASESIZE
  37
  38 functionClauseList
  39 functionClauseList_new (void)
  40 {
  41   return functionClauseList_undefined;
  42 }
  43
  44 static /*@notnull@*/ functionClauseList
  45 functionClauseList_newEmpty (void)
  46 {
  47   functionClauseList s = (functionClauseList) dmalloc (sizeof (*s));
  48
  49   s->nelements = 0;
  50   s->nspace = functionClauseListBASESIZE;
  51   s->elements = (functionClause *) dmalloc (sizeof (*s->elements) * functionClauseListBASESIZE);
  52
  53   return (s);
  54 }
  55
  56 static void
  57 functionClauseList_grow (/*@notnull@*/ functionClauseList s)
  58 {
  59   int i;
  60   functionClause *newelements;
  61
  62   s->nspace += functionClauseListBASESIZE;
  63
  64   newelements = (functionClause *) dmalloc (sizeof (*newelements) * (s->nelements + s->nspace));
  65
  66   if (newelements == (functionClause *) 0)
  67     {
  68       llfatalerror (cstring_makeLiteral ("functionClauseList_grow: out of memory!"));
  69     }
  70
  71   for (i = 0; i < s->nelements; i++)
  72     {
  73       newelements[i] = s->elements[i];
  74     }
  75
  76   sfree (s->elements);
  77   s->elements = newelements;
  78 }
  79
  80 static functionClauseList functionClauseList_add (/*@returned@*/ functionClauseList s, /*@keep@*/ functionClause el)
  81   /*@modifies s@*/
  82 {
  83   if (!functionClauseList_isDefined (s))
  84     {
  85       s = functionClauseList_newEmpty ();
  86     }
  87
  88   if (s->nspace <= 0)
  89     {
  90       functionClauseList_grow (s);
  91     }
  92
  93   s->nspace--;
  94   s->elements[s->nelements] = el;
  95   s->nelements++;
  96
  97   return s;
  98 }
  99
 100 static /*@only@*/ functionClauseList functionClauseList_single (/*@keep@*/ functionClause el)
 101 {
 102   functionClauseList s = functionClauseList_new ();
 103   s = functionClauseList_add (s, el);
 104   return s;
 105 }
 106
 107 functionClauseList functionClauseList_prepend (functionClauseList s, /*@keep@*/ functionClause el)
 108 {
 109   int i;
 110
 111   if (!functionClauseList_isDefined (s))
 112     {
 113       return functionClauseList_single (el);
 114     }
 115
 116   if (s->nspace <= 0)
 117     {
 118       functionClauseList_grow (s);
 119     }
 120
 121   s->nspace--;
 122
 123   for (i = s->nelements; i > 0; i--)
 124     {
 125       s->elements[i] = s->elements [i - 1];
 126     }
 127
 128   s->elements[0] = el;
 129   s->nelements++;
 130
 131   return s;
 132 }
 133
 134 static cstring
 135 functionClauseList_unparseSep (functionClauseList s, cstring sep)
 136 {
 137    cstring st = cstring_undefined;
 138
 139    if (functionClauseList_isDefined (s))
 140      {
 141        int i;
 142
 143        for (i = 0; i < s->nelements; i++)
 144          {
 145            if (i == 0)
 146              {
 147                st = functionClause_unparse (s->elements[i]);
 148              }
 149            else
 150              st = message ("%q%s%q", st, sep, functionClause_unparse (s->elements[i]));
 151          }
 152      }
 153
 154    return st;
 155 }
 156
 157 cstring
 158 functionClauseList_unparse (functionClauseList s)
 159 {
 160   return functionClauseList_unparseSep (s, cstring_makeLiteralTemp (" "));
 161 }
 162
 163 void
 164 functionClauseList_free (functionClauseList s)
 165 {
 166   if (functionClauseList_isDefined (s))
 167     {
 168       int i;
 169
 170       for (i = 0; i < s->nelements; i++) {
 171         functionClause_free (s->elements[i]);
 172       }
 173
 174       sfree (s->elements);
 175       sfree (s);
 176     }
 177 }
 178
 179 functionClauseList
 180 functionClauseList_setImplicitConstraints (/*@returned@*/ functionClauseList s)
 181 {
 182   bool addedConstraints;
 183
 184   constraintList c;
 185
 186   DPRINTF ((message ("functionClauseList_setImplicitConstraints called ") ));
 187
 188   addedConstraints = FALSE;
 189
 190   c = getImplicitFcnConstraints ();
 191
 192   if (constraintList_isEmpty(c) )
 193     {
 194       return s;
 195     }
 196
 197   functionClauseList_elements(s, el)
 198     {
 199       if (functionClause_isRequires(el))
 200         {
 201           functionConstraint con = functionClause_getRequires(el);
 202
 203           if (functionConstraint_hasBufferConstraint(con))
 204             {
 205               if (functionConstraint_isBufferConstraint (con))
 206                 {
 207                   constraintList implCons = getImplicitFcnConstraints ();
 208
 209                   DPRINTF ((message ("functionClauseList_ImplicitConstraints adding the implict constraints: %s to %s",
 210                                      constraintList_unparse(implCons), constraintList_unparse (con->constraint.buffer))));
 211
 212                   functionConstraint_addBufferConstraints (con, constraintList_copy (implCons) );
 213
 214                   addedConstraints = TRUE;
 215
 216                   DPRINTF ((message ("functionClauseList_ImplicitConstraints the new constraint is %s",
 217                                      functionConstraint_unparse (con))));
 218
 219                 }
 220               else
 221                 {
 222                   llassert (FALSE);
 223                 }
 224             }
 225         }
 226     }
 227
 228   end_functionClauseList_elements;
 229
 230   if (!addedConstraints)
 231     {
 232       functionConstraint fCon;
 233       functionClause fClause;
 234
 235       constraintList implCons = getImplicitFcnConstraints ();
 236
 237       fCon = functionConstraint_createBufferConstraint(constraintList_copy (implCons) );
 238       fClause = functionClause_createRequires(fCon);
 239       s = functionClauseList_add(s, fClause);
 240
 241
 242     }
 243   return s;
 244 }