src/functionConstraint.c

   1 /*
   2 ** LCLint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2001 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://lclint.cs.virginia.edu
  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_getBufferConstraint (functionConstraint node)
  89 {
  90   llassert (functionConstraint_isDefined (node));
  91
  92   if (node->kind == FCT_CONJUNCT)
  93     {
  94       if (functionConstraint_hasBufferConstraint (node->constraint.conjunct.op1))
  95         {
  96           return functionConstraint_getBufferConstraint (node->constraint.conjunct.op1);
  97         }
  98       else
  99         {
 100           llassert (functionConstraint_hasBufferConstraint (node->constraint.conjunct.op2));
 101           return functionConstraint_getBufferConstraint (node->constraint.conjunct.op2);
 102         }
 103     }
 104
 105   llassert (node->kind == FCT_BUFFER);
 106   return node->constraint.buffer;
 107 }
 108
 109 extern metaStateConstraint functionConstraint_getMetaStateConstraint (functionConstraint node)
 110 {
 111   llassert (functionConstraint_isDefined (node));
 112
 113   if (node->kind == FCT_CONJUNCT)
 114     {
 115       if (functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op1))
 116         {
 117           return functionConstraint_getMetaStateConstraint (node->constraint.conjunct.op1);
 118         }
 119       else
 120         {
 121           llassert (functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op2));
 122           return functionConstraint_getMetaStateConstraint (node->constraint.conjunct.op2);
 123         }
 124     }
 125
 126   llassert (node->kind == FCT_METASTATE);
 127   return node->constraint.metastate;
 128 }
 129
 130 extern bool functionConstraint_hasBufferConstraint (functionConstraint node)
 131 {
 132   if (functionConstraint_isDefined (node))
 133     {
 134       return node->kind == FCT_BUFFER
 135         || (node->kind == FCT_CONJUNCT
 136             && (functionConstraint_hasBufferConstraint (node->constraint.conjunct.op1)
 137                 || functionConstraint_hasBufferConstraint (node->constraint.conjunct.op2)));
 138     }
 139   else
 140     {
 141       return FALSE;
 142     }
 143 }
 144
 145 extern bool functionConstraint_hasMetaStateConstraint (functionConstraint node)
 146 {
 147   if (functionConstraint_isDefined (node))
 148     {
 149       return node->kind == FCT_METASTATE
 150         || (node->kind == FCT_CONJUNCT
 151             && (functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op1)
 152                 || functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op2)));
 153     }
 154   else
 155     {
 156       return FALSE;
 157     }
 158 }
 159
 160 extern functionConstraint functionConstraint_copy (functionConstraint node)
 161 {
 162   if (functionConstraint_isDefined (node))
 163     {
 164       switch (node->kind)
 165         {
 166         case FCT_BUFFER:
 167           return functionConstraint_createBufferConstraint (constraintList_copy (node->constraint.buffer));
 168         case FCT_METASTATE:
 169           return functionConstraint_createMetaStateConstraint (metaStateConstraint_copy (node->constraint.metastate));
 170         case FCT_CONJUNCT:
 171           return functionConstraint_conjoin (functionConstraint_copy (node->constraint.conjunct.op1),
 172                                              functionConstraint_copy (node->constraint.conjunct.op2));
 173         }
 174
 175       BADBRANCH;
 176     }
 177   else
 178     {
 179       return functionConstraint_undefined;
 180     }
 181 }
 182
 183 extern void functionConstraint_free (/*@only@*/ functionConstraint node)
 184 {
 185   if (functionConstraint_isDefined (node))
 186     {
 187       switch (node->kind)
 188         {
 189         case FCT_BUFFER:
 190           constraintList_free (node->constraint.buffer);
 191           break;
 192         case FCT_METASTATE:
 193           metaStateConstraint_free (node->constraint.metastate);
 194           break;
 195         case FCT_CONJUNCT:
 196           functionConstraint_free (node->constraint.conjunct.op1);
 197           functionConstraint_free (node->constraint.conjunct.op2);
 198           break;
 199         BADDEFAULT;
 200         }
 201
 202       sfree (node);
 203     }
 204 }
 205
 206
 207
 208
 209
 210
 211
 212
 213