]> andersk Git - splint.git/blame - src/constraint.c
andersk / splint.git / blame
? search:
summary | shortlog | log | commit | commitdiff | tree
blob | blame (incremental) | history | HEAD
*** empty log message ***
[splint.git] / src / constraint.c
CommitLineData
616915dd 1/*
4ab867d6 2** constraint.c
616915dd 3*/
4
5//#define DEBUGPRINT 1
6
7# include <ctype.h> /* for isdigit */
8# include "lclintMacros.nf"
9# include "basic.h"
10# include "cgrammar.h"
11# include "cgrammar_tokens.h"
616915dd 12# include "exprChecks.h"
616915dd 13# include "exprNodeSList.h"
616915dd 14
15/*@i33*/
616915dd 16
c3e695ff 17/*@access exprNode @*/
616915dd 18
d46ce6a4 19
28bf4b0b 20static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
2934b455 21
22
4ab867d6 23static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
24 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
25
d46ce6a4 26/* constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */
616915dd 27
d46ce6a4 28/* { */
29/* char *t; */
30/* int c; */
31/* constraint ret; */
32/* ret = constraint_makeNew(); */
33/* llassert (sRef_isValid(x) ); */
34/* if (!sRef_isValid(x)) */
35/* return ret; */
616915dd 36
37
d46ce6a4 38/* ret->lexpr = constraintExpr_makeTermsRef (x); */
39/* #warning fix abstraction */
616915dd 40
d46ce6a4 41/* if (relOp.tok == GE_OP) */
42/* ret->ar = GTE; */
43/* else if (relOp.tok == LE_OP) */
44/* ret->ar = LTE; */
45/* else if (relOp.tok == EQ_OP) */
46/* ret->ar = EQ; */
47/* else */
48/* llfatalbug(message ("Unsupported relational operator") ); */
616915dd 49
50
d46ce6a4 51/* t = cstring_toCharsSafe (exprNode_unparse(cconstant)); */
52/* c = atoi( t ); */
53/* ret->expr = constraintExpr_makeIntLiteral (c); */
616915dd 54
d46ce6a4 55/* ret->post = TRUE; */
56/* // ret->orig = ret; */
57/* DPRINTF(("GENERATED CONSTRAINT:")); */
58/* DPRINTF( (message ("%s", constraint_print(ret) ) ) ); */
59/* return ret; */
60/* } */
616915dd 61
920a3797 62
63static void
64advanceField (char **s)
65{
28bf4b0b 66 reader_checkChar (s, '@');
920a3797 67}
68
69
70
28bf4b0b 71static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
616915dd 72{
73 char *t;
74 int c;
75 constraint ret;
76 ret = constraint_makeNew();
28bf4b0b 77 llassert (constraintExpr_isDefined(l) );
d46ce6a4 78
616915dd 79 ret->lexpr = constraintExpr_copy (l);
2934b455 80
616915dd 81
82 if (relOp.tok == GE_OP)
83 ret->ar = GTE;
84 else if (relOp.tok == LE_OP)
85 ret->ar = LTE;
86 else if (relOp.tok == EQ_OP)
87 ret->ar = EQ;
88 else
dc92450f 89 llfatalbug(message("Unsupported relational operator") );
616915dd 90
91
92 t = cstring_toCharsSafe (exprNode_unparse(cconstant));
93 c = atoi( t );
94 ret->expr = constraintExpr_makeIntLiteral (c);
95
96 ret->post = TRUE;
97 // ret->orig = ret;
98 DPRINTF(("GENERATED CONSTRAINT:"));
99 DPRINTF( (message ("%s", constraint_print(ret) ) ) );
100 return ret;
101}
102
c3e695ff 103bool constraint_same (constraint c1, constraint c2)
90bc41f7 104{
105
106 if (c1->ar != c2->ar)
107 return FALSE;
108
109 if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
110 return FALSE;
111
112 if (!constraintExpr_similar (c1->expr, c2->expr) )
113 return FALSE;
114
115 return TRUE;
116}
616915dd 117
118constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
119{
120 constraint ret;
121 ret = constraint_makeNew();
28bf4b0b 122 llassert (constraintExpr_isDefined(l) );
616915dd 123
124 ret->lexpr = constraintExpr_copy (l);
616915dd 125
126 if (relOp.tok == GE_OP)
127 ret->ar = GTE;
128 else if (relOp.tok == LE_OP)
129 ret->ar = LTE;
130 else if (relOp.tok == EQ_OP)
131 ret->ar = EQ;
132 else
dc92450f 133 llfatalbug( message("Unsupported relational operator") );
616915dd 134
135 ret->expr = constraintExpr_copy (r);
136
137 ret->post = TRUE;
90bc41f7 138
139 ret->orig = constraint_copy(ret);
140
141 ret = constraint_simplify (ret);
142
616915dd 143 // ret->orig = ret;
144 DPRINTF(("GENERATED CONSTRAINT:"));
145 DPRINTF( (message ("%s", constraint_print(ret) ) ) );
146 return ret;
147}
148
28bf4b0b 149constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
616915dd 150{
151 constraint ret;
90bc41f7 152
c3e695ff 153 llassert (constraint_isDefined(c) );
28bf4b0b 154 // DPRINTF((message("Copying constraint %q", constraint_print) ));
90bc41f7 155
616915dd 156 ret = constraint_makeNew();
157 ret->lexpr = constraintExpr_copy (c->lexpr);
158 ret->ar = c->ar;
159 ret->expr = constraintExpr_copy (c->expr);
160 ret->post = c->post;
795e7f34 161 /*@-assignexpose@*/
28bf4b0b 162 ret->generatingExpr = c->generatingExpr;
795e7f34 163 /*@=assignexpose@*/
9280addf 164
616915dd 165 /*@i33 fix this*/
166 if (c->orig != NULL)
167 ret->orig = constraint_copy (c->orig);
168 else
169 ret->orig = NULL;
90bc41f7 170
171 if (c->or != NULL)
172 ret->or = constraint_copy (c->or);
173 else
174 ret->or = NULL;
4ab867d6 175
176 ret->fcnPre = c->fcnPre;
90bc41f7 177
616915dd 178 return ret;
179}
180
181/*like copy expect it doesn't allocate memory for the constraint*/
182
d46ce6a4 183void constraint_overWrite (constraint c1, constraint c2)
616915dd 184{
d46ce6a4 185 llassert (constraint_isDefined(c1) );
186
187 llassert (c1 != c2);
188
189 DPRINTF((message("OverWriteing constraint %q with %q", constraint_print(c1),
190 constraint_print(c2) ) ));
191
192 constraintExpr_free(c1->lexpr);
193 constraintExpr_free(c1->expr);
194
616915dd 195 c1->lexpr = constraintExpr_copy (c2->lexpr);
196 c1->ar = c2->ar;
197 c1->expr = constraintExpr_copy (c2->expr);
198 c1->post = c2->post;
d46ce6a4 199
200 if (c1->orig != NULL)
201 constraint_free (c1->orig);
202
616915dd 203 if (c2->orig != NULL)
204 c1->orig = constraint_copy (c2->orig);
205 else
206 c1->orig = NULL;
90bc41f7 207
d46ce6a4 208 /*@i33 make sure that the or is freed correctly*/
209 if (c1->or != NULL)
210 constraint_free (c1->or);
211
90bc41f7 212 if (c2->or != NULL)
213 c1->or = constraint_copy (c2->or);
214 else
215 c1->or = NULL;
4ab867d6 216
217 c1->fcnPre = c2->fcnPre;
795e7f34 218
219 /*@-assignexpose@*/
4ab867d6 220 c1->generatingExpr = c2->generatingExpr;
795e7f34 221 /*@=assignexpose@*/
616915dd 222}
223
616915dd 224
225
d46ce6a4 226static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
4ab867d6 227 /*@post:isnull result->or, result->orig, result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
616915dd 228{
229 constraint ret;
230 ret = dmalloc(sizeof (*ret) );
231 ret->lexpr = NULL;
232 ret->expr = NULL;
233 ret->ar = LT;
234 ret->post = FALSE;
235 ret->orig = NULL;
90bc41f7 236 ret->or = NULL;
9280addf 237 ret->generatingExpr = NULL;
4ab867d6 238 ret->fcnPre = NULL;
dc92450f 239 return ret;
616915dd 240}
241
9280addf 242constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
243{
244
245 if (c->generatingExpr == NULL)
246 {
28bf4b0b 247 c->generatingExpr = e;
9280addf 248 DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
249 }
250 else
251 {
252 DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
253 }
254 return c;
255}
256
4ab867d6 257constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
258{
259
260 if (c->orig != constraint_undefined)
261 {
262 c->orig = constraint_addGeneratingExpr(c->orig, e);
263 }
264 else
265 {
266 DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) ) ));
267 }
268 return c;
269}
270
4ab867d6 271constraint constraint_setFcnPre (/*@returned@*/ constraint c )
272{
273
274 if (c->orig != constraint_undefined)
275 {
276 c->orig->fcnPre = TRUE;
277 }
278 else
279 {
280 c->fcnPre = TRUE;
28bf4b0b 281 // DPRINTF(( message("Warning Setting fcnPre directly") ));
4ab867d6 282 }
283 return c;
284}
285
286
287
288
616915dd 289fileloc constraint_getFileloc (constraint c)
290{
c3e695ff 291 if (exprNode_isDefined(c->generatingExpr) )
d46ce6a4 292 return (fileloc_copy (exprNode_getfileloc (c->generatingExpr) ) );
9280addf 293
616915dd 294 return (constraintExpr_getFileloc (c->lexpr) );
295
296
297}
298
9280addf 299static bool checkForMaxSet (constraint c)
300{
301 if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
302 return TRUE;
303
304 return FALSE;
305}
306
307bool constraint_hasMaxSet(constraint c)
308{
dc92450f 309 if (c->orig != NULL)
9280addf 310 {
311 if (checkForMaxSet(c->orig) )
312 return TRUE;
313 }
314
315 return (checkForMaxSet(c) );
316}
317
28bf4b0b 318constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
616915dd 319{
320 constraint ret = constraint_makeNew();
321 // constraintTerm term;
28bf4b0b 322 po = po;
323 ind = ind;
616915dd 324 ret->lexpr = constraintExpr_makeMaxReadExpr(po);
325 ret->ar = GTE;
326 ret->expr = constraintExpr_makeValueExpr (ind);
d46ce6a4 327 ret->post = FALSE;
616915dd 328 return ret;
329}
330
28bf4b0b 331constraint constraint_makeWriteSafeInt ( exprNode po, int ind)
616915dd 332{
333 constraint ret = constraint_makeNew();
334
335
336 ret->lexpr =constraintExpr_makeMaxSetExpr(po);
337 ret->ar = GTE;
c3e695ff 338 ret->expr = constraintExpr_makeIntLiteral (ind);
616915dd 339 /*@i1*/return ret;
340}
341
84c9ffbf 342constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
616915dd 343{
344 constraint ret = constraint_makeNew();
4ab867d6 345 ret->lexpr = constraintExpr_makeSRefMaxset (s);
616915dd 346 ret->ar = EQ;
84c9ffbf 347 ret->expr = constraintExpr_makeIntLiteral ((int)size);
616915dd 348 ret->post = TRUE;
349 /*@i1*/return ret;
350}
351
352constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
353{
354 constraint ret = constraint_makeNew();
355
356
4ab867d6 357 ret->lexpr = constraintExpr_makeSRefMaxset ( s );
616915dd 358 ret->ar = GTE;
c3e695ff 359 ret->expr = constraintExpr_makeIntLiteral (ind);
616915dd 360 ret->post = TRUE;
361 /*@i1*/return ret;
362}
363
364/* drl added 01/12/2000
365
366 makes the constraint: Ensures index <= MaxRead(buffer) */
367
368constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
369{
370 constraint ret = constraint_makeNew();
371
372 ret->lexpr = constraintExpr_makeValueExpr (index);
373 ret->ar = LTE;
374 ret->expr = constraintExpr_makeMaxReadExpr(buffer);
375 ret->post = TRUE;
376 return ret;
377}
378
379constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
380{
381 constraint ret = constraint_makeNew();
382
383
384 ret->lexpr =constraintExpr_makeMaxSetExpr(po);
385 ret->ar = GTE;
386 ret->expr = constraintExpr_makeValueExpr (ind);
387 /*@i1*/return ret;
388}
389
390
28bf4b0b 391constraint constraint_makeReadSafeInt ( exprNode t1, int index)
616915dd 392{
393 constraint ret = constraint_makeNew();
394
28bf4b0b 395 ret->lexpr = constraintExpr_makeMaxReadExpr(t1);
616915dd 396 ret->ar = GTE;
28bf4b0b 397 ret->expr = constraintExpr_makeIntLiteral (index);
d46ce6a4 398 ret->post = FALSE;
616915dd 399 return ret;
400}
401
470b7798 402constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
403{
404 constraint ret = constraint_makeNew();
405
406
4ab867d6 407 ret->lexpr = constraintExpr_makeSRefMaxRead (s );
470b7798 408 ret->ar = GTE;
c3e695ff 409 ret->expr = constraintExpr_makeIntLiteral (ind);
470b7798 410 ret->post = TRUE;
411 /*@i1*/return ret;
412}
413
28bf4b0b 414constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
616915dd 415{
d46ce6a4 416 constraint ret;
616915dd 417
28bf4b0b 418 ret = constraint_makeReadSafeExprNode(t1, t2);
616915dd 419
420 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
421
422 ret->post = TRUE;
423
424 // fileloc_incColumn (ret->lexpr->term->loc);
425 return ret;
426}
427
d46ce6a4 428static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint, arithType ar)
470b7798 429{
430
431 constraint ret;
432
28bf4b0b 433 llassert(constraintExpr_isDefined(c1) && constraintExpr_isDefined(c2) );
470b7798 434 // llassert(sequencePoint);
435
436 ret = constraint_makeNew();
437
438 ret->lexpr = c1;
439 ret->ar = ar;
440 ret->post = TRUE;
441 ret->expr = c2;
442 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
443 return ret;
444}
616915dd 445
28bf4b0b 446static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint, arithType ar)
616915dd 447{
470b7798 448 constraintExpr c1, c2;
449 constraint ret;
616915dd 450 exprNode e;
470b7798 451
28bf4b0b 452 if (! (exprNode_isDefined(e1) && exprNode_isDefined(e2) ) )
616915dd 453 {
454 llcontbug((message("null exprNode, Exprnodes are %s and %s",
455 exprNode_unparse(e1), exprNode_unparse(e2) )
456 ));
457 }
470b7798 458
459 // llassert (sequencePoint);
460
28bf4b0b 461 e = e1;
470b7798 462 c1 = constraintExpr_makeValueExpr (e);
463
28bf4b0b 464 e = e2;
470b7798 465 c2 = constraintExpr_makeValueExpr (e);
466
467 ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
616915dd 468
616915dd 469 return ret;
470}
471
472
473/* make constraint ensures e1 == e2 */
474
475constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
476{
477 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
478}
479
480/*make constraint ensures e1 < e2 */
481constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
482{
470b7798 483 constraintExpr t1, t2;
484
485 t1 = constraintExpr_makeValueExpr (e1);
486 t2 = constraintExpr_makeValueExpr (e2);
487
488 /*change this to e1 <= (e2 -1) */
489
490 t2 = constraintExpr_makeDecConstraintExpr (t2);
491
492 return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
616915dd 493}
494
495constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
496{
497 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
498}
499
500constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
501{
470b7798 502 constraintExpr t1, t2;
503
504 t1 = constraintExpr_makeValueExpr (e1);
505 t2 = constraintExpr_makeValueExpr (e2);
506
507
508 /* change this to e1 >= (e2 + 1) */
509 t2 = constraintExpr_makeIncConstraintExpr (t2);
510
511
512 return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
616915dd 513}
514
515constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
516{
517 return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
518}
519
520
521exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
522{
d46ce6a4 523 constraintList_free(dst->ensuresConstraints);
524 constraintList_free(dst->requiresConstraints);
525 constraintList_free(dst->trueEnsuresConstraints);
526 constraintList_free(dst->falseEnsuresConstraints);
527
616915dd 528 dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
529 dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
530 dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
531 dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
532 return dst;
533}
534
2934b455 535/* Makes the constraint e = e + f */
536constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
537{
538 constraintExpr x1, x2, y;
539 constraint ret;
540
541 ret = constraint_makeNew();
542
543 x1 = constraintExpr_makeValueExpr (e);
544 x2 = constraintExpr_copy(x1);
545 y = constraintExpr_makeValueExpr (f);
546
547 ret->lexpr = x1;
548 ret->ar = EQ;
549 ret->post = TRUE;
550 ret->expr = constraintExpr_makeAddExpr (x2, y);
551
552 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
553
554 return ret;
555}
556
557
558/* Makes the constraint e = e - f */
559constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
560{
561 constraintExpr x1, x2, y;
562 constraint ret;
563
564 ret = constraint_makeNew();
565
566 x1 = constraintExpr_makeValueExpr (e);
567 x2 = constraintExpr_copy(x1);
568 y = constraintExpr_makeValueExpr (f);
569
570 ret->lexpr = x1;
571 ret->ar = EQ;
572 ret->post = TRUE;
573 ret->expr = constraintExpr_makeSubtractExpr (x2, y);
574
575 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
576
577 return ret;
578}
579
616915dd 580constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
581{
582 constraint ret = constraint_makeNew();
583 //constraintTerm term;
584
28bf4b0b 585 // e = exprNode_fakeCopy(e);
616915dd 586 ret->lexpr = constraintExpr_makeValueExpr (e);
587 ret->ar = EQ;
588 ret->post = TRUE;
589 ret->expr = constraintExpr_makeValueExpr (e);
590 ret->expr = constraintExpr_makeDecConstraintExpr (ret->expr);
591
592 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
593// fileloc_incColumn ( ret->lexpr->term->loc);
594// fileloc_incColumn ( ret->lexpr->term->loc);
595 return ret;
596}
597constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
598{
599 constraint ret = constraint_makeNew();
600 //constraintTerm term;
601
28bf4b0b 602 // e = exprNode_fakeCopy(e);
616915dd 603 ret->lexpr = constraintExpr_makeValueExpr (e);
604 ret->ar = EQ;
605 ret->post = TRUE;
606 ret->expr = constraintExpr_makeValueExpr (e);
607 ret->expr = constraintExpr_makeIncConstraintExpr (ret->expr);
608
609 ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
610// fileloc_incColumn ( ret->lexpr->term->loc);
611// fileloc_incColumn ( ret->lexpr->term->loc);
612 return ret;
613}
614
615
920a3797 616void constraint_free (/*@only@*/ constraint c)
d46ce6a4 617{
618 llassert(constraint_isDefined (c) );
619
620
621 if (constraint_isDefined(c->orig) )
622 constraint_free (c->orig);
623 if ( constraint_isDefined(c->or) )
624 constraint_free (c->or);
625
bb25bea6 626
d46ce6a4 627 constraintExpr_free(c->lexpr);
628 constraintExpr_free(c->expr);
bb25bea6 629
630 c->orig = NULL;
631 c->or = NULL;
632 c->lexpr = NULL;
633 c->expr = NULL;
634
d46ce6a4 635 free (c);
636
637}
638
616915dd 639
640// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
641// {
642// constraint ret = constraint_makeNew();
643// //constraintTerm term;
644
645// e = exprNode_fakeCopy(e);
646// ret->lexpr = constraintExpr_makeMaxReadExpr(e);
647// ret->ar = EQ;
648// ret->post = TRUE;
649// ret->expr = constraintExpr_makeIncConstraintExpr (e);
650// ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
651// return ret;
652// }
653
654
dc92450f 655cstring arithType_print (arithType ar) /*@*/
616915dd 656{
657 cstring st = cstring_undefined;
658 switch (ar)
659 {
660 case LT:
661 st = cstring_makeLiteral (" < ");
662 break;
663 case LTE:
664 st = cstring_makeLiteral (" <= ");
665 break;
666 case GT:
667 st = cstring_makeLiteral (" > ");
668 break;
669 case GTE:
670 st = cstring_makeLiteral (" >= ");
671 break;
672 case EQ:
673 st = cstring_makeLiteral (" == ");
674 break;
675 case NONNEGATIVE:
676 st = cstring_makeLiteral (" NONNEGATIVE ");
677 break;
678 case POSITIVE:
679 st = cstring_makeLiteral (" POSITIVE ");
680 break;
681 default:
682 llassert(FALSE);
683 break;
684 }
685 return st;
686}
687
8f299805 688void constraint_printErrorPostCondition (constraint c, fileloc loc)
689{
690 cstring string;
691 fileloc errorLoc, temp;
692
693 string = constraint_printDetailedPostCondition (c);
694
695 errorLoc = loc;
696
697 loc = NULL;
698
699 temp = constraint_getFileloc(c);
700
701 if (fileloc_isDefined(temp) )
702 {
703 errorLoc = temp;
704 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
705 fileloc_free(temp);
706 }
707 else
708 {
709 voptgenerror ( FLG_CHECKPOST, string, errorLoc);
710 }
711}
712
713
714
715
616915dd 716void constraint_printError (constraint c, fileloc loc)
717{
718 cstring string;
4ab867d6 719 fileloc errorLoc, temp;
9280addf 720
616915dd 721 string = constraint_printDetailed (c);
9280addf 722
723 errorLoc = loc;
724
4ab867d6 725 loc = NULL;
726
727 temp = constraint_getFileloc(c);
728
729 if (fileloc_isDefined(temp) )
616915dd 730 {
4ab867d6 731 errorLoc = temp;
732
733 if (c->post)
734 {
735 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
736 }
737 else
738 {
739 voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
740 }
741 fileloc_free(temp);
28bf4b0b 742 errorLoc = NULL;
616915dd 743 }
744 else
745 {
4ab867d6 746 if (c->post)
747 {
748 voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
749 }
750 else
751 {
752 voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
753 }
28bf4b0b 754 errorLoc = NULL;
616915dd 755 }
616915dd 756}
757
4ab867d6 758
28bf4b0b 759static cstring constraint_printDeep (constraint c)
616915dd 760{
28bf4b0b 761 cstring genExpr;
616915dd 762 cstring st = cstring_undefined;
763
4ab867d6 764 st = constraint_print(c);
765
28bf4b0b 766
4ab867d6 767 if (c->orig != constraint_undefined)
768 {
28bf4b0b 769 genExpr = exprNode_unparse(c->orig->generatingExpr);
4ab867d6 770 if (!c->post)
771 {
772 if (c->orig->fcnPre)
28bf4b0b 773 st = cstring_concatFree(st, (message(" derived from %s precondition: %q", genExpr, constraint_printDeep(c->orig) )
4ab867d6 774 ) );
775 else
776 st = cstring_concatFree(st,(message(" needed to satisfy %q",
777 constraint_printDeep(c->orig) )
778 ) );
779
780 }
781 else
782 {
783 st = cstring_concatFree(st,(message("derived from: %q",
784 constraint_printDeep(c->orig) )
785 ) );
786 }
787 }
788
789 return st;
790
791}
792
2934b455 793
794static /*@only@*/ cstring constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
8f299805 795{
796 cstring st = cstring_undefined;
28bf4b0b 797 cstring genExpr;
798
8f299805 799 st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
28bf4b0b 800
801 genExpr = exprNode_unparse (c->generatingExpr);
802
8f299805 803 if (context_getFlag (FLG_CONSTRAINTLOCATION) )
804 {
805 cstring temp;
806 // llassert (c->generatingExpr);
807 temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
28bf4b0b 808 genExpr );
8f299805 809 st = cstring_concatFree (st, temp);
810
811 if (constraint_hasMaxSet(c) )
812 {
813 temp = message ("Has MaxSet\n");
814 st = cstring_concatFree (st, temp);
815 }
816 }
817 return st;
818}
819
4ab867d6 820cstring constraint_printDetailed (constraint c)
821{
822 cstring st = cstring_undefined;
28bf4b0b 823 cstring genExpr;
824
616915dd 825 if (!c->post)
826 {
4ab867d6 827 st = message ("Unresolved constraint:\nLclint is unable to resolve %q", constraint_printDeep (c) );
616915dd 828 }
829 else
830 {
4ab867d6 831 st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
616915dd 832 }
9280addf 833
28bf4b0b 834 genExpr = exprNode_unparse (c->generatingExpr);
835
9280addf 836 if (context_getFlag (FLG_CONSTRAINTLOCATION) )
837 {
838 cstring temp;
839 // llassert (c->generatingExpr);
d46ce6a4 840 temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
28bf4b0b 841 genExpr );
d46ce6a4 842 st = cstring_concatFree (st, temp);
9280addf 843
844 if (constraint_hasMaxSet(c) )
845 {
8f299805 846 temp = message ("Has MaxSet\n");
d46ce6a4 847 st = cstring_concatFree (st, temp);
9280addf 848 }
849 }
616915dd 850 return st;
851}
852
d46ce6a4 853/*@only@*/ cstring constraint_print (constraint c) /*@*/
616915dd 854{
855 cstring st = cstring_undefined;
856 cstring type = cstring_undefined;
dc92450f 857 llassert (c !=NULL);
616915dd 858 if (c->post)
859 {
860 type = cstring_makeLiteral ("Ensures: ");
861 }
862 else
863 {
864 type = cstring_makeLiteral ("Requires: ");
865 }
d46ce6a4 866 st = message ("%q: %q %q %q",
616915dd 867 type,
868 constraintExpr_print (c->lexpr),
869 arithType_print(c->ar),
870 constraintExpr_print(c->expr)
871 );
872 return st;
873}
874
90bc41f7 875cstring constraint_printOr (constraint c) /*@*/
876{
877 cstring ret;
878 constraint temp;
879
880 ret = cstring_undefined;
881 temp = c;
882
d46ce6a4 883 ret = cstring_concatFree (ret, constraint_print(temp) );
90bc41f7 884
885 temp = temp->or;
886
c3e695ff 887 while ( constraint_isDefined(temp) )
90bc41f7 888 {
d46ce6a4 889 ret = cstring_concatFree (ret, cstring_makeLiteral (" OR ") );
890 ret = cstring_concatFree (ret, constraint_print(temp) );
90bc41f7 891 temp = temp->or;
892 }
893
894 return ret;
895
896}
897
dc92450f 898/*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
616915dd 899 exprNodeList arglist)
900{
901 precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
902 arglist);
903 precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
904 arglist);
905
906 return precondition;
907}
908
909
28bf4b0b 910constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
616915dd 911{
912 postcondition = constraint_copy (postcondition);
913 postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
914 postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
915
916 return postcondition;
917}
918
d46ce6a4 919/*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
616915dd 920 exprNodeList arglist)
921{
922
923 precondition = constraint_copy (precondition);
924 precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
925 precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
926
4ab867d6 927 precondition->fcnPre = FALSE;
616915dd 928 return precondition;
929}
930
931// bool constraint_hasTerm (constraint c, constraintTerm term)
932// {
933// DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
934
935// if (constraintExpr_includesTerm (c->lexpr, term) )
936// return TRUE;
937
938// if (constraintExpr_includesTerm (c->expr, term) )
939// return TRUE;
940
941// return FALSE;
942// }
943
d46ce6a4 944constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
616915dd 945{
4ab867d6 946
947 DPRINTF( (message("Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
948
d46ce6a4 949 if (c->orig == constraint_undefined)
950 c->orig = constraint_copy (c);
4ab867d6 951
952 else if (c->orig->fcnPre)
953 {
954 constraint temp;
955
956 temp = c->orig;
957
958 /* avoid infinite loop */
959 c->orig = NULL;
960 c->orig = constraint_copy (c);
961 if (c->orig->orig == NULL)
920a3797 962 {
963 c->orig->orig = temp;
964 temp = NULL;
965 }
4ab867d6 966 else
920a3797 967 {
968 llcontbug((message("Expected c->orig->orig to be null" ) ));
969 constraint_free(c->orig->orig);
970 c->orig->orig = temp;
971 temp = NULL;
972 }
4ab867d6 973 }
974 else
975 {
976 DPRINTF( (message("Not changing constraint") ));
977 }
d46ce6a4 978
4ab867d6 979 DPRINTF( (message("After Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
980
616915dd 981 return c;
982}
983/*@=fcnuse*/
984/*@=assignexpose*/
985/*@=czechfcns@*/
84c9ffbf 986
2934b455 987
84c9ffbf 988constraint constraint_togglePost (/*@returned@*/ constraint c)
989{
990 c->post = !c->post;
991 return c;
992}
2934b455 993
994constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
995{
996 if (c->orig != NULL)
997 c->orig = constraint_togglePost(c->orig);
998 return c;
999}
1000
1001bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c)
1002{
1003 if (c->orig == NULL)
1004 return FALSE;
1005 else
1006 return TRUE;
1007}
920a3797 1008
1009
1010constraint constraint_undump (FILE *f)
1011{
1012 constraint c;
1013 bool fcnPre;
1014 bool post;
1015 arithType ar;
1016
1017 constraintExpr lexpr;
1018 constraintExpr expr;
28bf4b0b 1019
920a3797 1020
1021 char * s;
1022
1023 char *os;
1024
1025 s = mstring_create (MAX_DUMP_LINE_LENGTH);
1026
1027 os = s;
1028
1029 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1030
1031 /*@i33*/ /*this should probably be wrappered...*/
1032
28bf4b0b 1033 fcnPre = (bool) reader_getInt (&s);
920a3797 1034 advanceField(&s);
28bf4b0b 1035 post = (bool) reader_getInt (&s);
920a3797 1036 advanceField(&s);
28bf4b0b 1037 ar = (arithType) reader_getInt (&s);
920a3797 1038
1039 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1040
28bf4b0b 1041 reader_checkChar (&s, 'l');
920a3797 1042
1043 lexpr = constraintExpr_undump (f);
1044
1045 s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
1046
28bf4b0b 1047 reader_checkChar (&s, 'r');
920a3797 1048 expr = constraintExpr_undump (f);
1049
1050 c = constraint_makeNew();
1051
1052 c->fcnPre = fcnPre;
1053 c->post = post;
1054 c->ar = ar;
1055
1056 c->lexpr = lexpr;
1057 c->expr = expr;
1058
1059 free(os);
1060 return c;
1061}
1062
1063
1064void constraint_dump (/*@observer@*/ constraint c, FILE *f)
1065{
1066 bool fcnPre;
1067 bool post;
1068 arithType ar;
1069
1070 constraintExpr lexpr;
1071 constraintExpr expr;
28bf4b0b 1072
920a3797 1073
1074 fcnPre = c->fcnPre;
1075 post = c->post;
1076 ar = c->ar;
1077 lexpr = c->lexpr;
1078 expr = c->expr;
1079
1080 fprintf(f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
1081 fprintf(f,"l\n");
1082 constraintExpr_dump (lexpr, f);
1083 fprintf(f,"r\n");
1084 constraintExpr_dump (expr, f);
1085}
1086
1087
git-cvsimport mirror of splint
This page took 0.260507 seconds and 5 git commands to generate.