src/functionConstraint.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2002 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 lclint: lclint-request@cs.virginia.edu
  21 ** To report a bug: lclint-bug@cs.virginia.edu
  22 ** For more information: http://www.splint.org
  23 */
  24 /*
  25 ** functionConstraint.c
  26 */
  27
  28 # include "lclintMacros.nf"
  29 # include "basic.h"
  30
  31 static /*@only@*/ /*@notnull@*/ /*@special@*/ functionConstraint  /*@i32 need special? @*/
  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           return constraintList_addListFree (functionConstraint_getBufferConstraints (node->constraint.conjunct.op1),
  95                                              functionConstraint_getBufferConstraints (node->constraint.conjunct.op2));
  96         }
  97       else
  98         {
  99           if (node->kind == FCT_BUFFER)
 100             {
 101               return constraintList_copy (node->constraint.buffer);
 102             }
 103           else
 104             {
 105               return constraintList_undefined;
 106             }
 107         }
 108     }
 109   else
 110     {
 111       return constraintList_undefined;
 112     }
 113 }
 114
 115 extern metaStateConstraintList functionConstraint_getMetaStateConstraints (functionConstraint node)
 116 {
 117   if (functionConstraint_isDefined (node))
 118     {
 119       if (node->kind == FCT_CONJUNCT)
 120         {
 121           return metaStateConstraintList_append
 122             (functionConstraint_getMetaStateConstraints (node->constraint.conjunct.op1),
 123              functionConstraint_getMetaStateConstraints (node->constraint.conjunct.op2));
 124         }
 125       else
 126         {
 127           if (node->kind == FCT_METASTATE)
 128             {
 129               return metaStateConstraintList_single (node->constraint.metastate);
 130             }
 131           else
 132             {
 133               return metaStateConstraintList_undefined;
 134             }
 135         }
 136     }
 137   else
 138     {
 139       return metaStateConstraintList_undefined;
 140     }
 141 }
 142
 143 extern bool functionConstraint_hasBufferConstraint (functionConstraint node)
 144 {
 145   if (functionConstraint_isDefined (node))
 146     {
 147       return node->kind == FCT_BUFFER
 148         || (node->kind == FCT_CONJUNCT
 149             && (functionConstraint_hasBufferConstraint (node->constraint.conjunct.op1)
 150                 || functionConstraint_hasBufferConstraint (node->constraint.conjunct.op2)));
 151     }
 152   else
 153     {
 154       return FALSE;
 155     }
 156 }
 157
 158 extern bool functionConstraint_hasMetaStateConstraint (functionConstraint node)
 159 {
 160   if (functionConstraint_isDefined (node))
 161     {
 162       return node->kind == FCT_METASTATE
 163         || (node->kind == FCT_CONJUNCT
 164             && (functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op1)
 165                 || functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op2)));
 166     }
 167   else
 168     {
 169       return FALSE;
 170     }
 171 }
 172
 173 extern functionConstraint functionConstraint_copy (functionConstraint node)
 174 {
 175   if (functionConstraint_isDefined (node))
 176     {
 177       switch (node->kind)
 178         {
 179         case FCT_BUFFER:
 180           return functionConstraint_createBufferConstraint (constraintList_copy (node->constraint.buffer));
 181         case FCT_METASTATE:
 182           return functionConstraint_createMetaStateConstraint (metaStateConstraint_copy (node->constraint.metastate));
 183         case FCT_CONJUNCT:
 184           return functionConstraint_conjoin (functionConstraint_copy (node->constraint.conjunct.op1),
 185                                              functionConstraint_copy (node->constraint.conjunct.op2));
 186         }
 187
 188       BADBRANCH;
 189     }
 190   else
 191     {
 192       return functionConstraint_undefined;
 193     }
 194
 195   BADBRANCHRET (functionConstraint_undefined);
 196 }
 197
 198 extern void functionConstraint_free (/*@only@*/ functionConstraint node)
 199 {
 200   if (functionConstraint_isDefined (node))
 201     {
 202       switch (node->kind)
 203         {
 204         case FCT_BUFFER:
 205           constraintList_free (node->constraint.buffer);
 206           break;
 207         case FCT_METASTATE:
 208           metaStateConstraint_free (node->constraint.metastate);
 209           break;
 210         case FCT_CONJUNCT:
 211           functionConstraint_free (node->constraint.conjunct.op1);
 212           functionConstraint_free (node->constraint.conjunct.op2);
 213           break;
 214         BADDEFAULT;
 215         }
 216
 217       sfree (node);
 218     }
 219 }
 220
 221
 222
 223
 224
 225
 226
 227
 228