src/mtDeclarationPiece.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 ** mtDeclarationPiece.c
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30
  31 static mtDeclarationPiece
  32 mtDeclarationPiece_create (mtPieceKind kind, /*@null@*/ /*@only@*/ void *node)
  33 {
  34   mtDeclarationPiece res = (mtDeclarationPiece) dmalloc (sizeof (*res));
  35
  36   res->kind = kind;
  37   res->node = node;
  38
  39   /*@i32@*/ return res;
  40 }
  41
  42 extern mtDeclarationPiece mtDeclarationPiece_createContext (mtContextNode node) /*@*/
  43 {
  44   return mtDeclarationPiece_create (MTP_CONTEXT, (void *) node);
  45 }
  46
  47 extern mtDeclarationPiece mtDeclarationPiece_createValues (mtValuesNode node) /*@*/
  48 {
  49   return mtDeclarationPiece_create (MTP_VALUES, (void *) node);
  50 }
  51
  52 extern mtDeclarationPiece mtDeclarationPiece_createDefaults (mtDefaultsNode node) /*@*/
  53 {
  54   return mtDeclarationPiece_create (MTP_DEFAULTS, (void *) node);
  55 }
  56
  57 extern mtDeclarationPiece mtDeclarationPiece_createValueDefault (mttok node) /*@*/
  58 {
  59   llassert (mttok_isIdentifier (node));
  60   return mtDeclarationPiece_create (MTP_DEFAULTVALUE, (void *) node);
  61 }
  62
  63 extern mtDeclarationPiece mtDeclarationPiece_createAnnotations (mtAnnotationsNode node) /*@*/
  64 {
  65   return mtDeclarationPiece_create (MTP_ANNOTATIONS, (void *) node);
  66 }
  67
  68 extern mtDeclarationPiece mtDeclarationPiece_createMerge (mtMergeNode node) /*@*/
  69 {
  70   return mtDeclarationPiece_create (MTP_MERGE, (void *) node);
  71 }
  72
  73 extern mtDeclarationPiece mtDeclarationPiece_createTransfers (mtTransferClauseList node) /*@*/
  74 {
  75   return mtDeclarationPiece_create (MTP_TRANSFERS, (void *) node);
  76 }
  77
  78 extern mtDeclarationPiece mtDeclarationPiece_createPreconditions (mtTransferClauseList node) /*@*/
  79 {
  80   return mtDeclarationPiece_create (MTP_PRECONDITIONS, (void *) node);
  81 }
  82
  83 mtDeclarationPiece mtDeclarationPiece_createPostconditions (mtTransferClauseList node) /*@*/
  84 {
  85   return mtDeclarationPiece_create (MTP_POSTCONDITIONS, (void *) node);
  86 }
  87
  88 mtDeclarationPiece mtDeclarationPiece_createLosers (mtLoseReferenceList node) /*@*/
  89 {
  90   return mtDeclarationPiece_create (MTP_LOSERS, (void *) node);
  91 }
  92
  93 /*@only@*/ cstring mtDeclarationPiece_unparse (mtDeclarationPiece p)
  94 {
  95   if (mtDeclarationPiece_isUndefined (p))
  96     {
  97       return cstring_undefined;
  98     }
  99
 100   switch (p->kind)
 101     {
 102     case MTP_CONTEXT:
 103       /*@access mtContextNode@*/
 104       return mtContextNode_unparse ((mtContextNode) p->node);
 105       /*@noaccess mtContextNode@*/
 106     case MTP_VALUES:
 107       /*@access mtValuesNode@*/
 108       return mtValuesNode_unparse ((mtValuesNode) p->node);
 109       /*@noaccess mtValuesNode@*/
 110     case MTP_DEFAULTS:
 111       /*@access mtDefaultsNode@*/
 112       return mtDefaultsNode_unparse ((mtDefaultsNode) p->node);
 113       /*@noaccess mtDefaultsNode@*/
 114     case MTP_DEFAULTVALUE:
 115       /*@access mttok@*/
 116       return message ("default %q", mttok_getText ((mttok) p->node));
 117       /*@noaccess mttok@*/
 118     case MTP_ANNOTATIONS:
 119       /*@access mtAnnotationsNode@*/
 120       return mtAnnotationsNode_unparse ((mtAnnotationsNode) p->node);
 121       /*@noaccess mtAnnotationsNode@*/
 122     case MTP_MERGE:
 123       /*@access mtMergeNode@*/
 124       return mtMergeNode_unparse ((mtMergeNode) p->node);
 125       /*@noaccess mtMergeNode@*/
 126     case MTP_TRANSFERS:
 127     case MTP_PRECONDITIONS:
 128     case MTP_POSTCONDITIONS:
 129       /*@access mtTransferClauseList@*/
 130       return mtTransferClauseList_unparse ((mtTransferClauseList) p->node);
 131       /*@noaccess mtTransferClauseList@*/
 132     case MTP_LOSERS:
 133       /*@access mtLoseReferenceList@*/
 134       return mtLoseReferenceList_unparse ((mtLoseReferenceList) p->node);
 135       /*@noaccess mtLoseReferenceList@*/
 136     case MTP_DEAD:
 137       return cstring_makeLiteral ("Dead Piece");
 138     }
 139
 140   BADBRANCHRET (cstring_undefined);
 141 }
 142
 143 extern bool mtDeclarationPiece_matchKind (mtDeclarationPiece p, mtPieceKind kind) /*@*/
 144 {
 145   if (mtDeclarationPiece_isDefined (p))
 146     {
 147       return (p->kind == kind);
 148     }
 149   else
 150     {
 151       return FALSE;
 152     }
 153 }
 154
 155 extern mtContextNode mtDeclarationPiece_getContext (mtDeclarationPiece node)
 156 {
 157   llassert (mtDeclarationPiece_isDefined (node));
 158   llassert (node->kind == MTP_CONTEXT);
 159
 160   /*@-abstract@*/
 161   return (mtContextNode) node->node;
 162   /*@=abstract@*/
 163 }
 164
 165 extern mtContextNode mtDeclarationPiece_stealContext (mtDeclarationPiece node)
 166 {
 167   mtContextNode res;
 168
 169   llassert (mtDeclarationPiece_isDefined (node));
 170   llassert (node->kind == MTP_CONTEXT);
 171
 172   /*@-abstract@*/
 173   res = (mtContextNode) node->node;
 174   /*@=abstract@*/
 175   node->kind = MTP_DEAD;
 176   node->node =  NULL;
 177   return res;
 178 }
 179
 180 extern mtDefaultsNode mtDeclarationPiece_getDefaults (mtDeclarationPiece node)
 181 {
 182   llassert (mtDeclarationPiece_isDefined (node));
 183   llassert (node->kind == MTP_DEFAULTS);
 184
 185   /*@-abstract@*/
 186   return (mtDefaultsNode) node->node;
 187   /*@=abstract@*/
 188 }
 189
 190 extern cstring mtDeclarationPiece_getDefaultValue (mtDeclarationPiece node)
 191 {
 192   llassert (mtDeclarationPiece_isDefined (node));
 193   llassert (node->kind == MTP_DEFAULTVALUE);
 194
 195   /*@-abstract@*/
 196   return mttok_observeText ((mttok) node->node);
 197   /*@=abstract@*/
 198 }
 199
 200 extern mtAnnotationsNode mtDeclarationPiece_getAnnotations (mtDeclarationPiece node)
 201 {
 202   llassert (mtDeclarationPiece_isDefined (node));
 203   llassert (node->kind == MTP_ANNOTATIONS);
 204
 205   /*@-abstract@*/
 206   return (mtAnnotationsNode) node->node;
 207   /*@=abstract@*/
 208 }
 209
 210 extern mtMergeNode mtDeclarationPiece_getMerge (mtDeclarationPiece node)
 211 {
 212   llassert (mtDeclarationPiece_isDefined (node));
 213   llassert (node->kind == MTP_MERGE);
 214
 215   /*@-abstract@*/
 216   return (mtMergeNode) node->node;
 217   /*@=abstract@*/
 218 }
 219
 220 extern mtTransferClauseList mtDeclarationPiece_getTransfers (mtDeclarationPiece node)
 221 {
 222   llassert (mtDeclarationPiece_isDefined (node));
 223   llassert (node->kind == MTP_TRANSFERS);
 224
 225   /*@-abstract@*/
 226   return (mtTransferClauseList) node->node;
 227   /*@=abstract@*/
 228 }
 229
 230 extern mtTransferClauseList mtDeclarationPiece_getPreconditions (mtDeclarationPiece node)
 231 {
 232   llassert (mtDeclarationPiece_isDefined (node));
 233   llassert (node->kind == MTP_PRECONDITIONS);
 234
 235   /*@-abstract@*/
 236   return (mtTransferClauseList) node->node;
 237   /*@=abstract@*/
 238 }
 239
 240 extern mtTransferClauseList mtDeclarationPiece_getPostconditions (mtDeclarationPiece node)
 241 {
 242   llassert (mtDeclarationPiece_isDefined (node));
 243   llassert (node->kind == MTP_POSTCONDITIONS);
 244
 245   /*@-abstract@*/
 246   return (mtTransferClauseList) node->node;
 247   /*@=abstract@*/
 248 }
 249
 250 extern mtLoseReferenceList mtDeclarationPiece_getLosers (mtDeclarationPiece node)
 251 {
 252   llassert (mtDeclarationPiece_isDefined (node));
 253   llassert (node->kind == MTP_LOSERS);
 254
 255   /*@-abstract@*/
 256   return (mtLoseReferenceList) node->node;
 257   /*@=abstract@*/
 258 }
 259
 260 extern mtValuesNode mtDeclarationPiece_getValues (mtDeclarationPiece node)
 261 {
 262   llassert (mtDeclarationPiece_isDefined (node));
 263   llassert (node->kind == MTP_VALUES);
 264
 265   /*@-abstract@*/
 266   return (mtValuesNode) node->node;
 267   /*@=abstract@*/
 268 }
 269
 270 extern void mtDeclarationPiece_free (/*@only@*/ mtDeclarationPiece node)
 271 {
 272   if (node != NULL)
 273     {
 274       switch (node->kind)
 275         {
 276         case MTP_DEAD:
 277           llassert (node->node == NULL);
 278           break;
 279
 280         case MTP_CONTEXT:
 281           /*@access mtContextNode@*/
 282           mtContextNode_free ((mtContextNode) node->node);
 283           break;
 284           /*@noaccess mtContextNode@*/
 285         case MTP_VALUES:
 286           /*@access mtValuesNode@*/
 287           mtValuesNode_free ((mtValuesNode) node->node);
 288           break;
 289           /*@noaccess mtValuesNode@*/
 290         case MTP_DEFAULTS:
 291           /*@access mtDefaultsNode@*/
 292           mtDefaultsNode_free ((mtDefaultsNode) node->node);
 293           break;
 294           /*@noaccess mtDefaultsNode@*/
 295         case MTP_DEFAULTVALUE:
 296           /*@access mttok@*/
 297           mttok_free ((mttok) node->node);
 298           break;
 299           /*@noaccess mttok@*/
 300         case MTP_ANNOTATIONS:
 301           /*@access mtAnnotationsNode@*/
 302           mtAnnotationsNode_free ((mtAnnotationsNode) node->node);
 303           break;
 304           /*@noaccess mtAnnotationsNode@*/
 305         case MTP_MERGE:
 306           /*@access mtMergeNode@*/
 307           mtMergeNode_free ((mtMergeNode) node->node);
 308           break;
 309           /*@noaccess mtMergeNode@*/
 310         case MTP_TRANSFERS:
 311         case MTP_PRECONDITIONS:
 312         case MTP_POSTCONDITIONS:
 313           /*@access mtTransferClauseList@*/
 314           mtTransferClauseList_free ((mtTransferClauseList) node->node);
 315           break;
 316           /*@noaccess mtTransferClauseList@*/
 317         case MTP_LOSERS:
 318           /*@access mtLoseReferenceList@*/
 319           mtLoseReferenceList_free ((mtLoseReferenceList) node->node);
 320           break;
 321           /*@noaccess mtLoseReferenceList@*/
 322         }
 323
 324       sfree (node);
 325     }
 326 }