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