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
28 # include "splintMacros.nf"
31 static /*@only@*/ /*@notnull@*/ /*@special@*/ functionClause
32 functionClause_alloc (functionClauseKind kind) /*@defines result->kind@*/
34 functionClause res = (functionClause) dmalloc (sizeof (*res));
40 extern functionClause functionClause_createGlobals (globalsClause node) /*@*/
42 functionClause res = functionClause_alloc (FCK_GLOBALS);
43 res->val.globals = node;
47 extern functionClause functionClause_createModifies (modifiesClause node) /*@*/
49 functionClause res = functionClause_alloc (FCK_MODIFIES);
50 res->val.modifies = node;
54 extern functionClause functionClause_createState (stateClause node) /*@*/
56 if (stateClause_hasEmptyReferences (node) &&
57 (!stateClause_isMetaState (node) ) )
59 DPRINTF((message("functionClause_createState:: Returning functionClause_undefined" ) ));
60 stateClause_free (node);
61 return functionClause_undefined;
65 functionClause res = functionClause_alloc (FCK_STATE);
66 res->val.state = node;
71 extern functionClause functionClause_createEnsures (functionConstraint node) /*@*/
73 functionClause res = functionClause_alloc (FCK_ENSURES);
74 res->val.constraint = node;
78 extern functionClause functionClause_createRequires (functionConstraint node) /*@*/
80 functionClause res = functionClause_alloc (FCK_REQUIRES);
81 res->val.constraint = node;
85 extern functionClause functionClause_createWarn (warnClause node) /*@*/
87 functionClause res = functionClause_alloc (FCK_WARN);
92 /*@only@*/ cstring functionClause_unparse (functionClause p)
94 if (functionClause_isUndefined (p))
96 return cstring_undefined;
102 return globalsClause_unparse (p->val.globals);
104 return modifiesClause_unparse (p->val.modifies);
106 return warnClause_unparse (p->val.warn);
108 return stateClause_unparse (p->val.state);
110 return message ("ensures %q", functionConstraint_unparse (p->val.constraint));
112 return message ("requires %q", functionConstraint_unparse (p->val.constraint));
114 return cstring_makeLiteral ("<dead clause>");
117 BADBRANCHRET (cstring_undefined);
120 extern bool functionClause_matchKind (functionClause p, functionClauseKind kind) /*@*/
122 if (functionClause_isDefined (p))
124 return (p->kind == kind);
132 extern stateClause functionClause_getState (functionClause node)
134 llassert (functionClause_isDefined (node));
135 llassert (node->kind == FCK_STATE);
137 return node->val.state;
140 extern stateClause functionClause_takeState (functionClause fc)
143 llassert (functionClause_isDefined (fc));
144 llassert (fc->kind == FCK_STATE);
147 fc->val.state = NULL;
152 extern functionConstraint functionClause_getEnsures (functionClause node)
154 llassert (functionClause_isDefined (node));
155 llassert (node->kind == FCK_ENSURES);
157 return node->val.constraint;
160 extern functionConstraint functionClause_takeEnsures (functionClause fc)
162 functionConstraint res;
163 llassert (functionClause_isDefined (fc));
164 llassert (fc->kind == FCK_ENSURES);
166 res = fc->val.constraint;
167 fc->val.constraint = NULL;
172 extern functionConstraint functionClause_getRequires (functionClause node)
174 llassert (functionClause_isDefined (node));
175 llassert (node->kind == FCK_REQUIRES);
177 return node->val.constraint;
180 extern functionConstraint functionClause_takeRequires (functionClause fc)
182 functionConstraint res;
183 llassert (functionClause_isDefined (fc));
184 llassert (fc->kind == FCK_REQUIRES);
186 res = fc->val.constraint;
187 fc->val.constraint = NULL;
192 extern warnClause functionClause_getWarn (functionClause node)
194 llassert (functionClause_isDefined (node));
195 llassert (node->kind == FCK_WARN);
197 return node->val.warn;
200 extern warnClause functionClause_takeWarn (functionClause fc)
203 llassert (functionClause_isDefined (fc));
204 llassert (fc->kind == FCK_WARN);
207 fc->val.warn = warnClause_undefined;
212 extern modifiesClause functionClause_getModifies (functionClause node)
214 llassert (functionClause_isDefined (node));
215 llassert (node->kind == FCK_MODIFIES);
217 return node->val.modifies;
220 extern globalsClause functionClause_getGlobals (functionClause node)
222 llassert (functionClause_isDefined (node));
223 llassert (node->kind == FCK_GLOBALS);
225 return node->val.globals;
228 extern void functionClause_free (/*@only@*/ functionClause node)
232 DPRINTF (("free: %s", functionClause_unparse (node)));
237 globalsClause_free (node->val.globals);
240 modifiesClause_free (node->val.modifies);
243 warnClause_free (node->val.warn);
246 stateClause_free (node->val.state);
249 functionConstraint_free (node->val.constraint);
252 functionConstraint_free (node->val.constraint);
255 /* Nothing to release */