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
);
179 void annotationInfo_showContextRefError (annotationInfo a
, sRef sr
)
181 mtContextNode mcontext
;
182 llassert (!annotationInfo_matchesContextRef (a
, sr
));
183 llassert (annotationInfo_isDefined (a
));
184 mcontext
= a
->context
;
186 if (mtContextNode_matchesRef (mcontext
, sr
))
188 /* Matches annotation context, must also match meta state context. */
189 metaStateInfo minfo
= a
->state
;
191 if (mtContextNode_matchesRef (metaStateInfo_getContext (minfo
), sr
))
197 mtContextNode_showRefError (metaStateInfo_getContext (minfo
), sr
);
202 mtContextNode_showRefError (mcontext
, sr
);
205 # endif /* DEADCODE */