2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2000 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 ** based on list_template.c
30 ** where T has T_equal (or change this) and T_unparse
33 # include "splintMacros.nf"
36 /*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/
37 # define constraintList_elements_private_only(x, m_el) \
38 { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
39 for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
40 { constraint m_el = *(m_elements++);
42 # define end_constraintList_elements_private_only }}}
45 /*@iter constraintList_elements_private (sef constraintList x, yield constraint el); @*/
46 # define constraintList_elements_private(x, m_el) \
47 { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
48 for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
49 { constraint m_el = *(m_elements++);
51 # define end_constraintList_elements_private }}}
54 /*@only@*/ constraintList constraintList_makeNew ()
56 constraintList s = (constraintList) dmalloc (sizeof (*s));
59 s->nspace = constraintListBASESIZE;
60 s->elements = (constraint *)
61 dmalloc (sizeof (*s->elements) * constraintListBASESIZE);
67 constraintList_grow (constraintList s)
70 constraint *newelements;
72 llassert (constraintList_isDefined (s));
74 s->nspace += constraintListBASESIZE;
75 newelements = (constraint *) dmalloc (sizeof (*newelements)
76 * (s->nelements + s->nspace));
78 for (i = 0; i < s->nelements; i++)
80 newelements[i] = s->elements[i];
84 s->elements = newelements;
89 constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
91 llassert (constraintList_isDefined (s));
95 if (constraintList_resolve (el, s))
97 DPRINTF (("Resolved constraint: %s", constraint_unparse (el)));
102 DPRINTF (("Adding constraint: %s", constraint_unparse (el)));
105 constraintList_grow (s);
108 s->elements[s->nelements] = el;
113 /* frees everything but actual constraints */
114 /* This function should only be used if you have
115 other references to unshared constraints
117 static void constraintList_freeShallow (/*@only@*/ constraintList c)
119 if (constraintList_isDefined(c) )
130 /*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ /*@temp@*/ constraintList newList)
132 llassert(constraintList_isDefined (s));
133 llassert(constraintList_isDefined (newList));
135 if (newList == constraintList_undefined)
138 constraintList_elements (newList, elem)
140 s = constraintList_add (s, constraint_copy(elem));
142 end_constraintList_elements;
147 constraintList constraintList_addListFree (/*@returned@*/ constraintList s, /*@only@*/ constraintList newList)
149 if (constraintList_isUndefined (newList))
152 llassert (constraintList_isDefined (s));
153 llassert (constraintList_isDefined (newList));
155 constraintList_elements_private_only(newList, elem)
157 s = constraintList_add (s, elem);
158 } end_constraintList_elements_private_only;
160 constraintList_freeShallow (newList);
164 constraintList constraintList_removeSurpressed (/*@only@*/ constraintList s)
169 llassert (constraintList_isDefined (s));
170 ret = constraintList_makeNew();
172 constraintList_elements_private_only (s, elem)
174 loc = constraint_getFileloc(elem);
176 if (fileloc_isUndefined(loc))
178 ret = constraintList_add (ret, elem);
180 else if (context_suppressFlagMsg(FLG_BOUNDSWRITE, loc) )
182 DPRINTF ((message ("constraintList_removeSurpressed getting rid of surpressed constraint %q",
183 constraint_unparse(elem))));
184 constraint_free(elem);
186 else if (!constraint_hasMaxSet(elem) && context_suppressFlagMsg(FLG_BOUNDSREAD, loc))
188 DPRINTF ((message("constraintList_removeSurpressed getting rid of surpressed constraint %q",
189 constraint_unparse(elem))));
190 constraint_free(elem);
194 ret = constraintList_add (ret, elem);
197 } end_constraintList_elements_private_only;
199 constraintList_freeShallow(s);
204 static /*@only@*/ cstring
205 constraintList_unparseLocation (/*@temp@*/ constraintList s) /*@*/
208 cstring st = cstring_undefined;
211 if (!constraintList_isDefined (s))
213 return cstring_makeLiteral ("<undefined>");
216 if (s->nelements == 0)
218 st = cstring_makeLiteral("<List Empty>");
222 for (i = 0; i < s->nelements; i++)
224 cstring type = cstring_undefined;
225 constraint current = s->elements[i];
227 if (constraint_isDefined(current) )
230 temp1 = constraint_unparseLocation(current);
231 type = message ("%q %q\n", type, temp1 );
241 st = message ("%q, %q", st, type);
250 constraintList_unparse (/*@temp@*/ constraintList s) /*@*/
253 cstring st = cstring_undefined;
256 if (!constraintList_isDefined (s))
258 return cstring_makeLiteral ("<undefined>");
261 if (s->nelements == 0)
263 st = cstring_makeLiteral("<List Empty>");
267 for (i = 0; i < s->nelements; i++)
269 cstring type = cstring_undefined;
270 constraint current = s->elements[i];
272 if (constraint_isDefined(current) )
276 if (context_getFlag (FLG_ORCONSTRAINT))
278 temp1 = constraint_unparseOr (current);
282 temp1 = constraint_unparse (current);
284 type = message ("%q %q\n", type, temp1 );
294 st = message ("%q, %q", st, type);
301 void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
304 constraintList_elements (s, elem)
306 if (constraint_isDefined(elem))
308 constraint_printErrorPostCondition (elem, loc);
311 end_constraintList_elements;
315 void constraintList_printError (constraintList s, fileloc loc)
318 constraintList_elements (s, elem)
320 if (constraint_isDefined(elem) )
322 if (constraint_isPost(elem) )
323 constraint_printErrorPostCondition (elem, loc);
325 constraint_printError (elem, loc);
328 end_constraintList_elements;
334 constraintList_unparseDetailed (constraintList s)
337 cstring st = cstring_undefined;
340 if (!constraintList_isDefined (s))
342 return cstring_makeLiteral ("<undefined>");
345 if (s->nelements == 0)
347 st = cstring_makeLiteral("<List Empty>");
351 for (i = 0; i < s->nelements; i++)
353 cstring type = cstring_undefined;
354 constraint current = s->elements[i];
356 if (constraint_isDefined(current ) )
358 cstring temp1 = constraint_unparseDetailed (current);
359 type = message ("%s %s\n", type, temp1 );
371 st = message ("%q %q", st, type);
377 /*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
381 constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
385 DPRINTF ((message ("Logical or on %s and %s",
386 constraintList_unparse(l1),
387 constraintList_unparse(l2)) ) );
389 ret = constraintList_makeNew();
390 constraintList_elements (l1, el)
392 temp = constraint_substitute (el, l2);
394 if (constraintList_resolve (el, l2) || constraintList_resolve(temp,l2) )
395 { /*avoid redundant constraints*/
396 if (!constraintList_resolve (el, ret) )
399 temp2 = constraint_copy(el);
400 ret = constraintList_add (ret, temp2);
403 constraint_free(temp);
405 end_constraintList_elements;
407 constraintList_elements (l2, el)
409 temp = constraint_substitute (el, l1);
411 if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) )
413 /*avoid redundant constraints*/
414 if (!constraintList_resolve (el, ret) )
417 temp2 = constraint_copy(el);
418 ret = constraintList_add (ret, temp2);
421 constraint_free(temp);
423 end_constraintList_elements;
430 constraintList_free (/*@only@*/ constraintList s)
432 if (constraintList_isDefined (s))
436 for (i = 0; i < s->nelements; i++)
438 constraint_free (s->elements[i]);
451 constraintList_copy (/*@observer@*/ /*@temp@*/ constraintList s)
453 constraintList ret = constraintList_makeNew ();
455 constraintList_elements (s, el)
457 ret = constraintList_add (ret, constraint_copy (el));
458 } end_constraintList_elements;
463 constraintList constraintList_preserveOrig (constraintList c)
465 DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_unparse (c) ) ));
467 constraintList_elements_private (c, el)
469 el = constraint_preserveOrig (el);
471 end_constraintList_elements_private;
475 constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/ exprNode fcn)
477 DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_unparse (c) ) ));
479 constraintList_elements_private (c, el)
481 el = constraint_setFcnPre(el);
482 el = constraint_origAddGeneratingExpr (el, fcn);
484 end_constraintList_elements_private;
488 constraintList constraintList_single (constraint c)
491 res = constraintList_makeNew();
492 res = constraintList_add (res, c);
496 constraintList constraintList_addGeneratingExpr (constraintList c,/*@dependent@*/ exprNode e)
498 DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) ));
500 constraintList_elements_private (c, el)
502 DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_unparse(el), exprNode_unparse(e) ) ));
503 el = constraint_addGeneratingExpr (el, e);
505 end_constraintList_elements_private;
509 /*@only@*/ constraintList constraintList_doFixResult (/*@only@*/constraintList postconditions, exprNode fcnCall)
512 ret = constraintList_makeNew();
513 constraintList_elements_private (postconditions, el)
515 ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) );
517 end_constraintList_elements_private;
519 constraintList_free(postconditions);
523 Commenting out because function is not yet stable
525 / *@only@* / constraintList constraintList_doSRefFixStructConstraint(constraintList invars, sRef s, ctype ct )
528 ret = constraintList_makeNew();
530 constraintList_elements (invars, el)
532 ret = constraintList_add(ret, constraint_doSRefFixInvarConstraint (el, s, ct) );
534 end_constraintList_elements;
536 / * constraintList_free (invars);* /
542 /*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist)
545 ret = constraintList_makeNew();
547 constraintList_elements (preconditions, el)
549 ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
551 end_constraintList_elements;
553 constraintList_free (preconditions);
557 constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/
558 exprNodeList arglist)
562 ret = constraintList_makeNew();
564 constraintList_elements (preconditions, el)
566 temp = constraint_copy(el);
567 ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
569 end_constraintList_elements;
574 constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
576 constraintList_elements_private (c, el)
578 el = constraint_togglePost(el);
579 if (constraint_hasOrig(el) )
581 el = constraint_togglePostOrig (el);
584 end_constraintList_elements_private;
588 /*@only@*/ constraintList constraintList_undump (FILE *f)
594 ret = constraintList_makeNew();
596 os = mstring_create (MAX_DUMP_LINE_LENGTH);
597 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
599 while (s != NULL && *s != ';')
604 c = reader_getWord(&s);
606 if (! mstring_isDefined(c) )
608 llfatalbug(message("Library file is corrupted") );
612 if (strcmp (c, "C") != 0)
614 llfatalbug(message("Error reading library. File may be corrupted"));
617 temp = constraint_undump (f);
618 ret = constraintList_add (ret, temp);
619 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
628 void constraintList_dump (/*@observer@*/ constraintList c, FILE *f)
630 constraintList_elements (c, el)
633 constraint_dump (el, f);
635 end_constraintList_elements; ;
638 constraintList constraintList_sort (/*@returned@*/ constraintList ret)
640 if (constraintList_isUndefined(ret) )
646 qsort (ret->elements, (size_t) ret->nelements,
647 (sizeof (*ret->elements)),
648 (int (*)(const void *, const void *)) constraint_compare);
650 DPRINTF((message("onstraint_sort returning") ));