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   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 # ifdef DEADCODE
 156 extern mtContextNode mtDeclarationPiece_getContext (mtDeclarationPiece node)
 157 {
 158   llassert (mtDeclarationPiece_isDefined (node));
 159   llassert (node->kind == MTP_CONTEXT);
 160
 161   /*@-abstract@*/
 162   return (mtContextNode) node->node;
 163   /*@=abstract@*/
 164 }
 165 # endif /* DEADCODE */
 166
 167 extern mtContextNode mtDeclarationPiece_stealContext (mtDeclarationPiece node)
 168 {
 169   mtContextNode res;
 170
 171   llassert (mtDeclarationPiece_isDefined (node));
 172   llassert (node->kind == MTP_CONTEXT);
 173
 174   /*@-abstract@*/
 175   res = (mtContextNode) node->node;
 176   /*@=abstract@*/
 177   node->kind = MTP_DEAD;
 178   node->node =  NULL;
 179   return res;
 180 }
 181
 182 extern mtDefaultsNode mtDeclarationPiece_getDefaults (mtDeclarationPiece node)
 183 {
 184   llassert (mtDeclarationPiece_isDefined (node));
 185   llassert (node->kind == MTP_DEFAULTS);
 186
 187   /*@-abstract@*/
 188   return (mtDefaultsNode) node->node;
 189   /*@=abstract@*/
 190 }
 191
 192 extern cstring mtDeclarationPiece_getDefaultValue (mtDeclarationPiece node)
 193 {
 194   llassert (mtDeclarationPiece_isDefined (node));
 195   llassert (node->kind == MTP_DEFAULTVALUE);
 196
 197   /*@-abstract@*/
 198   return mttok_observeText ((mttok) node->node);
 199   /*@=abstract@*/
 200 }
 201
 202 extern mtAnnotationsNode mtDeclarationPiece_getAnnotations (mtDeclarationPiece node)
 203 {
 204   llassert (mtDeclarationPiece_isDefined (node));
 205   llassert (node->kind == MTP_ANNOTATIONS);
 206
 207   /*@-abstract@*/
 208   return (mtAnnotationsNode) node->node;
 209   /*@=abstract@*/
 210 }
 211
 212 extern mtMergeNode mtDeclarationPiece_getMerge (mtDeclarationPiece node)
 213 {
 214   llassert (mtDeclarationPiece_isDefined (node));
 215   llassert (node->kind == MTP_MERGE);
 216
 217   /*@-abstract@*/
 218   return (mtMergeNode) node->node;
 219   /*@=abstract@*/
 220 }
 221
 222 extern mtTransferClauseList mtDeclarationPiece_getTransfers (mtDeclarationPiece node)
 223 {
 224   llassert (mtDeclarationPiece_isDefined (node));
 225   llassert (node->kind == MTP_TRANSFERS);
 226
 227   /*@-abstract@*/
 228   return (mtTransferClauseList) node->node;
 229   /*@=abstract@*/
 230 }
 231
 232 extern mtTransferClauseList mtDeclarationPiece_getPreconditions (mtDeclarationPiece node)
 233 {
 234   llassert (mtDeclarationPiece_isDefined (node));
 235   llassert (node->kind == MTP_PRECONDITIONS);
 236
 237   /*@-abstract@*/
 238   return (mtTransferClauseList) node->node;
 239   /*@=abstract@*/
 240 }
 241
 242 # ifdef DEADCODE
 243 extern mtTransferClauseList mtDeclarationPiece_getPostconditions (mtDeclarationPiece node)
 244 {
 245   llassert (mtDeclarationPiece_isDefined (node));
 246   llassert (node->kind == MTP_POSTCONDITIONS);
 247
 248   /*@-abstract@*/
 249   return (mtTransferClauseList) node->node;
 250   /*@=abstract@*/
 251 }
 252 # endif /* DEADCODE */
 253
 254 extern mtLoseReferenceList mtDeclarationPiece_getLosers (mtDeclarationPiece node)
 255 {
 256   llassert (mtDeclarationPiece_isDefined (node));
 257   llassert (node->kind == MTP_LOSERS);
 258
 259   /*@-abstract@*/
 260   return (mtLoseReferenceList) node->node;
 261   /*@=abstract@*/
 262 }
 263
 264 extern mtValuesNode mtDeclarationPiece_getValues (mtDeclarationPiece node)
 265 {
 266   llassert (mtDeclarationPiece_isDefined (node));
 267   llassert (node->kind == MTP_VALUES);
 268
 269   /*@-abstract@*/
 270   return (mtValuesNode) node->node;
 271   /*@=abstract@*/
 272 }
 273
 274 extern void mtDeclarationPiece_free (/*@only@*/ mtDeclarationPiece node)
 275 {
 276   if (node != NULL)
 277     {
 278       switch (node->kind)
 279         {
 280         case MTP_DEAD:
 281           llassert (node->node == NULL);
 282           break;
 283
 284         case MTP_CONTEXT:
 285           /*@access mtContextNode@*/
 286           mtContextNode_free ((mtContextNode) node->node);
 287           break;
 288           /*@noaccess mtContextNode@*/
 289         case MTP_VALUES:
 290           /*@access mtValuesNode@*/
 291           mtValuesNode_free ((mtValuesNode) node->node);
 292           break;
 293           /*@noaccess mtValuesNode@*/
 294         case MTP_DEFAULTS:
 295           /*@access mtDefaultsNode@*/
 296           mtDefaultsNode_free ((mtDefaultsNode) node->node);
 297           break;
 298           /*@noaccess mtDefaultsNode@*/
 299         case MTP_DEFAULTVALUE:
 300           /*@access mttok@*/
 301           mttok_free ((mttok) node->node);
 302           break;
 303           /*@noaccess mttok@*/
 304         case MTP_ANNOTATIONS:
 305           /*@access mtAnnotationsNode@*/
 306           mtAnnotationsNode_free ((mtAnnotationsNode) node->node);
 307           break;
 308           /*@noaccess mtAnnotationsNode@*/
 309         case MTP_MERGE:
 310           /*@access mtMergeNode@*/
 311           mtMergeNode_free ((mtMergeNode) node->node);
 312           break;
 313           /*@noaccess mtMergeNode@*/
 314         case MTP_TRANSFERS:
 315         case MTP_PRECONDITIONS:
 316         case MTP_POSTCONDITIONS:
 317           /*@access mtTransferClauseList@*/
 318           mtTransferClauseList_free ((mtTransferClauseList) node->node);
 319           break;
 320           /*@noaccess mtTransferClauseList@*/
 321         case MTP_LOSERS:
 322           /*@access mtLoseReferenceList@*/
 323           mtLoseReferenceList_free ((mtLoseReferenceList) node->node);
 324           break;
 325           /*@noaccess mtLoseReferenceList@*/
 326         }
 327
 328       sfree (node);
 329     }
 330 }