2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2002 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"
32 /*@notnull@*/ stateValue stateValue_create (int value, stateInfo info) {
33 stateValue sv = (stateValue) dmalloc (sizeof (*sv));
42 /*@notnull@*/ stateValue stateValue_createImplicit (int value, stateInfo info) {
43 stateValue sv = (stateValue) dmalloc (sizeof (*sv));
51 stateValue stateValue_copy (stateValue s) {
53 llassert (stateValue_isDefined (s));
54 res = stateValue_create (s->value, stateInfo_copy (s->info));
55 res->implicit = s->implicit;
59 bool stateValue_sameValue (stateValue s1, stateValue s2)
61 if (stateValue_isDefined (s1) && stateValue_isDefined (s2))
63 return s1->value == s2->value;
67 return !stateValue_isDefined (s1) && !stateValue_isDefined (s2);
72 cstring stateValue_unparse (stateValue s) {
73 if (stateValue_isDefined (s))
75 return (message ("%d:%q", s->value, stateInfo_unparse (s->info)));
79 return (cstring_makeLiteral ("<stateValue_undefined>"));
83 void stateValue_updateValue (stateValue s, int value, stateInfo info)
85 llassert (stateValue_isDefined (s));
88 if (stateInfo_isDefined (info)) {
89 stateInfo_free (s->info);
93 DPRINTF (("update state value: %s", stateValue_unparse (s)));
96 void stateValue_updateValueLoc (stateValue s, int value, fileloc loc)
98 llassert (stateValue_isDefined (s));
100 DPRINTF (("Update state: %s -> %d at %s", stateValue_unparse (s), value,
101 fileloc_unparse (loc)));
105 if (fileloc_isDefined (loc)) {
106 s->info = stateInfo_updateLoc (s->info, loc);
110 void stateValue_update (stateValue res, stateValue val)
112 llassert (stateValue_isDefined (res));
113 llassert (stateValue_isDefined (val));
115 res->value = val->value;
116 res->info = stateInfo_update (res->info, val->info);
118 DPRINTF (("update state: %s", stateValue_unparse (res)));
121 void stateValue_show (stateValue s, metaStateInfo msinfo)
123 if (stateValue_isDefined (s))
125 stateInfo info = stateValue_getInfo (s);
127 if (stateInfo_isDefined (info))
129 if (fileloc_isDefined (info->loc))
131 llgenindentmsg (message
133 stateValue_unparseValue (s, msinfo)),
140 /*@only@*/ cstring stateValue_unparseValue (stateValue s, metaStateInfo msinfo)
142 if (stateValue_isImplicit (s))
144 return message ("implicitly %s",
145 metaStateInfo_unparseValue (msinfo,
146 stateValue_getValue (s)));
150 return cstring_copy (metaStateInfo_unparseValue (msinfo,
151 stateValue_getValue (s)));
155 int stateValue_getValue (stateValue s)
157 if (!stateValue_isDefined (s))
159 llassert (stateValue_isDefined (s));
160 return stateValue_error;
166 bool stateValue_isImplicit (stateValue s)
168 llassert (stateValue_isDefined (s));
172 stateInfo stateValue_getInfo (stateValue s)
174 llassert (stateValue_isDefined (s));
178 bool stateValue_hasLoc (stateValue s)
180 return (fileloc_isDefined (stateValue_getLoc (s)));