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 annotationInfo annotationInfo_create (cstring name,
32 metaStateInfo state, mtContextNode context,
33 int value, fileloc loc)
35 annotationInfo res = (annotationInfo) dmalloc (sizeof (*res));
39 res->context = context;
46 void annotationInfo_free (annotationInfo a)
48 if (annotationInfo_isDefined (a))
50 cstring_free (a->name);
51 fileloc_free (a->loc);
52 mtContextNode_free (a->context); /* evans 2002-01-03 */
57 cstring annotationInfo_getName (annotationInfo a)
59 llassert (annotationInfo_isDefined (a));
63 /*@observer@*/ cstring annotationInfo_unparse (annotationInfo a)
65 return annotationInfo_getName (a);
68 /*@observer@*/ metaStateInfo annotationInfo_getState (annotationInfo a) /*@*/
70 llassert (annotationInfo_isDefined (a));
74 /*@observer@*/ fileloc annotationInfo_getLoc (annotationInfo a) /*@*/
76 llassert (annotationInfo_isDefined (a));
80 int annotationInfo_getValue (annotationInfo a) /*@*/
82 llassert (annotationInfo_isDefined (a));
87 bool annotationInfo_matchesContext (annotationInfo a, uentry ue)
90 ** Returns true iff the annotation context matches the uentry.
93 mtContextNode mcontext;
95 llassert (annotationInfo_isDefined (a));
96 mcontext = a->context;
98 if (mtContextNode_matchesEntry (mcontext, ue))
100 /* Matches annotation context, must also match meta state context. */
101 metaStateInfo minfo = a->state;
103 if (mtContextNode_matchesEntry (metaStateInfo_getContext (minfo), ue))
118 bool annotationInfo_matchesContextRef (annotationInfo a, sRef sr)
121 ** Returns true iff the annotation context matches the uentry.
124 mtContextNode mcontext;
126 llassert (annotationInfo_isDefined (a));
127 mcontext = a->context;
129 if (mtContextNode_matchesRef (mcontext, sr))
131 /* Matches annotation context, must also match meta state context. */
132 metaStateInfo minfo = a->state;
134 if (mtContextNode_matchesRef (metaStateInfo_getContext (minfo), sr))
149 cstring annotationInfo_dump (annotationInfo a)
151 llassert (annotationInfo_isDefined (a));
155 /*@observer@*/ annotationInfo annotationInfo_undump (char **s)
157 cstring mname = reader_readUntil (s, '.');
160 llassert (cstring_isDefined (mname));
161 a = context_lookupAnnotation (mname);
163 if (annotationInfo_isUndefined (a))
166 (message ("Library uses undefined annotation %s. Must use same -mts flags as when library was created.",
171 cstring_free (mname);
175 BADBRANCHRET (annotationInfo_undefined);
178 void annotationInfo_showContextRefError (annotationInfo a, sRef sr)
180 mtContextNode mcontext;
181 llassert (!annotationInfo_matchesContextRef (a, sr));
182 llassert (annotationInfo_isDefined (a));
183 mcontext = a->context;
185 if (mtContextNode_matchesRef (mcontext, sr))
187 /* Matches annotation context, must also match meta state context. */
188 metaStateInfo minfo = a->state;
190 if (mtContextNode_matchesRef (metaStateInfo_getContext (minfo), sr))
196 mtContextNode_showRefError (metaStateInfo_getContext (minfo), sr);
201 mtContextNode_showRefError (mcontext, sr);