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 static /*@notnull@*/ stateClauseList stateClauseList_new (void)
33 stateClauseList s = (stateClauseList) dmalloc (sizeof (*s));
36 s->nspace = stateClauseListBASESIZE;
37 s->elements = (stateClause *)
38 dmalloc (sizeof (*s->elements) * stateClauseListBASESIZE);
44 stateClauseList_grow (stateClauseList s)
47 stateClause *newelements;
49 llassert (stateClauseList_isDefined (s));
51 s->nspace += stateClauseListBASESIZE;
53 newelements = (stateClause *)
54 dmalloc (sizeof (*newelements) * (s->nelements + s->nspace));
56 for (i = 0; i < s->nelements; i++)
58 newelements[i] = s->elements[i];
62 s->elements = newelements;
65 stateClauseList stateClauseList_add (stateClauseList s, stateClause el)
67 DPRINTF (("Adding: %s", stateClause_unparse (el)));
69 if (stateClauseList_isUndefined (s))
71 s = stateClauseList_new ();
75 stateClauseList_elements (s, cl)
77 if (stateClause_sameKind (cl, el))
81 message ("Multiple %q clauses for one function (ignoring second)",
82 stateClause_unparseKind (cl)),
85 stateClause_free (el);
88 } end_stateClauseList_elements ;
93 stateClauseList_grow (s);
97 s->elements[s->nelements] = el;
103 cstring stateClauseList_unparse (stateClauseList s)
105 cstring st = cstring_undefined;
108 if (stateClauseList_isDefined (s))
110 for (i = 0; i < stateClauseList_size (s); i++)
114 st = message ("%q;", stateClause_unparse (s->elements[i]));
117 st = message ("%q %q;", st, stateClause_unparse (s->elements[i]));
124 stateClauseList stateClauseList_copy (stateClauseList s)
126 if (stateClauseList_isDefined (s))
128 stateClauseList t = (stateClauseList) dmalloc (sizeof (*t));
131 t->nelements = s->nelements;
134 if (s->nelements > 0)
136 t->elements = (stateClause *) dmalloc (sizeof (*t->elements) * t->nelements);
137 for (i = 0; i < s->nelements; i++)
139 t->elements[i] = stateClause_copy (s->elements[i]);
151 return stateClauseList_undefined;
156 stateClauseList_free (stateClauseList s)
158 if (!stateClauseList_isUndefined (s))
162 for (i = 0; i < s->nelements; i++)
164 stateClause_free (s->elements[i]);
172 cstring stateClauseList_dump (stateClauseList s)
174 cstring st = cstring_undefined;
176 if (stateClauseList_isUndefined (s)) return st;
178 stateClauseList_elements (s, current)
180 st = message ("%q%q$", st, stateClause_dump (current));
181 } end_stateClauseList_elements;
186 stateClauseList stateClauseList_undump (char **s)
189 stateClauseList pn = stateClauseList_new ();
194 while (c != '#' && c != '@')
196 stateClause sc = stateClause_undump (s);
198 pn = stateClauseList_add (pn, sc);
199 reader_checkChar (s, '$');
207 int stateClauseList_compare (stateClauseList s1, stateClauseList s2)
209 if (stateClauseList_isUndefined (s1)
210 && stateClauseList_isUndefined (s2))
216 if (s1 - s2 > 0) /* evans 2001-08-21: was (int) s1 > (int) s2) */
227 static /*@exposed@*/ sRefSet
228 stateClauseList_getClause (stateClauseList s, stateClause k)
230 stateClauseList_elements (s, el)
232 if (stateClause_matchKind (el, k))
234 return stateClause_getRefs (el);
236 } end_stateClauseList_elements ;
238 return sRefSet_undefined;
241 void stateClauseList_checkAll (uentry ue)
243 stateClauseList clauses = uentry_getStateClauseList (ue);
244 sRef res = uentry_getSref (ue);
245 bool specialResult = FALSE;
247 DPRINTF (("Check state clauses: %s", uentry_unparseFull (ue)));
249 stateClauseList_elements (clauses, cl)
251 bool isPre = stateClause_isBeforeOnly (cl);
253 if (stateClause_isGlobal (cl))
259 sRefSet refs = stateClause_getRefs (cl);
261 sRefSet_allElements (refs, el)
263 sRef rb = sRef_getRootBase (el);
265 DPRINTF (("Check: %s", sRef_unparse (el)));
267 if (sRef_isResult (rb))
270 ** The result type is now know, need to set it:
273 if (ctype_isUnknown (sRef_getType (rb)))
275 ctype utype = uentry_getType (ue);
276 llassert (ctype_isFunction (utype));
278 sRef_setTypeFull (rb, ctype_getReturnType (utype));
279 DPRINTF (("el: %s", sRef_unparseFull (el)));
283 if (stateClause_setsMetaState (cl))
285 qual q = stateClause_getMetaQual (cl);
286 annotationInfo qa = qual_getAnnotationInfo (q);
288 if (!annotationInfo_matchesContextRef (qa, el))
291 (FLG_ANNOTATIONERROR,
292 message ("Attribute annotation %s used on inappropriate reference %q in %q clause of %q: %q",
295 stateClause_unparseKind (cl),
297 stateClause_unparse (cl)),
298 uentry_whereLast (ue)))
300 /*@i! annotationInfo_showContextError (ainfo, ue); */
305 if (sRef_isResult (rb))
311 message ("Function result is used in %q clause of %q "
312 "(%q applies to the state before function is "
313 "called, so should not use result): %q",
314 stateClause_unparseKind (cl),
316 stateClause_unparseKind (cl),
318 uentry_whereLast (ue));
322 if (!sRef_isStateSpecial (res))
324 DPRINTF (("Here we are: %s", sRef_unparseFull (res)));
328 sstate pstate = sRef_getDefState (res);
330 if (!sRef_makeStateSpecial (res))
334 message ("Function result is used in %q clause of %q "
335 "but was previously annotated with %s: %q",
336 stateClause_unparseKind (cl),
338 sstate_unparse (pstate),
340 uentry_whereLast (ue)))
342 specialResult = TRUE;
348 DPRINTF (("Fixing result type! %s", sRef_unparseFull (el)));
349 (void) sRef_fixResultType (el, sRef_getType (res), ue);
352 else if (sRef_isParam (rb))
354 DPRINTF (("Make special: %s", sRef_unparseFull (rb)));
356 if (!sRef_makeStateSpecial (rb))
358 if (fileloc_isXHFile (uentry_whereLast (ue)))
360 ; /* Okay to override in .xh files */
362 else if (stateClause_isQual (cl))
364 ; /* qual clauses don't interfere with definition state */
370 message ("Reference %q used in %q clause of %q, "
371 "but was previously annotated with %s: %q",
373 stateClause_unparseKind (cl),
375 sstate_unparse (sRef_getDefState (res)),
377 uentry_whereLast (ue));
381 DPRINTF (("Made special: %s", sRef_unparseFull (rb)));
383 else if (sRef_isInvalid (rb))
385 /*@innercontinue@*/ continue;
390 /*@innercontinue@*/ continue;
393 if (stateClause_isMemoryAllocation (cl))
395 if (!ctype_isVisiblySharable (sRef_getType (el)))
398 (FLG_ANNOTATIONERROR,
399 /*@-sefparams@*/ /* This is okay because its fresh storage. */ /*@i32@*/
401 ("%q clauses includes %q of "
402 "non-dynamically allocated type %s",
403 cstring_capitalizeFree (stateClause_unparseKind (cl)),
405 ctype_unparse (sRef_getType (el))),
406 uentry_whereLast (ue));
411 } end_sRefSet_allElements ;
413 } end_stateClauseList_elements ;
416 void stateClauseList_checkEqual (uentry old, uentry unew)
418 stateClauseList oldClauses = uentry_getStateClauseList (old);
419 stateClauseList newClauses = uentry_getStateClauseList (unew);
421 if (stateClauseList_isDefined (newClauses))
423 stateClauseList_elements (newClauses, cl)
425 if (stateClause_isGlobal (cl))
431 sRefSet sc = stateClauseList_getClause (oldClauses, cl);
433 if (!sRefSet_equal (sc, stateClause_getRefs (cl)))
437 message ("Function %q %rdeclared with inconsistent %q clause: %q",
438 uentry_getName (old),
439 uentry_isDeclared (old),
440 stateClause_unparseKind (cl),
441 sRefSet_unparsePlain (stateClause_getRefs (cl))),
444 uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc));
448 } end_stateClauseList_elements ;
450 stateClauseList_elements (oldClauses, cl)
452 if (stateClause_isGlobal (cl))
458 sRefSet sc = stateClauseList_getClause (newClauses, cl);
460 if (sRefSet_isUndefined (sc) && !sRefSet_isEmpty (stateClause_getRefs (cl)))
464 message ("Function %q %rdeclared without %q clause (either "
465 "use no special clauses in redeclaration, or "
466 "they must match exactly: %q",
467 uentry_getName (old),
468 uentry_isDeclared (old),
469 stateClause_unparseKind (cl),
470 sRefSet_unparsePlain (stateClause_getRefs (cl))),
473 uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc));
477 } end_stateClauseList_elements ;