2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 University of Virginia,
4 ** Massachusetts Institute of Technology
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.
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.
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.
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
25 ** mtDeclarationPiece.c
28 # include "splintMacros.nf"
31 static mtDeclarationPiece
32 mtDeclarationPiece_create (mtPieceKind kind, /*@null@*/ /*@only@*/ void *node)
34 mtDeclarationPiece res = (mtDeclarationPiece) dmalloc (sizeof (*res));
42 extern mtDeclarationPiece mtDeclarationPiece_createContext (mtContextNode node) /*@*/
44 return mtDeclarationPiece_create (MTP_CONTEXT, (void *) node);
47 extern mtDeclarationPiece mtDeclarationPiece_createValues (mtValuesNode node) /*@*/
49 return mtDeclarationPiece_create (MTP_VALUES, (void *) node);
52 extern mtDeclarationPiece mtDeclarationPiece_createDefaults (mtDefaultsNode node) /*@*/
54 return mtDeclarationPiece_create (MTP_DEFAULTS, (void *) node);
57 extern mtDeclarationPiece mtDeclarationPiece_createValueDefault (mttok node) /*@*/
59 llassert (mttok_isIdentifier (node));
60 return mtDeclarationPiece_create (MTP_DEFAULTVALUE, (void *) node);
63 extern mtDeclarationPiece mtDeclarationPiece_createAnnotations (mtAnnotationsNode node) /*@*/
65 return mtDeclarationPiece_create (MTP_ANNOTATIONS, (void *) node);
68 extern mtDeclarationPiece mtDeclarationPiece_createMerge (mtMergeNode node) /*@*/
70 return mtDeclarationPiece_create (MTP_MERGE, (void *) node);
73 extern mtDeclarationPiece mtDeclarationPiece_createTransfers (mtTransferClauseList node) /*@*/
75 return mtDeclarationPiece_create (MTP_TRANSFERS, (void *) node);
78 extern mtDeclarationPiece mtDeclarationPiece_createPreconditions (mtTransferClauseList node) /*@*/
80 return mtDeclarationPiece_create (MTP_PRECONDITIONS, (void *) node);
83 mtDeclarationPiece mtDeclarationPiece_createPostconditions (mtTransferClauseList node) /*@*/
85 return mtDeclarationPiece_create (MTP_POSTCONDITIONS, (void *) node);
88 mtDeclarationPiece mtDeclarationPiece_createLosers (mtLoseReferenceList node) /*@*/
90 return mtDeclarationPiece_create (MTP_LOSERS, (void *) node);
93 /*@only@*/ cstring mtDeclarationPiece_unparse (mtDeclarationPiece p)
95 if (mtDeclarationPiece_isUndefined (p))
97 return cstring_undefined;
103 /*@access mtContextNode@*/
104 return mtContextNode_unparse ((mtContextNode) p->node);
105 /*@noaccess mtContextNode@*/
107 /*@access mtValuesNode@*/
108 return mtValuesNode_unparse ((mtValuesNode) p->node);
109 /*@noaccess mtValuesNode@*/
111 /*@access mtDefaultsNode@*/
112 return mtDefaultsNode_unparse ((mtDefaultsNode) p->node);
113 /*@noaccess mtDefaultsNode@*/
114 case MTP_DEFAULTVALUE:
116 return message ("default %q", mttok_getText ((mttok) p->node));
118 case MTP_ANNOTATIONS:
119 /*@access mtAnnotationsNode@*/
120 return mtAnnotationsNode_unparse ((mtAnnotationsNode) p->node);
121 /*@noaccess mtAnnotationsNode@*/
123 /*@access mtMergeNode@*/
124 return mtMergeNode_unparse ((mtMergeNode) p->node);
125 /*@noaccess mtMergeNode@*/
127 case MTP_PRECONDITIONS:
128 case MTP_POSTCONDITIONS:
129 /*@access mtTransferClauseList@*/
130 return mtTransferClauseList_unparse ((mtTransferClauseList) p->node);
131 /*@noaccess mtTransferClauseList@*/
133 /*@access mtLoseReferenceList@*/
134 return mtLoseReferenceList_unparse ((mtLoseReferenceList) p->node);
135 /*@noaccess mtLoseReferenceList@*/
137 return cstring_makeLiteral ("Dead Piece");
140 BADBRANCHRET (cstring_undefined);
143 extern bool mtDeclarationPiece_matchKind (mtDeclarationPiece p, mtPieceKind kind) /*@*/
145 if (mtDeclarationPiece_isDefined (p))
147 return (p->kind == kind);
155 extern mtContextNode mtDeclarationPiece_getContext (mtDeclarationPiece node)
157 llassert (mtDeclarationPiece_isDefined (node));
158 llassert (node->kind == MTP_CONTEXT);
161 return (mtContextNode) node->node;
165 extern mtContextNode mtDeclarationPiece_stealContext (mtDeclarationPiece node)
169 llassert (mtDeclarationPiece_isDefined (node));
170 llassert (node->kind == MTP_CONTEXT);
173 res = (mtContextNode) node->node;
175 node->kind = MTP_DEAD;
180 extern mtDefaultsNode mtDeclarationPiece_getDefaults (mtDeclarationPiece node)
182 llassert (mtDeclarationPiece_isDefined (node));
183 llassert (node->kind == MTP_DEFAULTS);
186 return (mtDefaultsNode) node->node;
190 extern cstring mtDeclarationPiece_getDefaultValue (mtDeclarationPiece node)
192 llassert (mtDeclarationPiece_isDefined (node));
193 llassert (node->kind == MTP_DEFAULTVALUE);
196 return mttok_observeText ((mttok) node->node);
200 extern mtAnnotationsNode mtDeclarationPiece_getAnnotations (mtDeclarationPiece node)
202 llassert (mtDeclarationPiece_isDefined (node));
203 llassert (node->kind == MTP_ANNOTATIONS);
206 return (mtAnnotationsNode) node->node;
210 extern mtMergeNode mtDeclarationPiece_getMerge (mtDeclarationPiece node)
212 llassert (mtDeclarationPiece_isDefined (node));
213 llassert (node->kind == MTP_MERGE);
216 return (mtMergeNode) node->node;
220 extern mtTransferClauseList mtDeclarationPiece_getTransfers (mtDeclarationPiece node)
222 llassert (mtDeclarationPiece_isDefined (node));
223 llassert (node->kind == MTP_TRANSFERS);
226 return (mtTransferClauseList) node->node;
230 extern mtTransferClauseList mtDeclarationPiece_getPreconditions (mtDeclarationPiece node)
232 llassert (mtDeclarationPiece_isDefined (node));
233 llassert (node->kind == MTP_PRECONDITIONS);
236 return (mtTransferClauseList) node->node;
240 extern mtTransferClauseList mtDeclarationPiece_getPostconditions (mtDeclarationPiece node)
242 llassert (mtDeclarationPiece_isDefined (node));
243 llassert (node->kind == MTP_POSTCONDITIONS);
246 return (mtTransferClauseList) node->node;
250 extern mtLoseReferenceList mtDeclarationPiece_getLosers (mtDeclarationPiece node)
252 llassert (mtDeclarationPiece_isDefined (node));
253 llassert (node->kind == MTP_LOSERS);
256 return (mtLoseReferenceList) node->node;
260 extern mtValuesNode mtDeclarationPiece_getValues (mtDeclarationPiece node)
262 llassert (mtDeclarationPiece_isDefined (node));
263 llassert (node->kind == MTP_VALUES);
266 return (mtValuesNode) node->node;
270 extern void mtDeclarationPiece_free (/*@only@*/ mtDeclarationPiece node)
277 llassert (node->node == NULL);
281 /*@access mtContextNode@*/
282 mtContextNode_free ((mtContextNode) node->node);
284 /*@noaccess mtContextNode@*/
286 /*@access mtValuesNode@*/
287 mtValuesNode_free ((mtValuesNode) node->node);
289 /*@noaccess mtValuesNode@*/
291 /*@access mtDefaultsNode@*/
292 mtDefaultsNode_free ((mtDefaultsNode) node->node);
294 /*@noaccess mtDefaultsNode@*/
295 case MTP_DEFAULTVALUE:
297 mttok_free ((mttok) node->node);
300 case MTP_ANNOTATIONS:
301 /*@access mtAnnotationsNode@*/
302 mtAnnotationsNode_free ((mtAnnotationsNode) node->node);
304 /*@noaccess mtAnnotationsNode@*/
306 /*@access mtMergeNode@*/
307 mtMergeNode_free ((mtMergeNode) node->node);
309 /*@noaccess mtMergeNode@*/
311 case MTP_PRECONDITIONS:
312 case MTP_POSTCONDITIONS:
313 /*@access mtTransferClauseList@*/
314 mtTransferClauseList_free ((mtTransferClauseList) node->node);
316 /*@noaccess mtTransferClauseList@*/
318 /*@access mtLoseReferenceList@*/
319 mtLoseReferenceList_free ((mtLoseReferenceList) node->node);
321 /*@noaccess mtLoseReferenceList@*/