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"
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
;
60 bool stateValue_sameValue (stateValue s1
, stateValue s2
)
62 if (stateValue_isDefined (s1
) && stateValue_isDefined (s2
))
64 return s1
->value
== s2
->value
;
68 return !stateValue_isDefined (s1
) && !stateValue_isDefined (s2
);
71 # endif /* DEADCODE */
74 cstring
stateValue_unparse (stateValue s
) {
75 if (stateValue_isDefined (s
))
77 return (message ("%d:%q", s
->value
, stateInfo_unparse (s
->info
)));
81 return (cstring_makeLiteral ("<stateValue_undefined>"));
86 void stateValue_updateValue (stateValue s
, int value
, stateInfo info
)
88 llassert (stateValue_isDefined (s
));
91 if (stateInfo_isDefined (info
)) {
92 stateInfo_free (s
->info
);
96 DPRINTF (("update state value: %s", stateValue_unparse (s
)));
98 # endif /* DEADCODE */
100 void stateValue_updateValueLoc (stateValue s
, int value
, fileloc loc
)
102 llassert (stateValue_isDefined (s
));
104 DPRINTF (("Update state: %s -> %d at %s", stateValue_unparse (s
), value
,
105 fileloc_unparse (loc
)));
108 s
->info
= stateInfo_updateLoc (s
->info
, SA_CHANGED
, loc
);
112 void stateValue_update (stateValue res
, stateValue val
)
114 llassert (stateValue_isDefined (res
));
115 llassert (stateValue_isDefined (val
));
117 res
->value
= val
->value
;
118 res
->info
= stateInfo_update (res
->info
, val
->info
);
120 DPRINTF (("update state: %s", stateValue_unparse (res
)));
122 # endif /* DEADCODE */
124 void stateValue_show (stateValue s
, metaStateInfo msinfo
)
126 if (stateValue_isDefined (s
))
128 stateInfo info
= stateValue_getInfo (s
);
130 if (stateInfo_isDefined (info
))
132 if (fileloc_isDefined (info
->loc
))
134 llgenindentmsg (message
136 stateValue_unparseValue (s
, msinfo
)),
143 /*@only@*/ cstring
stateValue_unparseValue (stateValue s
, metaStateInfo msinfo
)
145 if (stateValue_isImplicit (s
))
147 return message ("implicitly %s",
148 metaStateInfo_unparseValue (msinfo
,
149 stateValue_getValue (s
)));
153 return cstring_copy (metaStateInfo_unparseValue (msinfo
,
154 stateValue_getValue (s
)));
158 int stateValue_getValue (stateValue s
)
160 if (!stateValue_isDefined (s
))
162 llassert (stateValue_isDefined (s
));
163 return stateValue_error
;
169 bool stateValue_isImplicit (stateValue s
)
171 llassert (stateValue_isDefined (s
));
175 stateInfo
stateValue_getInfo (stateValue s
)
177 llassert (stateValue_isDefined (s
));
181 bool stateValue_hasLoc (stateValue s
)
183 return (fileloc_isDefined (stateValue_getLoc (s
)));