src/mtDeclarationPieces.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 ** mtDeclarationPieces.c
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30
  31 extern mtDeclarationPieces mtDeclarationPieces_create (void) /*@*/
  32 {
  33   return mtDeclarationPieces_undefined;
  34 }
  35
  36 extern mtDeclarationPieces mtDeclarationPieces_append (mtDeclarationPieces node,
  37                                                        /*@only@*/ mtDeclarationPiece piece)
  38      /*@modifies node*/
  39 {
  40   mtDeclarationPieces tnode = node;
  41   mtDeclarationPieces res = (mtDeclarationPieces) dmalloc (sizeof (*node));
  42
  43   res->thisPiece = piece;
  44   res->rest = mtDeclarationPieces_undefined;
  45
  46   if (mtDeclarationPieces_isUndefined (node)) {
  47     return res;
  48   }
  49
  50   while (mtDeclarationPieces_isDefined (tnode->rest))
  51     {
  52       tnode = tnode->rest;
  53     }
  54
  55   tnode->rest = res;
  56   return node;
  57 }
  58
  59 extern cstring mtDeclarationPieces_unparse (mtDeclarationPieces node) /*@*/
  60 {
  61   cstring res = cstring_newEmpty ();
  62
  63   while (mtDeclarationPieces_isDefined (node))
  64     {
  65       res = message ("%q%q; ", res, mtDeclarationPiece_unparse (node->thisPiece));
  66       node = node->rest;
  67     }
  68
  69   return res;
  70 }
  71
  72 mtDeclarationPiece
  73 mtDeclarationPieces_findPiece (mtDeclarationPieces pieces, mtPieceKind kind)
  74 {
  75   bool foundone = FALSE;
  76   mtDeclarationPiece res = mtDeclarationPiece_undefined;
  77
  78   while (mtDeclarationPieces_isDefined (pieces))
  79     {
  80       if (mtDeclarationPiece_matchKind (pieces->thisPiece, kind))
  81         {
  82           if (foundone)
  83             {
  84               llassert (mtDeclarationPiece_isDefined (res));
  85               voptgenerror
  86                 (FLG_SYNTAX,
  87                  message ("Metastate declaration has duplicate pieces: %q / %q",
  88                           mtDeclarationPiece_unparse (res),
  89                           mtDeclarationPiece_unparse (pieces->thisPiece)),
  90                  g_currentloc); /*@i43 pieces's should have locs! */
  91             }
  92           else
  93             {
  94               foundone = TRUE;
  95               llassert (mtDeclarationPiece_isUndefined (res));
  96               res = pieces->thisPiece;
  97             }
  98         }
  99
 100       pieces = pieces->rest;
 101     }
 102
 103   return res;
 104 }
 105
 106 extern void mtDeclarationPieces_free (/*@only@*/ mtDeclarationPieces node)
 107 {
 108   if (mtDeclarationPieces_isDefined (node))
 109     {
 110       mtDeclarationPiece_free (node->thisPiece);
 111       mtDeclarationPieces_free (node->rest);
 112     }
 113
 114   sfree (node);
 115 }