src/functionConstraint.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 ** functionConstraint.c
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30
  31 static /*@only@*/ /*@notnull@*/ /*@special@*/ functionConstraint
  32 functionConstraint_alloc (functionConstraintKind kind) /*@defines result->kind@*/
  33 {
  34   functionConstraint res = (functionConstraint) dmalloc (sizeof (*res));
  35
  36   res->kind = kind;
  37   return res;
  38 }
  39
  40 extern functionConstraint functionConstraint_createBufferConstraint (constraintList buf)
  41 {
  42   functionConstraint res = functionConstraint_alloc (FCT_BUFFER);
  43   res->constraint.buffer = buf;
  44   return res;
  45 }
  46
  47 extern functionConstraint functionConstraint_createMetaStateConstraint (metaStateConstraint msc)
  48 {
  49   functionConstraint res = functionConstraint_alloc (FCT_METASTATE);
  50   res->constraint.metastate = msc;
  51   return res;
  52 }
  53
  54 extern functionConstraint functionConstraint_conjoin (functionConstraint f1, functionConstraint f2)
  55 {
  56   functionConstraint res = functionConstraint_alloc (FCT_CONJUNCT);
  57   res->constraint.conjunct.op1 = f1;
  58   res->constraint.conjunct.op2 = f2;
  59   DPRINTF (("Conjoining ==> %s",
  60             functionConstraint_unparse (res)));
  61   return res;
  62 }
  63
  64 /*@only@*/ cstring functionConstraint_unparse (functionConstraint p)
  65 {
  66   if (functionConstraint_isDefined (p))
  67     {
  68       switch (p->kind)
  69         {
  70         case FCT_BUFFER:
  71           return constraintList_unparse (p->constraint.buffer);
  72         case FCT_METASTATE:
  73           return metaStateConstraint_unparse (p->constraint.metastate);
  74         case FCT_CONJUNCT:
  75           return message ("%q /\\ %q",
  76                           functionConstraint_unparse (p->constraint.conjunct.op1),
  77                           functionConstraint_unparse (p->constraint.conjunct.op2));
  78           BADDEFAULT;
  79         }
  80       BADBRANCH;
  81     }
  82   else
  83     {
  84       return cstring_makeLiteral ("< empty constraint >");
  85     }
  86 }
  87
  88 extern constraintList functionConstraint_getBufferConstraints (functionConstraint node)
  89 {
  90   if (functionConstraint_isDefined (node))
  91     {
  92       if (node->kind == FCT_CONJUNCT)
  93         {
  94           /* make sure this is safe*/
  95           return constraintList_addListFree (functionConstraint_getBufferConstraints (node->constraint.conjunct.op1),
  96                                              functionConstraint_getBufferConstraints (node->constraint.conjunct.op2));
  97         }
  98       else
  99         {
 100           if (node->kind == FCT_BUFFER)
 101             {
 102               return constraintList_copy (node->constraint.buffer);
 103             }
 104           else
 105             {
 106               return constraintList_undefined;
 107             }
 108         }
 109     }
 110   else
 111     {
 112       return constraintList_undefined;
 113     }
 114 }
 115
 116 extern metaStateConstraintList functionConstraint_getMetaStateConstraints (functionConstraint node)
 117 {
 118   if (functionConstraint_isDefined (node))
 119     {
 120       if (node->kind == FCT_CONJUNCT)
 121         {
 122           return metaStateConstraintList_append
 123             (functionConstraint_getMetaStateConstraints (node->constraint.conjunct.op1),
 124              functionConstraint_getMetaStateConstraints (node->constraint.conjunct.op2));
 125         }
 126       else
 127         {
 128           if (node->kind == FCT_METASTATE)
 129             {
 130               return metaStateConstraintList_single (node->constraint.metastate);
 131             }
 132           else
 133             {
 134               return metaStateConstraintList_undefined;
 135             }
 136         }
 137     }
 138   else
 139     {
 140       return metaStateConstraintList_undefined;
 141     }
 142 }
 143
 144 extern bool functionConstraint_hasBufferConstraint (functionConstraint node)
 145 {
 146   if (functionConstraint_isDefined (node))
 147     {
 148       return node->kind == FCT_BUFFER
 149         || (node->kind == FCT_CONJUNCT
 150             && (functionConstraint_hasBufferConstraint (node->constraint.conjunct.op1)
 151                 || functionConstraint_hasBufferConstraint (node->constraint.conjunct.op2)));
 152     }
 153   else
 154     {
 155       return FALSE;
 156     }
 157 }
 158
 159 extern bool functionConstraint_hasMetaStateConstraint (functionConstraint node)
 160 {
 161   if (functionConstraint_isDefined (node))
 162     {
 163       return node->kind == FCT_METASTATE
 164         || (node->kind == FCT_CONJUNCT
 165             && (functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op1)
 166                 || functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op2)));
 167     }
 168   else
 169     {
 170       return FALSE;
 171     }
 172 }
 173
 174 extern functionConstraint functionConstraint_copy (functionConstraint node)
 175 {
 176   if (functionConstraint_isDefined (node))
 177     {
 178       switch (node->kind)
 179         {
 180         case FCT_BUFFER:
 181           return functionConstraint_createBufferConstraint (constraintList_copy (node->constraint.buffer));
 182         case FCT_METASTATE:
 183           return functionConstraint_createMetaStateConstraint (metaStateConstraint_copy (node->constraint.metastate));
 184         case FCT_CONJUNCT:
 185           return functionConstraint_conjoin (functionConstraint_copy (node->constraint.conjunct.op1),
 186                                              functionConstraint_copy (node->constraint.conjunct.op2));
 187         }
 188
 189       BADBRANCH;
 190     }
 191   else
 192     {
 193       return functionConstraint_undefined;
 194     }
 195
 196   BADBRANCHRET (functionConstraint_undefined);
 197 }
 198
 199 extern void functionConstraint_free (/*@only@*/ functionConstraint node)
 200 {
 201   if (functionConstraint_isDefined (node))
 202     {
 203       switch (node->kind)
 204         {
 205         case FCT_BUFFER:
 206           constraintList_free (node->constraint.buffer);
 207           break;
 208         case FCT_METASTATE:
 209           metaStateConstraint_free (node->constraint.metastate);
 210           break;
 211         case FCT_CONJUNCT:
 212           functionConstraint_free (node->constraint.conjunct.op1);
 213           functionConstraint_free (node->constraint.conjunct.op2);
 214           break;
 215         BADDEFAULT;
 216         }
 217
 218       sfree (node);
 219     }
 220 }
 221
 222 /*drl modified */
 223 void functionConstraint_addBufferConstraints (functionConstraint node, constraintList clist)
 224 {
 225   constraintList temp;
 226
 227   temp = constraintList_copy (clist);
 228
 229   if (functionConstraint_isDefined (node))
 230     {
 231       if (node->kind == FCT_CONJUNCT)
 232         {
 233           functionConstraint_addBufferConstraints (node->constraint.conjunct.op1, constraintList_copy(temp) );
 234           functionConstraint_addBufferConstraints (node->constraint.conjunct.op2,temp);
 235         }
 236       else
 237         {
 238           if (node->kind == FCT_BUFFER)
 239             {
 240               node->constraint.buffer = constraintList_addListFree(node->constraint.buffer, temp);
 241             }
 242           else
 243             {
 244               constraintList_free (temp);
 245               return;
 246             }
 247         }
 248     }
 249   else
 250     {
 251       constraintList_free (temp);
 252       return;
 253     }
 254 }