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