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 /*@-nullderef@*/ /* !!! DRL needs to fix this code! */
37 /*@-nullstate@*/ /* !!! DRL needs to fix this code! */
38 /*@-nullpass@*/ /* !!! DRL needs to fix this code! */
39 /*@-temptrans@*/ /* !!! DRL needs to fix this code! */
41 /*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/
42 # define constraintList_elements_private_only(x, m_el) \
43 { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
44 for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
45 { constraint m_el = *(m_elements++);
47 # define end_constraintList_elements_private_only }}}
50 /*@iter constraintList_elements_private (sef constraintList x, yield constraint el); @*/
51 # define constraintList_elements_private(x, m_el) \
52 { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
53 for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
54 { constraint m_el = *(m_elements++);
56 # define end_constraintList_elements_private }}}
59 /*@only@*/ constraintList constraintList_makeNew ()
61 constraintList s = (constraintList) dmalloc (sizeof (*s));
64 s->nspace = constraintListBASESIZE;
65 s->elements = (constraint *)
66 dmalloc (sizeof (*s->elements) * constraintListBASESIZE);
72 constraintList_grow (constraintList s)
75 constraint *newelements;
77 llassert (constraintList_isDefined (s));
79 s->nspace += constraintListBASESIZE;
80 newelements = (constraint *) dmalloc (sizeof (*newelements)
81 * (s->nelements + s->nspace));
83 for (i = 0; i < s->nelements; i++)
85 newelements[i] = s->elements[i];
89 s->elements = newelements;
94 constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
96 llassert (constraintList_isDefined (s));
100 if (constraintList_resolve (el, s) )
102 constraint_free (el);
107 constraintList_grow (s);
110 s->elements[s->nelements] = el;
115 /* frees everything but actual constraints */
116 /* This function should only be used if you have
117 other references to unshared constraints
119 static void constraintList_freeShallow (/*@only@*/ constraintList c)
121 if (constraintList_isDefined(c) )
132 /*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ /*@temp@*/ constraintList newList)
134 llassert(constraintList_isDefined(s) );
135 llassert(constraintList_isDefined(newList) );
137 if (newList == constraintList_undefined)
140 constraintList_elements (newList, elem)
142 s = constraintList_add (s, constraint_copy(elem) );
144 end_constraintList_elements;
149 constraintList constraintList_addListFree (/*@returned@*/ constraintList s, /*@only@*/ constraintList newList)
151 llassert(constraintList_isDefined(s) );
152 llassert(constraintList_isDefined(newList) );
154 if (constraintList_isUndefined(newList) )
157 constraintList_elements_private_only(newList, elem)
159 s = constraintList_add (s, elem);
161 end_constraintList_elements_private_only
163 constraintList_freeShallow(newList);
168 constraintList constraintList_removeSurpressed (/*@only@*/ constraintList s)
172 llassert(constraintList_isDefined(s) );
174 ret = constraintList_makeNew();
176 constraintList_elements_private_only(s, elem)
178 loc = constraint_getFileloc(elem);
180 if (fileloc_isUndefined(loc))
182 ret = constraintList_add (ret, elem);
185 else if (context_suppressFlagMsg(FLG_BOUNDSWRITE, loc) )
187 DPRINTF ((message ("constraintList_removeSurpressed getting rid of surpressed constraint %q",
188 constraint_print(elem))));
189 constraint_free(elem);
192 else if (!constraint_hasMaxSet(elem) && context_suppressFlagMsg(FLG_BOUNDSREAD, loc))
194 DPRINTF ((message("constraintList_removeSurpressed getting rid of surpressed constraint %q",
195 constraint_print(elem))));
196 constraint_free(elem);
200 ret = constraintList_add (ret, elem);
204 end_constraintList_elements_private_only;
206 constraintList_freeShallow(s);
212 extern /*@only@*/ cstring constraintList_unparse ( /*@observer@*/ constraintList s) /*@*/
214 return (constraintList_print(s));
218 static /*@only@*/ cstring
219 constraintList_printLocation (/*@temp@*/ constraintList s) /*@*/
222 cstring st = cstring_undefined;
225 if (!constraintList_isDefined (s))
227 return cstring_makeLiteral ("<undefined>");
230 if (s->nelements == 0)
232 st = cstring_makeLiteral("<List Empty>");
236 for (i = 0; i < s->nelements; i++)
238 cstring type = cstring_undefined;
239 constraint current = s->elements[i];
241 if (constraint_isDefined(current) )
244 temp1 = constraint_printLocation(current);
245 type = message ("%q %q\n", type, temp1 );
255 st = message ("%q, %q", st, type);
264 constraintList_print (/*@temp@*/ constraintList s) /*@*/
267 cstring st = cstring_undefined;
270 if (!constraintList_isDefined (s))
272 return cstring_makeLiteral ("<undefined>");
275 if (s->nelements == 0)
277 st = cstring_makeLiteral("<List Empty>");
281 for (i = 0; i < s->nelements; i++)
283 cstring type = cstring_undefined;
284 constraint current = s->elements[i];
286 if (constraint_isDefined(current) )
290 if (context_getFlag (FLG_ORCONSTRAINT))
292 temp1 = constraint_printOr(current);
296 temp1 = constraint_print (current);
298 type = message ("%q %q\n", type, temp1 );
308 st = message ("%q, %q", st, type);
315 void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
318 constraintList_elements (s, elem)
320 if (constraint_isDefined(elem))
322 constraint_printErrorPostCondition (elem, loc);
325 end_constraintList_elements;
329 void constraintList_printError (constraintList s, fileloc loc)
332 constraintList_elements (s, elem)
334 if (constraint_isDefined(elem) )
336 if (constraint_isPost(elem) )
337 constraint_printErrorPostCondition (elem, loc);
339 constraint_printError (elem, loc);
342 end_constraintList_elements;
348 constraintList_printDetailed (constraintList s)
351 cstring st = cstring_undefined;
354 if (!constraintList_isDefined (s))
356 return cstring_makeLiteral ("<undefined>");
359 if (s->nelements == 0)
361 st = cstring_makeLiteral("<List Empty>");
365 for (i = 0; i < s->nelements; i++)
367 cstring type = cstring_undefined;
368 constraint current = s->elements[i];
370 if (constraint_isDefined(current ) )
372 cstring temp1 = constraint_printDetailed (current);
373 type = message ("%s %s\n", type, temp1 );
385 st = message ("%q %q", st, type);
391 /*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
395 constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
399 DPRINTF ((message ("Logical or on %s and %s",
400 constraintList_print(l1),
401 constraintList_print(l2)) ) );
403 ret = constraintList_makeNew();
404 constraintList_elements (l1, el)
406 temp = constraint_substitute (el, l2);
408 if (constraintList_resolve (el, l2) || constraintList_resolve(temp,l2) )
409 { /*avoid redundant constraints*/
410 if (!constraintList_resolve (el, ret) )
413 temp2 = constraint_copy(el);
414 ret = constraintList_add (ret, temp2);
417 constraint_free(temp);
419 end_constraintList_elements;
421 constraintList_elements (l2, el)
423 temp = constraint_substitute (el, l1);
425 if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) )
427 /*avoid redundant constraints*/
428 if (!constraintList_resolve (el, ret) )
431 temp2 = constraint_copy(el);
432 ret = constraintList_add (ret, temp2);
435 constraint_free(temp);
437 end_constraintList_elements;
444 constraintList_free (/*@only@*/ constraintList s)
448 llassert(constraintList_isDefined(s) );
451 for (i = 0; i < s->nelements; i++)
453 constraint_free (s->elements[i]);
465 constraintList_copy (/*@observer@*/ /*@temp@*/ constraintList s)
467 constraintList ret = constraintList_makeNew ();
469 constraintList_elements (s, el)
471 ret = constraintList_add (ret, constraint_copy (el));
472 } end_constraintList_elements;
477 constraintList constraintList_preserveOrig (constraintList c)
479 DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
481 constraintList_elements_private (c, el)
483 el = constraint_preserveOrig (el);
485 end_constraintList_elements_private;
489 constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/ exprNode fcn)
491 DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_print (c) ) ));
493 constraintList_elements_private (c, el)
495 el = constraint_setFcnPre(el);
496 el = constraint_origAddGeneratingExpr (el, fcn);
498 end_constraintList_elements_private;
502 constraintList constraintList_single (constraint c)
505 res = constraintList_makeNew();
506 res = constraintList_add (res, c);
510 constraintList constraintList_addGeneratingExpr (constraintList c,/*@dependent@*/ exprNode e)
512 DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) ));
514 constraintList_elements_private (c, el)
516 DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(el), exprNode_unparse(e) ) ));
517 el = constraint_addGeneratingExpr (el, e);
519 end_constraintList_elements_private;
523 /*@only@*/ constraintList constraintList_doFixResult (/*@only@*/constraintList postconditions, exprNode fcnCall)
526 ret = constraintList_makeNew();
527 constraintList_elements_private (postconditions, el)
529 ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) );
531 end_constraintList_elements_private;
533 constraintList_free(postconditions);
537 Commenting out because function is not yet stable
539 / *@only@* / constraintList constraintList_doSRefFixStructConstraint(constraintList invars, sRef s, ctype ct )
542 ret = constraintList_makeNew();
544 constraintList_elements (invars, el)
546 ret = constraintList_add(ret, constraint_doSRefFixInvarConstraint (el, s, ct) );
548 end_constraintList_elements;
550 / * constraintList_free (invars);* /
556 /*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist)
559 ret = constraintList_makeNew();
561 constraintList_elements (preconditions, el)
563 ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
565 end_constraintList_elements;
567 constraintList_free (preconditions);
571 constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/
572 exprNodeList arglist)
576 ret = constraintList_makeNew();
578 constraintList_elements (preconditions, el)
580 temp = constraint_copy(el);
581 ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
583 end_constraintList_elements;
588 constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
590 constraintList_elements_private (c, el)
592 el = constraint_togglePost(el);
593 if (constraint_hasOrig(el) )
595 el = constraint_togglePostOrig (el);
598 end_constraintList_elements_private;
602 /*@only@*/ constraintList constraintList_undump (FILE *f)
608 ret = constraintList_makeNew();
610 os = mstring_create (MAX_DUMP_LINE_LENGTH);
611 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
613 while (s != NULL && *s != ';')
618 c = reader_getWord(&s);
620 if (strcmp (c, "C") != 0)
622 llfatalbug(message("Error reading library. File may be corrupted"));
625 temp = constraint_undump (f);
626 ret = constraintList_add (ret, temp);
627 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
636 void constraintList_dump (/*@observer@*/ constraintList c, FILE *f)
638 constraintList_elements (c, el)
641 constraint_dump (el, f);
643 end_constraintList_elements; ;
647 constraintList constraintList_sort (/*@returned@*/ constraintList ret)
649 qsort (ret->elements, (size_t) ret->nelements,
650 (sizeof (*ret->elements)),
651 (int (*)(const void *, const void *)) constraint_compare);
653 DPRINTF((message("onstraint_sort returning") ));