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 # include "mtincludes.h"
  31
  32 static /*@only@*/ /*@notnull@*/ /*@special@*/ functionConstraint  /*@i32 need special? @*/
  33 functionConstraint_alloc (functionConstraintKind kind) /*@defines result->kind@*/
  34 {
  35   functionConstraint res = (functionConstraint) dmalloc (sizeof (*res));
  36
  37   res->kind = kind;
  38   return res;
  39 }
  40
  41 extern functionConstraint functionConstraint_createBufferConstraint (constraintList buf)
  42 {
  43   functionConstraint res = functionConstraint_alloc (FCT_BUFFER);
  44   res->constraint.buffer = buf;
  45   return res;
  46 }
  47
  48 extern functionConstraint functionConstraint_createMetaStateConstraint (metaStateConstraint msc)
  49 {
  50   functionConstraint res = functionConstraint_alloc (FCT_METASTATE);
  51   res->constraint.metastate = msc;
  52   return res;
  53 }
  54
  55 extern functionConstraint functionConstraint_conjoin (functionConstraint f1, functionConstraint f2)
  56 {
  57   functionConstraint res = functionConstraint_alloc (FCT_CONJUNCT);
  58   res->constraint.conjunct.op1 = f1;
  59   res->constraint.conjunct.op2 = f2;
  60   DPRINTF (("Conjoining ==> %s",
  61             functionConstraint_unparse (res)));
  62   return res;
  63 }
  64
  65 /*@only@*/ cstring functionConstraint_unparse (functionConstraint p)
  66 {
  67   if (functionConstraint_isDefined (p))
  68     {
  69       switch (p->kind)
  70         {
  71         case FCT_BUFFER:
  72           return constraintList_unparse (p->constraint.buffer);
  73         case FCT_METASTATE:
  74           return metaStateConstraint_unparse (p->constraint.metastate);
  75         case FCT_CONJUNCT:
  76           return message ("%q /\\ %q",
  77                           functionConstraint_unparse (p->constraint.conjunct.op1),
  78                           functionConstraint_unparse (p->constraint.conjunct.op2));
  79           BADDEFAULT;
  80         }
  81       BADBRANCH;
  82     }
  83   else
  84     {
  85       return cstring_makeLiteral ("< empty constraint >");
  86     }
  87 }
  88
  89 extern constraintList functionConstraint_getBufferConstraint (functionConstraint node)
  90 {
  91   llassert (functionConstraint_isDefined (node));
  92
  93   if (node->kind == FCT_CONJUNCT)
  94     {
  95       if (functionConstraint_hasBufferConstraint (node->constraint.conjunct.op1))
  96         {
  97           return functionConstraint_getBufferConstraint (node->constraint.conjunct.op1);
  98         }
  99       else
 100         {
 101           llassert (functionConstraint_hasBufferConstraint (node->constraint.conjunct.op2));
 102           return functionConstraint_getBufferConstraint (node->constraint.conjunct.op2);
 103         }
 104     }
 105
 106   llassert (node->kind == FCT_BUFFER);
 107   return node->constraint.buffer;
 108 }
 109
 110 extern metaStateConstraint functionConstraint_getMetaStateConstraint (functionConstraint node)
 111 {
 112   llassert (functionConstraint_isDefined (node));
 113
 114   if (node->kind == FCT_CONJUNCT)
 115     {
 116       if (functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op1))
 117         {
 118           return functionConstraint_getMetaStateConstraint (node->constraint.conjunct.op1);
 119         }
 120       else
 121         {
 122           llassert (functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op2));
 123           return functionConstraint_getMetaStateConstraint (node->constraint.conjunct.op2);
 124         }
 125     }
 126
 127   llassert (node->kind == FCT_METASTATE);
 128   return node->constraint.metastate;
 129 }
 130
 131 extern bool functionConstraint_hasBufferConstraint (functionConstraint node)
 132 {
 133   if (functionConstraint_isDefined (node))
 134     {
 135       return node->kind == FCT_BUFFER
 136         || (node->kind == FCT_CONJUNCT
 137             && (functionConstraint_hasBufferConstraint (node->constraint.conjunct.op1)
 138                 || functionConstraint_hasBufferConstraint (node->constraint.conjunct.op2)));
 139     }
 140   else
 141     {
 142       return FALSE;
 143     }
 144 }
 145
 146 extern bool functionConstraint_hasMetaStateConstraint (functionConstraint node)
 147 {
 148   if (functionConstraint_isDefined (node))
 149     {
 150       return node->kind == FCT_METASTATE
 151         || (node->kind == FCT_CONJUNCT
 152             && (functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op1)
 153                 || functionConstraint_hasMetaStateConstraint (node->constraint.conjunct.op2)));
 154     }
 155   else
 156     {
 157       return FALSE;
 158     }
 159 }
 160
 161 extern functionConstraint functionConstraint_copy (functionConstraint node)
 162 {
 163   if (functionConstraint_isDefined (node))
 164     {
 165       switch (node->kind)
 166         {
 167         case FCT_BUFFER:
 168           return functionConstraint_createBufferConstraint (constraintList_copy (node->constraint.buffer));
 169         case FCT_METASTATE:
 170           return functionConstraint_createMetaStateConstraint (metaStateConstraint_copy (node->constraint.metastate));
 171         case FCT_CONJUNCT:
 172           return functionConstraint_conjoin (functionConstraint_copy (node->constraint.conjunct.op1),
 173                                              functionConstraint_copy (node->constraint.conjunct.op2));
 174         }
 175
 176       BADBRANCH;
 177     }
 178   else
 179     {
 180       return functionConstraint_undefined;
 181     }
 182 }
 183
 184 extern void functionConstraint_free (/*@only@*/ functionConstraint node)
 185 {
 186   if (functionConstraint_isDefined (node))
 187     {
 188       switch (node->kind)
 189         {
 190         case FCT_BUFFER:
 191           constraintList_free (node->constraint.buffer);
 192           break;
 193         case FCT_METASTATE:
 194           metaStateConstraint_free (node->constraint.metastate);
 195           break;
 196         case FCT_CONJUNCT:
 197           functionConstraint_free (node->constraint.conjunct.op1);
 198           functionConstraint_free (node->constraint.conjunct.op2);
 199           break;
 200         BADDEFAULT;
 201         }
 202
 203       sfree (node);
 204     }
 205 }
 206
 207
 208
 209
 210
 211
 212
 213
 214