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