src/functionClause.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 ** functionClause.c
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30
  31 static /*@only@*/ /*@notnull@*/ /*@special@*/ functionClause  /*@i32 need special? @*/
  32 functionClause_alloc (functionClauseKind kind) /*@defines result->kind@*/
  33 {
  34   functionClause res = (functionClause) dmalloc (sizeof (*res));
  35
  36   res->kind = kind;
  37   return res;
  38 }
  39
  40 extern functionClause functionClause_createGlobals (globalsClause node) /*@*/
  41 {
  42   functionClause res = functionClause_alloc (FCK_GLOBALS);
  43   res->val.globals = node;
  44   return res;
  45 }
  46
  47 extern functionClause functionClause_createModifies (modifiesClause node) /*@*/
  48 {
  49   functionClause res = functionClause_alloc (FCK_MODIFIES);
  50   res->val.modifies = node;
  51   return res;
  52 }
  53
  54 extern functionClause functionClause_createState (stateClause node) /*@*/
  55 {
  56   if (stateClause_hasEmptyReferences (node) &&
  57       (!stateClause_isMetaState (node) ) )
  58     {
  59       DPRINTF((message("functionClause_createState:: Returning functionClause_undefined" ) ));
  60       return functionClause_undefined;
  61     }
  62   else
  63     {
  64       functionClause res = functionClause_alloc (FCK_STATE);
  65       res->val.state = node;
  66       return res;
  67     }
  68 }
  69
  70 extern functionClause functionClause_createEnsures (functionConstraint node) /*@*/
  71 {
  72   functionClause res = functionClause_alloc (FCK_ENSURES);
  73   res->val.constraint = node;
  74   return res;
  75 }
  76
  77 extern functionClause functionClause_createRequires (functionConstraint node) /*@*/
  78 {
  79   functionClause res = functionClause_alloc (FCK_REQUIRES);
  80   res->val.constraint = node;
  81   return res;
  82 }
  83
  84 extern functionClause functionClause_createWarn (warnClause node) /*@*/
  85 {
  86   functionClause res = functionClause_alloc (FCK_WARN);
  87   res->val.warn = node;
  88   return res;
  89 }
  90
  91 /*@only@*/ cstring functionClause_unparse (functionClause p)
  92 {
  93   if (functionClause_isUndefined (p))
  94     {
  95       return cstring_undefined;
  96     }
  97
  98   switch (p->kind)
  99     {
 100     case FCK_GLOBALS:
 101       return globalsClause_unparse (p->val.globals);
 102     case FCK_MODIFIES:
 103       return modifiesClause_unparse (p->val.modifies);
 104     case FCK_WARN:
 105       return warnClause_unparse (p->val.warn);
 106     case FCK_STATE:
 107       return stateClause_unparse (p->val.state);
 108     case FCK_ENSURES:
 109       return message ("ensures %q", functionConstraint_unparse (p->val.constraint));
 110     case FCK_REQUIRES:
 111       return message ("requires %q", functionConstraint_unparse (p->val.constraint));
 112     case FCK_DEAD:
 113       return cstring_makeLiteral ("<dead clause>");
 114     }
 115
 116   BADBRANCHRET (cstring_undefined);
 117 }
 118
 119 extern bool functionClause_matchKind (functionClause p, functionClauseKind kind) /*@*/
 120 {
 121   if (functionClause_isDefined (p))
 122     {
 123       return (p->kind == kind);
 124     }
 125   else
 126     {
 127       return FALSE;
 128     }
 129 }
 130
 131 extern stateClause functionClause_getState (functionClause node)
 132 {
 133   llassert (functionClause_isDefined (node));
 134   llassert (node->kind == FCK_STATE);
 135
 136   return node->val.state;
 137 }
 138
 139 extern stateClause functionClause_takeState (functionClause fc)
 140 {
 141   stateClause res;
 142   llassert (functionClause_isDefined (fc));
 143   llassert (fc->kind == FCK_STATE);
 144
 145   res = fc->val.state;
 146   fc->val.state = NULL;
 147   fc->kind = FCK_DEAD;
 148   return res;
 149 }
 150
 151 extern functionConstraint functionClause_getEnsures (functionClause node)
 152 {
 153   llassert (functionClause_isDefined (node));
 154   llassert (node->kind == FCK_ENSURES);
 155
 156   return node->val.constraint;
 157 }
 158
 159 extern functionConstraint functionClause_takeEnsures (functionClause fc)
 160 {
 161   functionConstraint res;
 162   llassert (functionClause_isDefined (fc));
 163   llassert (fc->kind == FCK_ENSURES);
 164
 165   res = fc->val.constraint;
 166   fc->val.constraint = NULL;
 167   fc->kind = FCK_DEAD;
 168   return res;
 169 }
 170
 171 extern functionConstraint functionClause_getRequires (functionClause node)
 172 {
 173   llassert (functionClause_isDefined (node));
 174   llassert (node->kind == FCK_REQUIRES);
 175
 176   return node->val.constraint;
 177 }
 178
 179 extern functionConstraint functionClause_takeRequires (functionClause fc)
 180 {
 181   functionConstraint res;
 182   llassert (functionClause_isDefined (fc));
 183   llassert (fc->kind == FCK_REQUIRES);
 184
 185   res = fc->val.constraint;
 186   fc->val.constraint = NULL;
 187   fc->kind = FCK_DEAD;
 188   return res;
 189 }
 190
 191 extern warnClause functionClause_getWarn (functionClause node)
 192 {
 193   llassert (functionClause_isDefined (node));
 194   llassert (node->kind == FCK_WARN);
 195
 196   return node->val.warn;
 197 }
 198
 199 extern warnClause functionClause_takeWarn (functionClause fc)
 200 {
 201   warnClause res;
 202   llassert (functionClause_isDefined (fc));
 203   llassert (fc->kind == FCK_WARN);
 204
 205   res = fc->val.warn;
 206   fc->val.warn = warnClause_undefined;
 207   fc->kind = FCK_DEAD;
 208   return res;
 209 }
 210
 211 extern modifiesClause functionClause_getModifies (functionClause node)
 212 {
 213   llassert (functionClause_isDefined (node));
 214   llassert (node->kind == FCK_MODIFIES);
 215
 216   return node->val.modifies;
 217 }
 218
 219 extern globalsClause functionClause_getGlobals (functionClause node)
 220 {
 221   llassert (functionClause_isDefined (node));
 222   llassert (node->kind == FCK_GLOBALS);
 223
 224   return node->val.globals;
 225 }
 226
 227 extern void functionClause_free (/*@only@*/ functionClause node)
 228 {
 229   if (node != NULL)
 230     {
 231       DPRINTF (("free: %s", functionClause_unparse (node)));
 232
 233       switch (node->kind)
 234         {
 235         case FCK_GLOBALS:
 236           globalsClause_free (node->val.globals);
 237           break;
 238         case FCK_MODIFIES:
 239           modifiesClause_free (node->val.modifies);
 240           break;
 241         case FCK_WARN:
 242           warnClause_free (node->val.warn);
 243           break;
 244         case FCK_STATE:
 245           stateClause_free (node->val.state);
 246           break;
 247         case FCK_ENSURES:
 248           functionConstraint_free (node->val.constraint);
 249           break;
 250         case FCK_REQUIRES:
 251           functionConstraint_free (node->val.constraint);
 252           break;
 253         case FCK_DEAD:
 254           /* Nothing to release */
 255           break;
 256         }
 257
 258       sfree (node);
 259     }
 260 }