]> andersk Git - splint.git/blame - src/constraintList.c
Changes to fix malloc size problem.
[splint.git] / src / constraintList.c
CommitLineData
616915dd 1/*
11db3170 2** Splint - annotation-assisted static program checker
616915dd 3** Copyright (C) 1994-2000 University of Virginia,
4** Massachusetts Institute of Technology
5**
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.
10**
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.
15**
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.
19**
155af98d 20** For information on splint: info@splint.org
21** To report a bug: splint-bug@splint.org
11db3170 22** For more information: http://www.splint.org
616915dd 23*/
65f973be 24
616915dd 25/*
26** constraintList.c
27**
28** based on list_template.c
29**
30** where T has T_equal (or change this) and T_unparse
31*/
32
1b8ae690 33# include "splintMacros.nf"
b73d1009 34# include "basic.h"
616915dd 35
28bf4b0b 36/*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/
37# define constraintList_elements_private_only(x, m_el) \
60eced23 38 { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
28bf4b0b 39 for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
40 { constraint m_el = *(m_elements++);
41
60eced23 42# define end_constraintList_elements_private_only }}}
28bf4b0b 43
44
60eced23 45/*@iter constraintList_elements_private (sef constraintList x, yield constraint el); @*/
d46ce6a4 46# define constraintList_elements_private(x, m_el) \
60eced23 47 { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
d46ce6a4 48 for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
49 { constraint m_el = *(m_elements++);
50
60eced23 51# define end_constraintList_elements_private }}}
d46ce6a4 52
53
03d670b6 54/*@only@*/ constraintList constraintList_makeNew ()
616915dd 55{
56 constraintList s = (constraintList) dmalloc (sizeof (*s));
57
58 s->nelements = 0;
59 s->nspace = constraintListBASESIZE;
60 s->elements = (constraint *)
61 dmalloc (sizeof (*s->elements) * constraintListBASESIZE);
02b84d4b 62
616915dd 63 return (s);
64}
65
66static void
67constraintList_grow (constraintList s)
68{
69 int i;
70 constraint *newelements;
71
60eced23 72 llassert (constraintList_isDefined (s));
73
616915dd 74 s->nspace += constraintListBASESIZE;
75 newelements = (constraint *) dmalloc (sizeof (*newelements)
76 * (s->nelements + s->nspace));
77
78 for (i = 0; i < s->nelements; i++)
79 {
80 newelements[i] = s->elements[i];
81 }
82
83 sfree (s->elements);
84 s->elements = newelements;
85}
86
c3e695ff 87
616915dd 88constraintList
bb25bea6 89constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
616915dd 90{
60eced23 91 llassert (constraintList_isDefined (s));
92
c3e695ff 93 /*drl7x */
b7b694d6 94
ae133592 95 if (constraintList_resolve (el, s))
d46ce6a4 96 {
ae133592 97 DPRINTF (("Resolved constraint: %s", constraint_unparse (el)));
d46ce6a4 98 constraint_free (el);
99 return s;
100 }
ae133592 101
102 DPRINTF (("Adding constraint: %s", constraint_unparse (el)));
616915dd 103
104 if (s->nspace <= 0)
105 constraintList_grow (s);
106
107 s->nspace--;
108 s->elements[s->nelements] = el;
109 s->nelements++;
110 return s;
111}
112
d46ce6a4 113/* frees everything but actual constraints */
114/* This function should only be used if you have
115 other references to unshared constraints
116*/
117static void constraintList_freeShallow (/*@only@*/ constraintList c)
118{
119 if (constraintList_isDefined(c) )
bb25bea6 120 {
121 free (c->elements);
122 c->elements = NULL;
123 c->nelements = -1;
124 c->nspace = -1;
125 }
d46ce6a4 126 free (c);
bb25bea6 127 c = NULL;
128}
129
779066e2 130/*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ /*@temp@*/ constraintList newList)
bb25bea6 131{
ae133592 132 llassert(constraintList_isDefined (s));
133 llassert(constraintList_isDefined (newList));
bb25bea6 134
28bf4b0b 135 if (newList == constraintList_undefined)
bb25bea6 136 return s;
137
28bf4b0b 138 constraintList_elements (newList, elem)
bb25bea6 139 {
ae133592 140 s = constraintList_add (s, constraint_copy(elem));
bb25bea6 141 }
142 end_constraintList_elements;
143
144 return s;
d46ce6a4 145}
146
28bf4b0b 147constraintList constraintList_addListFree (/*@returned@*/ constraintList s, /*@only@*/ constraintList newList)
616915dd 148{
517a2db3 149 if (constraintList_isUndefined (newList))
616915dd 150 return s;
517a2db3 151
152 llassert (constraintList_isDefined (s));
153 llassert (constraintList_isDefined (newList));
616915dd 154
28bf4b0b 155 constraintList_elements_private_only(newList, elem)
616915dd 156 {
517a2db3 157 s = constraintList_add (s, elem);
158 } end_constraintList_elements_private_only;
159
160 constraintList_freeShallow (newList);
161 return s;
616915dd 162}
163
7edb30e6 164constraintList constraintList_removeSurpressed (/*@only@*/ constraintList s)
165{
166 constraintList ret;
167 fileloc loc;
7edb30e6 168
517a2db3 169 llassert (constraintList_isDefined (s));
7edb30e6 170 ret = constraintList_makeNew();
171
517a2db3 172 constraintList_elements_private_only (s, elem)
7edb30e6 173 {
174 loc = constraint_getFileloc(elem);
175
bb7c2085 176 if (fileloc_isUndefined(loc))
7edb30e6 177 {
178 ret = constraintList_add (ret, elem);
179 }
bb7c2085 180 else if (context_suppressFlagMsg(FLG_BOUNDSWRITE, loc) )
7edb30e6 181 {
bb7c2085 182 DPRINTF ((message ("constraintList_removeSurpressed getting rid of surpressed constraint %q",
9a48d98c 183 constraint_unparse(elem))));
7edb30e6 184 constraint_free(elem);
185 }
bb7c2085 186 else if (!constraint_hasMaxSet(elem) && context_suppressFlagMsg(FLG_BOUNDSREAD, loc))
7edb30e6 187 {
bb7c2085 188 DPRINTF ((message("constraintList_removeSurpressed getting rid of surpressed constraint %q",
9a48d98c 189 constraint_unparse(elem))));
7edb30e6 190 constraint_free(elem);
191 }
192 else
193 {
194 ret = constraintList_add (ret, elem);
195 }
196 fileloc_free(loc);
517a2db3 197 } end_constraintList_elements_private_only;
7edb30e6 198
199 constraintList_freeShallow(s);
7edb30e6 200 return ret;
201}
202
15b3d2b2 203# if 0
f4ec8018 204static /*@only@*/ cstring
9a48d98c 205constraintList_unparseLocation (/*@temp@*/ constraintList s) /*@*/
f4ec8018 206{
207 int i;
208 cstring st = cstring_undefined;
209 bool first = TRUE;
210
211 if (!constraintList_isDefined (s))
212 {
213 return cstring_makeLiteral ("<undefined>");
214 }
215
216 if (s->nelements == 0)
217 {
218 st = cstring_makeLiteral("<List Empty>");
219 return st;
220 }
221
222 for (i = 0; i < s->nelements; i++)
223 {
224 cstring type = cstring_undefined;
225 constraint current = s->elements[i];
226
227 if (constraint_isDefined(current) )
228 {
229 cstring temp1;
9a48d98c 230 temp1 = constraint_unparseLocation(current);
f4ec8018 231 type = message ("%q %q\n", type, temp1 );
232 }
233
234 if (first)
235 {
236 st = type;
237 first = FALSE;
238 }
239 else
240 {
241 st = message ("%q, %q", st, type);
242 }
b7b694d6 243 }
f4ec8018 244
245 return st;
246}
15b3d2b2 247# endif
f4ec8018 248
920a3797 249/*@only@*/ cstring
9a48d98c 250constraintList_unparse (/*@temp@*/ constraintList s) /*@*/
616915dd 251{
252 int i;
253 cstring st = cstring_undefined;
254 bool first = TRUE;
60eced23 255
256 if (!constraintList_isDefined (s))
257 {
258 return cstring_makeLiteral ("<undefined>");
259 }
616915dd 260
261 if (s->nelements == 0)
d46ce6a4 262 {
263 st = cstring_makeLiteral("<List Empty>");
264 return st;
265 }
266
616915dd 267 for (i = 0; i < s->nelements; i++)
268 {
269 cstring type = cstring_undefined;
270 constraint current = s->elements[i];
271
28bf4b0b 272 if (constraint_isDefined(current) )
616915dd 273 {
90bc41f7 274 cstring temp1;
21f0106c 275
276 if (context_getFlag (FLG_ORCONSTRAINT))
277 {
2a6e9c30 278 temp1 = constraint_unparseOr (current);
21f0106c 279 }
280 else
281 {
9a48d98c 282 temp1 = constraint_unparse (current);
21f0106c 283 }
616915dd 284 type = message ("%q %q\n", type, temp1 );
285 }
286
287 if (first)
288 {
289 st = type;
290 first = FALSE;
291 }
292 else
293 {
294 st = message ("%q, %q", st, type);
295 }
b7b694d6 296 }
d46ce6a4 297
616915dd 298 return st;
299}
300
2a6e9c30 301void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
8f299805 302{
303
304 constraintList_elements (s, elem)
305 {
28bf4b0b 306 if (constraint_isDefined(elem))
8f299805 307 {
308 constraint_printErrorPostCondition (elem, loc);
309 }
310 }
311 end_constraintList_elements;
312 return;
313}
314
2a6e9c30 315void constraintList_printError (constraintList s, fileloc loc)
616915dd 316{
317
bb25bea6 318 constraintList_elements (s, elem)
616915dd 319 {
28bf4b0b 320 if (constraint_isDefined(elem) )
616915dd 321 {
84380658 322 if (constraint_isPost(elem) )
323 constraint_printErrorPostCondition (elem, loc);
324 else
325 constraint_printError (elem, loc);
616915dd 326 }
327 }
bb25bea6 328 end_constraintList_elements;
616915dd 329 return;
330}
331
8f299805 332
616915dd 333cstring
9a48d98c 334constraintList_unparseDetailed (constraintList s)
616915dd 335{
336 int i;
337 cstring st = cstring_undefined;
338 bool first = TRUE;
339
60eced23 340 if (!constraintList_isDefined (s))
341 {
342 return cstring_makeLiteral ("<undefined>");
343 }
344
616915dd 345 if (s->nelements == 0)
d46ce6a4 346 {
347 st = cstring_makeLiteral("<List Empty>");
348 return st;
349 }
350
616915dd 351 for (i = 0; i < s->nelements; i++)
352 {
353 cstring type = cstring_undefined;
354 constraint current = s->elements[i];
355
28bf4b0b 356 if (constraint_isDefined(current ) )
616915dd 357 {
9a48d98c 358 cstring temp1 = constraint_unparseDetailed (current);
616915dd 359 type = message ("%s %s\n", type, temp1 );
d46ce6a4 360 cstring_free(temp1);
616915dd 361 }
362
363 if (first)
364 {
365 st = type;
366 first = FALSE;
920a3797 367 type = NULL;
616915dd 368 }
369 else
370 {
920a3797 371 st = message ("%q %q", st, type);
616915dd 372 }
373 }
374 return st;
375}
376
377/*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
378} */
379
380constraintList
bb25bea6 381constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
616915dd 382{
383 constraint temp;
384 constraintList ret;
bb7c2085 385 DPRINTF ((message ("Logical or on %s and %s",
9a48d98c 386 constraintList_unparse(l1),
387 constraintList_unparse(l2)) ) );
616915dd 388
c3e695ff 389 ret = constraintList_makeNew();
bb25bea6 390 constraintList_elements (l1, el)
616915dd 391 {
28bf4b0b 392 temp = constraint_substitute (el, l2);
616915dd 393
28bf4b0b 394 if (constraintList_resolve (el, l2) || constraintList_resolve(temp,l2) )
616915dd 395 { /*avoid redundant constraints*/
28bf4b0b 396 if (!constraintList_resolve (el, ret) )
bb25bea6 397 {
398 constraint temp2;
399 temp2 = constraint_copy(el);
400 ret = constraintList_add (ret, temp2);
401 }
616915dd 402 }
d46ce6a4 403 constraint_free(temp);
616915dd 404 }
bb25bea6 405 end_constraintList_elements;
616915dd 406
bb25bea6 407 constraintList_elements (l2, el)
616915dd 408 {
28bf4b0b 409 temp = constraint_substitute (el, l1);
616915dd 410
28bf4b0b 411 if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) )
616915dd 412 {
413 /*avoid redundant constraints*/
28bf4b0b 414 if (!constraintList_resolve (el, ret) )
bb25bea6 415 {
416 constraint temp2;
417 temp2 = constraint_copy(el);
418 ret = constraintList_add (ret, temp2);
419 }
616915dd 420 }
d46ce6a4 421 constraint_free(temp);
616915dd 422 }
bb25bea6 423 end_constraintList_elements;
616915dd 424
425
426 return ret;
427}
428
429void
bb25bea6 430constraintList_free (/*@only@*/ constraintList s)
616915dd 431{
9a48d98c 432 if (constraintList_isDefined (s))
616915dd 433 {
9a48d98c 434 int i;
435
436 for (i = 0; i < s->nelements; i++)
437 {
438 constraint_free (s->elements[i]);
439 }
440
441 sfree (s->elements);
442 s->elements = NULL;
443 s->nelements = -1;
444 s->nspace = -1;
445 sfree (s);
446 s = NULL;
616915dd 447 }
616915dd 448}
449
450constraintList
03d670b6 451constraintList_copy (/*@observer@*/ /*@temp@*/ constraintList s)
616915dd 452{
c3e695ff 453 constraintList ret = constraintList_makeNew ();
616915dd 454
bb25bea6 455 constraintList_elements (s, el)
616915dd 456 {
457 ret = constraintList_add (ret, constraint_copy (el));
bb25bea6 458 } end_constraintList_elements;
616915dd 459
460 return ret;
461}
462
463constraintList constraintList_preserveOrig (constraintList c)
464{
9a48d98c 465 DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_unparse (c) ) ));
d46ce6a4 466
467 constraintList_elements_private (c, el)
616915dd 468 {
469 el = constraint_preserveOrig (el);
470 }
d46ce6a4 471 end_constraintList_elements_private;
616915dd 472 return c;
473}
474
03d670b6 475constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/ exprNode fcn)
4ab867d6 476{
9a48d98c 477 DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_unparse (c) ) ));
4ab867d6 478
479 constraintList_elements_private (c, el)
480 {
4ab867d6 481 el = constraint_setFcnPre(el);
482 el = constraint_origAddGeneratingExpr (el, fcn);
483 }
484 end_constraintList_elements_private;
485 return c;
486}
487
3814599d 488constraintList constraintList_single (constraint c)
489{
490 constraintList res;
491 res = constraintList_makeNew();
492 res = constraintList_add (res, c);
493 return res;
494}
4ab867d6 495
28bf4b0b 496constraintList constraintList_addGeneratingExpr (constraintList c,/*@dependent@*/ exprNode e)
9280addf 497{
498 DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) ));
499
d46ce6a4 500 constraintList_elements_private (c, el)
9280addf 501 {
9a48d98c 502 DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_unparse(el), exprNode_unparse(e) ) ));
9280addf 503 el = constraint_addGeneratingExpr (el, e);
504 }
d46ce6a4 505 end_constraintList_elements_private;
9280addf 506 return c;
507}
508
d46ce6a4 509/*@only@*/ constraintList constraintList_doFixResult (/*@only@*/constraintList postconditions, exprNode fcnCall)
616915dd 510{
511 constraintList ret;
c3e695ff 512 ret = constraintList_makeNew();
d46ce6a4 513 constraintList_elements_private (postconditions, el)
616915dd 514 {
515 ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) );
516 }
d46ce6a4 517 end_constraintList_elements_private;
616915dd 518
d46ce6a4 519 constraintList_free(postconditions);
616915dd 520 return ret;
521}
86d93ed3 522/*
523Commenting out because function is not yet stable
524
525/ *@only@* / constraintList constraintList_doSRefFixStructConstraint(constraintList invars, sRef s, ctype ct )
526{
527 constraintList ret;
528 ret = constraintList_makeNew();
529
530 constraintList_elements (invars, el)
531 {
532 ret = constraintList_add(ret, constraint_doSRefFixInvarConstraint (el, s, ct) );
533 }
534 end_constraintList_elements;
535
536 / * constraintList_free (invars);* /
537
538 return ret;
539}
540*/
616915dd 541
28bf4b0b 542/*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist)
616915dd 543{
544 constraintList ret;
c3e695ff 545 ret = constraintList_makeNew();
616915dd 546
bb25bea6 547 constraintList_elements (preconditions, el)
616915dd 548 {
549 ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
550 }
bb25bea6 551 end_constraintList_elements;
d46ce6a4 552
553 constraintList_free (preconditions);
616915dd 554
555 return ret;
556}
28bf4b0b 557constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/
616915dd 558 exprNodeList arglist)
559{
560 constraintList ret;
bb25bea6 561 constraint temp;
c3e695ff 562 ret = constraintList_makeNew();
616915dd 563
bb25bea6 564 constraintList_elements (preconditions, el)
616915dd 565 {
bb25bea6 566 temp = constraint_copy(el);
567 ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
616915dd 568 }
bb25bea6 569 end_constraintList_elements;
616915dd 570
571 return ret;
572}
573
574constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
575{
d46ce6a4 576 constraintList_elements_private (c, el)
616915dd 577 {
84c9ffbf 578 el = constraint_togglePost(el);
2934b455 579 if (constraint_hasOrig(el) )
4ab867d6 580 {
2934b455 581 el = constraint_togglePostOrig (el);
4ab867d6 582 }
616915dd 583 }
d46ce6a4 584 end_constraintList_elements_private;
616915dd 585 return c;
586}
587
920a3797 588/*@only@*/ constraintList constraintList_undump (FILE *f)
589{
590 constraintList ret;
3be9a165 591 char *s;
920a3797 592 char *os;
593
594 ret = constraintList_makeNew();
595
3be9a165 596 os = mstring_create (MAX_DUMP_LINE_LENGTH);
920a3797 597 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
598
599 while (s != NULL && *s != ';')
600 {
601 constraint temp;
602 char * c;
603
28bf4b0b 604 c = reader_getWord(&s);
920a3797 605
2e4caa51 606 if (! mstring_isDefined(c) )
607 {
608 llfatalbug(message("Library file is corrupted") );
609 }
610
611
920a3797 612 if (strcmp (c, "C") != 0)
613 {
614 llfatalbug(message("Error reading library. File may be corrupted"));
615 }
616
617 temp = constraint_undump (f);
618 ret = constraintList_add (ret, temp);
619 s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
620 free(c);
621 }
622 free(s);
623
624 return ret;
625}
626
627
628void constraintList_dump (/*@observer@*/ constraintList c, FILE *f)
629{
630 constraintList_elements (c, el)
631 {
632 fprintf(f, "C\n");
633 constraint_dump (el, f);
634 }
635 end_constraintList_elements; ;
636}
637
ae133592 638//! don't use this!
639void constraintList_castConstraints (constraintList c, ctype tfrom, ctype tto)
640{
641 if (TRUE) /* flag to allow casting */
642 {
643 int fsize = ctype_getSize (tfrom);
644 int tsize = ctype_getSize (tto);
645
646 DPRINTF (("Sizes: [%s] [%s] %d / %d", ctype_unparse (tfrom),
647 ctype_unparse (tto), fsize, tsize));
648
649 if (fsize == tsize)
650 {
651 return; /* Sizes match, no change to constraints */
652 }
653 else
654 {
655 float scale = fsize / tsize;
656
657 DPRINTF (("Scaling constraints by: %f", scale));
658
659 constraintList_elements (c, el)
660 {
661 DPRINTF (("Scale: %s", constraint_unparse (el)));
662 // constraint_scaleSize (el, scale);
663 DPRINTF ((" ==> %s", constraint_unparse (el)));
664 }
665 end_constraintList_elements;
666 }
667 }
668}
669
616915dd 670
02984642 671constraintList constraintList_sort (/*@returned@*/ constraintList ret)
672{
2e4caa51 673 if (constraintList_isUndefined(ret) )
674 {
675 llassert(FALSE);
676 return ret;
677 }
517a2db3 678
02984642 679 qsort (ret->elements, (size_t) ret->nelements,
15b3d2b2 680 (sizeof (*ret->elements)),
681 (int (*)(const void *, const void *)) constraint_compare);
682
683 DPRINTF((message("onstraint_sort returning") ));
02984642 684 return ret;
685}
f4ec8018 686
687
This page took 0.181222 seconds and 5 git commands to generate.