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