2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2001 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 lclint: lclint-request@cs.virginia.edu
21 ** To report a bug: lclint-bug@cs.virginia.edu
22 ** For more information: http://www.splint.org
28 # include "lclintMacros.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 ainfo)
48 if (annotationInfo_isDefined (ainfo))
50 cstring_free (ainfo->name);
51 fileloc_free (ainfo->loc);
56 cstring annotationInfo_getName (annotationInfo ainfo)
58 llassert (annotationInfo_isDefined (ainfo));
62 /*@observer@*/ cstring annotationInfo_unparse (annotationInfo ainfo)
64 return annotationInfo_getName (ainfo);
67 /*@observer@*/ metaStateInfo annotationInfo_getState (annotationInfo a) /*@*/
69 llassert (annotationInfo_isDefined (a));
73 /*@observer@*/ fileloc annotationInfo_getLoc (annotationInfo ainfo) /*@*/
75 llassert (annotationInfo_isDefined (ainfo));
79 int annotationInfo_getValue (annotationInfo a) /*@*/
81 llassert (annotationInfo_isDefined (a));
86 bool annotationInfo_matchesContext (annotationInfo a, uentry ue)
89 ** Returns true iff the annotation context matches the uentry.
92 mtContextNode mcontext;
94 llassert (annotationInfo_isDefined (a));
95 mcontext = a->context;
97 if (mtContextNode_matchesEntry (mcontext, ue))
99 /* Matches annotation context, must also match meta state context. */
100 metaStateInfo minfo = a->state;
102 if (mtContextNode_matchesEntry (metaStateInfo_getContext (minfo), ue))
117 bool annotationInfo_matchesContextRef (annotationInfo a, sRef sr)
120 ** Returns true iff the annotation context matches the uentry.
123 mtContextNode mcontext;
125 llassert (annotationInfo_isDefined (a));
126 mcontext = a->context;
128 if (mtContextNode_matchesRef (mcontext, sr))
130 /* Matches annotation context, must also match meta state context. */
131 metaStateInfo minfo = a->state;
133 if (mtContextNode_matchesRef (metaStateInfo_getContext (minfo), sr))
148 cstring annotationInfo_dump (annotationInfo ainfo)
150 llassert (annotationInfo_isDefined (ainfo));
154 /*@observer@*/ annotationInfo annotationInfo_undump (char **s)
156 cstring mname = reader_readUntil (s, '.');
157 annotationInfo ainfo;
159 llassert (cstring_isDefined (mname));
160 ainfo = context_lookupAnnotation (mname);
162 if (annotationInfo_isUndefined (ainfo))
165 (message ("Library uses undefined annotation %s. Must use same -mts flags as when library was created.",
170 cstring_free (mname);
174 BADBRANCHRET (annotationInfo_undefined);
177 void annotationInfo_showContextRefError (annotationInfo a, sRef sr)
179 mtContextNode mcontext;
180 llassert (!annotationInfo_matchesContextRef (a, sr));
181 llassert (annotationInfo_isDefined (a));
182 mcontext = a->context;
184 if (mtContextNode_matchesRef (mcontext, sr))
186 /* Matches annotation context, must also match meta state context. */
187 metaStateInfo minfo = a->state;
189 if (mtContextNode_matchesRef (metaStateInfo_getContext (minfo), sr))
195 mtContextNode_showRefError (metaStateInfo_getContext (minfo), sr);
200 mtContextNode_showRefError (mcontext, sr);