3 ** constraintGeneration.c
8 # include <ctype.h> /* for isdigit */
9 # include "lclintMacros.nf"
12 # include "cgrammar_tokens.h"
14 # include "exprChecks.h"
15 # include "exprNodeSList.h"
17 //# include "exprDataQuite.i"
19 /*@access exprNode @*/
22 static bool exprNode_handleError(/*@dependent@*/ exprNode p_e);
24 //static cstring exprNode_findConstraints ( exprNode p_e);
25 static bool exprNode_isMultiStatement(/*@dependent@*/ exprNode p_e);
26 static void exprNode_multiStatement (/*@dependent@*/ exprNode p_e);
28 //static void exprNode_constraintPropagateUp (exprNode p_e);
30 static constraintList exprNode_traversTrueEnsuresConstraints (/*@dependent@*/ exprNode p_e);
31 static constraintList exprNode_traversFalseEnsuresConstraints (/*@dependent@*/ exprNode p_e);
33 static exprNode makeDataTypeConstraints (/*@returned@*/ exprNode p_e);
35 static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/;
37 static constraintList checkCall (/*@dependent@*/ exprNode p_fcn, exprNodeList p_arglist);
39 //constraintList constraintList_makeFixedArrayConstraints (sRefSet s);
41 //bool exprNode_testd()
43 /* if ( ( (exprNode_isError ) ) )
52 static bool exprNode_isUnhandled (/*@dependent@*/ /*@obsever@*/ exprNode e)
54 llassert( exprNode_isDefined(e) );
82 DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
94 bool exprNode_handleError( exprNode e)
96 if (exprNode_isError (e) || exprNode_isUnhandled(e) )
98 static /*@only@*/ cstring error = cstring_undefined;
100 if (!cstring_isDefined (error))
102 error = cstring_makeLiteral ("<error>");
105 /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/
110 bool /*@alt void@*/ exprNode_generateConstraints (/*@dependent@*/ exprNode e)
112 if (exprNode_isError (e) )
115 if (exprNode_isUnhandled (e) )
117 DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) );
122 // e = makeDataTypeConstraints (e);
124 DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e),
125 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
127 if (exprNode_isMultiStatement ( e) )
129 exprNode_multiStatement(e);
135 loc = exprNode_getNextSequencePoint(e);
136 exprNode_exprTraverse(e, FALSE, FALSE, loc);
145 c = constraintList_makeFixedArrayConstraints (e->uses);
146 e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, c);
148 // e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints);
150 constraintList_free(c);
153 DPRINTF ( (message ("e->requiresConstraints %s", constraintList_printDetailed (e->requiresConstraints) ) ) );
158 /* handles multiple statements */
160 bool exprNode_isMultiStatement(exprNode e)
162 if (exprNode_handleError (e) != NULL)
185 static void exprNode_stmt ( /*@dependent@*/ exprNode e)
191 if (exprNode_isError(e) )
195 /*e->requiresConstraints = constraintList_makeNew();
196 e->ensuresConstraints = constraintList_makeNew(); */
197 // e = makeDataTypeConstraints(e);
200 DPRINTF(( "STMT:") );
201 s = exprNode_unparse(e);
202 // DPRINTF ( ( message("STMT: %s ") ) );
204 if (e->kind == XPR_INIT)
206 constraintList tempList;
208 DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
209 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
210 exprNode_exprTraverse (e, FALSE, FALSE, loc);
213 tempList = e->requiresConstraints;
214 e->requiresConstraints = exprNode_traversRequiresConstraints(e);
215 constraintList_free(tempList);
217 tempList = e->ensuresConstraints;
218 e->ensuresConstraints = exprNode_traversEnsuresConstraints(e);
219 constraintList_free(tempList);
223 if (e->kind != XPR_STMT)
226 DPRINTF (("Not Stmt") );
227 DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
228 if (exprNode_isMultiStatement (e) )
230 return exprNode_multiStatement (e );
232 DPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) );
238 DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
240 snode = exprData_getUopNode (e->edata);
242 /* could be stmt involving multiple statements:
243 i.e. if, while for ect.
246 if (exprNode_isMultiStatement (snode))
248 exprNode_multiStatement (snode);
249 (void) exprNode_copyConstraints (e, snode);
253 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
255 exprNode_exprTraverse (snode, FALSE, FALSE, loc);
259 constraintList_free (e->requiresConstraints);
260 e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
261 // printf ("For: %s \n", exprNode_unparse (e) );
262 // printf ("%s\n", constraintList_print(e->requiresConstraints) );
264 constraintList_free (e->ensuresConstraints);
265 e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode);
266 // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
267 // llassert(notError);
269 DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
270 constraintList_print(e->requiresConstraints),
271 constraintList_print(e->ensuresConstraints) ) ) );
278 static void exprNode_stmtList (/*@dependent@*/ exprNode e)
280 exprNode stmt1, stmt2;
281 if (exprNode_isError (e) )
287 e->requiresConstraints = constraintList_makeNew();
288 e->ensuresConstraints = constraintList_makeNew();
290 // e = makeDataTypeConstraints(e);
292 /*Handle case of stmtList with only one statement:
293 The parse tree stores this as stmt instead of stmtList*/
294 if (e->kind != XPR_STMTLIST)
299 llassert (e->kind == XPR_STMTLIST);
300 DPRINTF(( "STMTLIST:") );
301 DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
302 stmt1 = exprData_getPairA (e->edata);
303 stmt2 = exprData_getPairB (e->edata);
306 DPRINTF((" stmtlist ") );
307 DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
309 exprNode_stmt (stmt1);
310 DPRINTF(("\nstmt after stmtList call " ));
312 exprNode_stmt (stmt2);
313 exprNode_mergeResolve (e, stmt1, stmt2 );
315 DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
316 constraintList_print(e->requiresConstraints),
317 constraintList_print(e->ensuresConstraints) ) ) );
321 static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
325 DPRINTF ((message ("doIf: %s ", exprNode_unparse(e) ) ) );
327 llassert(exprNode_isDefined(test) );
328 llassert (exprNode_isDefined (e) );
329 llassert (exprNode_isDefined (body) );
332 DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
334 DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
336 DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) ));
338 DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) ));
342 DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) ));
344 DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints) ) ));
346 DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->trueEnsuresConstraints) ) ));
348 DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->falseEnsuresConstraints) ) ));
352 temp = test->trueEnsuresConstraints;
353 test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
354 constraintList_free(temp);
356 temp = test->ensuresConstraints;
357 test->ensuresConstraints = exprNode_traversEnsuresConstraints (test);
358 constraintList_free(temp);
360 temp = test->requiresConstraints;
361 test->requiresConstraints = exprNode_traversRequiresConstraints (test);
362 constraintList_free(temp);
365 test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints);
367 DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints) ) ) );
369 DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints) ) ) );
371 constraintList_free(e->requiresConstraints);
372 e->requiresConstraints = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints);
374 e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints,
375 test->ensuresConstraints);
376 temp = e->requiresConstraints;
377 e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints);
378 constraintList_free(temp);
381 //drl possible problem : warning bad
382 constraintList_free(e->ensuresConstraints);
383 e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
385 if (exprNode_mayEscape (body) )
387 DPRINTF (( message("doIf: the if statement body %s returns or exits", exprNode_unparse(body) ) ));
388 e->ensuresConstraints = constraintList_mergeEnsuresFreeFirst (e->ensuresConstraints,
389 test->falseEnsuresConstraints);
392 DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints) ) ) );
398 Also used for condition i.e. ?: operation
401 This function assumes that p, trueBranch, falseBranch have have all been traversed
402 for constraints i.e. we assume that exprNode_traversEnsuresConstraints,
403 exprNode_traversRequiresConstraints, exprNode_traversTrueEnsuresConstraints,
404 exprNode_traversFalseEnsuresConstraints have all been run
408 static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch)
411 constraintList c1, cons, t, t2, f, f2;
413 DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e) ) ) );
415 // do requires clauses
416 c1 = constraintList_copy (p->ensuresConstraints);
418 t = constraintList_reflectChanges(trueBranch->requiresConstraints, p->trueEnsuresConstraints);
419 t = constraintList_reflectChangesFreePre (t, p->ensuresConstraints);
421 cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints);
422 cons = constraintList_reflectChangesFreePre (cons, c1);
424 constraintList_free(e->requiresConstraints);
425 e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons);
426 e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints);
428 // do ensures clauses
429 // find the the ensures lists for each subbranch
430 t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
432 t = constraintList_mergeEnsures (p->ensuresConstraints, t);
433 constraintList_free(t2);
435 f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
437 f = constraintList_mergeEnsures (p->ensuresConstraints, f);
438 constraintList_free(f2);
440 // find ensures for whole if/else statement
442 constraintList_free(e->ensuresConstraints);
444 e->ensuresConstraints = constraintList_logicalOr (t, f);
446 constraintList_free(t);
447 constraintList_free(f);
448 constraintList_free(cons);
449 constraintList_free(c1);
451 DPRINTF ((message ("doIfElse: if requires %q ", constraintList_print(e->requiresConstraints) ) ) );
452 DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_print(e->ensuresConstraints) ) ) );
457 static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
459 DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e) ) ) );
460 return doIf (e, test, body);
463 /*@only@*/ constraintList constraintList_makeFixedArrayConstraints (/*@observer@*/ sRefSet s)
467 ret = constraintList_makeNew();
469 sRefSet_elements (s, el)
472 if (sRef_isFixedArray(el) )
475 DPRINTF( (message("%s is a fixed array",
476 sRef_unparse(el)) ) );
477 //if (el->kind == SK_DERIVED)
478 // break; //hack until I find the real problem
479 size = sRef_getArraySize(el);
480 DPRINTF( (message("%s is a fixed array with size %d",
481 sRef_unparse(el), (int)size) ) );
482 con = constraint_makeSRefSetBufferSize (el, (size - 1));
483 //con = constraint_makeSRefWriteSafeInt (el, (size - 1));
484 ret = constraintList_add(ret, con);
488 DPRINTF( (message("%s is not a fixed array",
489 sRef_unparse(el)) ) );
492 if (sRef_isExternallyVisible (el) )
494 /*DPRINTF( (message("%s is externally visible",
495 sRef_unparse(el) ) ));
496 con = constraint_makeSRefWriteSafeInt(el, 0);
497 ret = constraintList_add(ret, con);
499 con = constraint_makeSRefReadSafeInt(el, 0);
501 ret = constraintList_add(ret, con);*/
507 DPRINTF(( message("constraintList_makeFixedArrayConstraints returning %s",
508 constraintList_print(ret) ) ));
512 exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e)
515 DPRINTF(("makeDataTypeConstraints"));
517 c = constraintList_makeFixedArrayConstraints (e->uses);
519 e->ensuresConstraints = constraintList_addListFree (e->ensuresConstraints, c);
524 static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, /*@dependent@*/ exprNode forBody)
526 exprNode init, test, inc;
527 //merge the constraints: modle as if statement
532 init = exprData_getTripleInit (forPred->edata);
533 test = exprData_getTripleTest (forPred->edata);
534 inc = exprData_getTripleInc (forPred->edata);
536 if ( ( (exprNode_isError (test) /*|| (exprNode_isError(init) )*/ ) || (exprNode_isError (inc) ) ) )
538 DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) );
542 exprNode_forLoopHeuristics(e, forPred, forBody);
544 constraintList_free(e->requiresConstraints);
545 e->requiresConstraints = constraintList_reflectChanges(forBody->requiresConstraints, test->ensuresConstraints);
546 e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints);
547 e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints);
549 if (!forBody->canBreak)
551 e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints) );
552 e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy( test->falseEnsuresConstraints));
553 // forPred->ensuresConstraints = constraintList_undefined;
554 // test->falseEnsuresConstraints = constraintList_undefined;
558 DPRINTF(("Can break") );
563 static exprNode doSwitch (/*@returned@*/ exprNode e)
570 DPRINTF (( message ("doSwitch for: switch (%s) %s",
571 exprNode_unparse (exprData_getPairA (data)),
572 exprNode_unparse (exprData_getPairB (data))) ));
574 body = exprData_getPairB (data);
576 exprNode_generateConstraints(body);
578 constraintList_free(e->requiresConstraints);
579 constraintList_free(e->ensuresConstraints);
581 e->requiresConstraints = NULL;
582 e->ensuresConstraints = NULL;
584 e->requiresConstraints = constraintList_copy ( body->requiresConstraints );
585 e->ensuresConstraints = constraintList_copy ( body->ensuresConstraints );
591 void exprNode_multiStatement (/*@dependent@*/ exprNode e)
597 exprNode p, trueBranch, falseBranch;
598 exprNode forPred, forBody;
603 // constraintList t, f;
604 /*e->requiresConstraints = constraintList_makeNew();
605 e->ensuresConstraints = constraintList_makeNew();
606 e->trueEnsuresConstraints = constraintList_makeNew();
607 e->falseEnsuresConstraints = constraintList_makeNew();
609 // e = makeDataTypeConstraints(e);
611 DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
612 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
614 if (exprNode_handleError (e))
627 // ret = message ("%s %s",
628 forPred = exprData_getPairA (data);
629 forBody = exprData_getPairB (data);
631 //first generate the constraints
632 exprNode_generateConstraints (forPred);
633 exprNode_generateConstraints (forBody);
636 doFor (e, forPred, forBody);
641 // ret = message ("for (%s; %s; %s)",
642 exprNode_generateConstraints (exprData_getTripleInit (data) );
643 test = exprData_getTripleTest (data);
644 exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
645 exprNode_generateConstraints (exprData_getTripleInc (data) );
647 if (!exprNode_isError(test) )
649 constraintList temp2;
650 temp2 = test->trueEnsuresConstraints;
651 test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
652 constraintList_free(temp2);
655 exprNode_generateConstraints (exprData_getTripleInc (data));
659 e1 = exprData_getPairA (data);
660 e2 = exprData_getPairB (data);
662 exprNode_exprTraverse (e1,
663 FALSE, FALSE, exprNode_loc(e1));
665 exprNode_generateConstraints (e2);
667 e = doWhile (e, e1, e2);
673 DPRINTF ((exprNode_unparse(e) ) );
674 // ret = message ("if (%s) %s",
675 e1 = exprData_getPairA (data);
676 e2 = exprData_getPairB (data);
678 exprNode_exprTraverse (e1,
679 FALSE, FALSE, exprNode_loc(e1));
681 exprNode_generateConstraints (e2);
682 e = doIf (e, e1, e2);
685 // e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
690 DPRINTF(("Starting IFELSE"));
691 // ret = message ("if (%s) %s else %s",
692 p = exprData_getTriplePred (data);
693 trueBranch = exprData_getTripleTrue (data);
694 falseBranch = exprData_getTripleFalse (data);
696 exprNode_exprTraverse (p,
697 FALSE, FALSE, exprNode_loc(p));
698 exprNode_generateConstraints (trueBranch);
699 exprNode_generateConstraints (falseBranch);
701 temp = p->ensuresConstraints;
702 p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
703 constraintList_free(temp);
705 temp = p->requiresConstraints;
706 p->requiresConstraints = exprNode_traversRequiresConstraints (p);
707 constraintList_free(temp);
709 temp = p->trueEnsuresConstraints;
710 p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p);
711 constraintList_free(temp);
713 temp = p->falseEnsuresConstraints;
714 p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p);
715 constraintList_free(temp);
717 e = doIfElse (e, p, trueBranch, falseBranch);
718 DPRINTF( ("Done IFELSE") );
723 e2 = (exprData_getPairB (data));
724 e1 = (exprData_getPairA (data));
726 DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1) ) ));
727 exprNode_generateConstraints (e2);
728 exprNode_generateConstraints (e1);
729 e = exprNode_copyConstraints (e, e2);
730 DPRINTF ((message ("e = %s ", constraintList_print(e->requiresConstraints) ) ));
735 // ret = message ("{ %s }",
736 exprNode_generateConstraints (exprData_getSingle (data));
738 constraintList_free(e->requiresConstraints);
739 e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
741 constraintList_free(e->ensuresConstraints);
742 e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
743 // e->constraints = (exprData_getSingle (data))->constraints;
751 exprNode_stmtList (e);
761 static bool lltok_isBoolean_Op (lltok tok)
763 /*this should really be a switch statement but
764 I don't want to violate the abstraction
765 maybe this should go in lltok.c */
767 if (lltok_isEq_Op (tok) )
771 if (lltok_isAnd_Op (tok) )
777 if (lltok_isOr_Op (tok) )
782 if (lltok_isGt_Op (tok) )
786 if (lltok_isLt_Op (tok) )
791 if (lltok_isLe_Op (tok) )
796 if (lltok_isGe_Op (tok) )
806 static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint)
812 constraintList tempList, temp;
815 tok = exprData_getOpTok (data);
818 t1 = exprData_getOpA (data);
819 t2 = exprData_getOpB (data);
822 tempList = constraintList_undefined;
824 /* arithmetic tests */
826 if (lltok_isEq_Op (tok) )
828 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
829 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
833 if (lltok_isLt_Op (tok) )
835 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
836 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
837 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
838 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
842 if (lltok_isGe_Op (tok) )
845 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
846 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
848 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
849 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
854 if (lltok_isGt_Op (tok) )
856 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
857 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
858 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
859 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
862 if (lltok_isLe_Op (tok) )
864 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
865 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
867 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
868 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
873 /*Logical operations */
876 if (lltok_isAnd_Op (tok) )
880 tempList = constraintList_copy (t1->trueEnsuresConstraints);
881 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
882 e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
884 //false ensures: fens t1 or tens t1 and fens t2
885 tempList = constraintList_copy (t1->trueEnsuresConstraints);
886 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
888 tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
889 constraintList_free (temp);
891 /* evans - was constraintList_addList - memory leak detected by lclint */
892 e->falseEnsuresConstraints =constraintList_addListFree (e->falseEnsuresConstraints, tempList);
894 else if (lltok_isOr_Op (tok) )
897 tempList = constraintList_copy (t1->falseEnsuresConstraints);
898 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
899 e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList);
901 //true ensures: tens t1 or fens t1 and tens t2
902 tempList = constraintList_copy (t1->falseEnsuresConstraints);
903 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
906 tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
907 constraintList_free(temp);
909 e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
910 tempList = constraintList_undefined;
914 DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok) ) ));
918 void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
920 exprNode t1, t2, fcn;
922 bool handledExprNode;
928 if (exprNode_isError(e) )
933 DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
934 fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
936 /*e->requiresConstraints = constraintList_makeNew();
937 e->ensuresConstraints = constraintList_makeNew();
938 e->trueEnsuresConstraints = constraintList_makeNew();;
939 e->falseEnsuresConstraints = constraintList_makeNew();;
941 if (exprNode_isUnhandled (e) )
945 // e = makeDataTypeConstraints (e);
947 handledExprNode = TRUE;
954 t1 = exprData_getSingle (data);
955 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
956 e = exprNode_copyConstraints (e, t1);
963 t1 = (exprData_getPairA (data) );
964 t2 = (exprData_getPairB (data) );
965 cons = constraint_makeWriteSafeExprNode (t1, t2);
969 t1 = (exprData_getPairA (data) );
970 t2 = (exprData_getPairB (data) );
971 cons = constraint_makeReadSafeExprNode (t1, t2 );
974 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
975 cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
976 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
978 cons = constraint_makeEnsureLteMaxRead (t2, t1);
979 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
981 // cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
982 // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
984 exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
985 exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
987 /*@i325 Should check which is array/index. */
991 exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
992 // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
1002 t = exprData_getInitId (data);
1003 ue = usymtab_lookup (idDecl_observeId (t));
1004 lhs = exprNode_createId (ue);
1006 t2 = exprData_getInitNode (data);
1008 /* DPRINTF(( (message("initialization: %s = %s",
1009 exprNode_unparse(lhs),
1010 exprNode_unparse(t2)
1014 //exprNode_exprTraverse (t1, TRUE, FALSE, sequencePoint );
1016 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1018 /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
1019 if ( (!exprNode_isError (e)) && (!exprNode_isError(t2)) )
1021 cons = constraint_makeEnsureEqual (e, t2, sequencePoint);
1022 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1028 t1 = exprData_getOpA (data);
1029 t2 = exprData_getOpB (data);
1030 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1031 //lltok_unparse (exprData_getOpTok (data));
1033 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1035 /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
1036 if ( (!exprNode_isError (t1)) && (!exprNode_isError(t2)) )
1038 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
1039 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1043 t1 = exprData_getOpA (data);
1044 t2 = exprData_getOpB (data);
1045 tok = exprData_getOpTok (data);
1048 if (tok.tok == ADD_ASSIGN)
1050 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1051 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1053 cons = constraint_makeAddAssign (t1, t2, sequencePoint );
1054 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1056 else if (tok.tok == SUB_ASSIGN)
1058 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
1059 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
1061 cons = constraint_makeSubtractAssign (t1, t2, sequencePoint );
1062 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1066 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
1067 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1070 if (lltok_isBoolean_Op (tok) )
1071 exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
1073 // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
1076 //drl possible problem : warning make sure the case can be ignored..
1081 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
1082 // e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
1086 fcn = exprData_getFcn(data);
1088 exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint );
1089 DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data) ) ) ) );
1091 fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
1092 checkCall (fcn, exprData_getArgs (data) ) );
1094 fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
1095 exprNode_getPostConditions(fcn, exprData_getArgs (data),e ) );
1097 t1 = exprNode_createNew (exprNode_getType (e) );
1099 checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
1102 exprNode_mergeResolve (e, t1, fcn);
1106 // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) );
1111 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
1114 case XPR_NULLRETURN:
1120 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
1124 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
1127 case XPR_STRINGLITERAL:
1136 t1 = exprData_getUopNode(data);
1137 tok = (exprData_getUopTok (data));
1138 //lltok_unparse (exprData_getUopTok (data));
1139 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
1140 /*handle * pointer access */
1141 if (lltok_isInc_Op (tok) )
1143 DPRINTF(("doing ++(var)"));
1144 t1 = exprData_getUopNode (data);
1145 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1146 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1148 else if (lltok_isDec_Op (tok) )
1150 DPRINTF(("doing --(var)"));
1151 t1 = exprData_getUopNode (data);
1152 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1153 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1155 else if (lltok_isMult( tok ) )
1159 cons = constraint_makeWriteSafeInt (t1, 0);
1163 cons = constraint_makeReadSafeInt (t1, 0);
1165 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1167 else if (lltok_isNot_Op (tok) )
1170 constraintList_free(e->trueEnsuresConstraints);
1172 e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints);
1173 constraintList_free(e->falseEnsuresConstraints);
1174 e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
1177 else if (lltok_isAmpersand_Op (tok) )
1181 else if (lltok_isMinus_Op (tok) )
1185 else if ( lltok_isExcl_Op (tok) )
1189 else if (lltok_isTilde_Op (tok) )
1195 llcontbug((message("Unsupported preop in %s", exprNode_unparse(e) ) ));
1202 exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
1204 if (lltok_isInc_Op (exprData_getUopTok (data) ) )
1206 DPRINTF(("doing ++"));
1207 t1 = exprData_getUopNode (data);
1208 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
1209 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1211 if (lltok_isDec_Op (exprData_getUopTok (data) ) )
1213 DPRINTF(("doing --"));
1214 t1 = exprData_getUopNode (data);
1215 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint );
1216 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1221 t2 = exprData_getCastNode (data);
1222 DPRINTF (( message ("Examining cast (%q)%s",
1223 qtype_unparse (exprData_getCastType (data)),
1224 exprNode_unparse (t2) )
1226 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1232 exprNode pred, trueBranch, falseBranch;
1234 pred = exprData_getTriplePred (data);
1235 trueBranch = exprData_getTripleTrue (data);
1236 falseBranch = exprData_getTripleFalse (data);
1238 exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint );
1240 temp = pred->ensuresConstraints;
1241 pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
1242 constraintList_free(temp);
1244 temp = pred->requiresConstraints;
1245 pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
1246 constraintList_free(temp);
1248 temp = pred->trueEnsuresConstraints;
1249 pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred);
1250 constraintList_free(temp);
1252 temp = pred->falseEnsuresConstraints;
1253 pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
1254 constraintList_free(temp);
1257 exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint );
1259 temp = trueBranch->ensuresConstraints;
1260 trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
1261 constraintList_free(temp);
1264 temp = trueBranch->requiresConstraints;
1265 trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
1266 constraintList_free(temp);
1269 temp = trueBranch->trueEnsuresConstraints;
1270 trueBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(trueBranch);
1271 constraintList_free(temp);
1273 temp = trueBranch->falseEnsuresConstraints;
1274 trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
1275 constraintList_free(temp);
1278 exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint );
1280 temp = falseBranch->ensuresConstraints;
1281 falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
1282 constraintList_free(temp);
1285 temp = falseBranch->requiresConstraints;
1286 falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
1287 constraintList_free(temp);
1290 temp = falseBranch->trueEnsuresConstraints;
1291 falseBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(falseBranch);
1292 constraintList_free(temp);
1294 temp = falseBranch->falseEnsuresConstraints;
1295 falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
1296 constraintList_free(temp);
1298 /* if pred is true e equals true otherwise pred equals false */
1300 cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1301 trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
1303 cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1304 falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
1306 e = doIfElse (e, pred, trueBranch, falseBranch);
1312 t1 = exprData_getPairA (data);
1313 t2 = exprData_getPairB (data);
1314 /* we essiantially treat this like expr1; expr2
1315 of course sequencePoint isn't adjusted so this isn't completely accurate
1317 exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint );
1318 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
1319 exprNode_mergeResolve (e, t1, t2);
1323 handledExprNode = FALSE;
1326 e->requiresConstraints = constraintList_preserveOrig ( e->requiresConstraints);
1327 e->ensuresConstraints = constraintList_preserveOrig ( e->ensuresConstraints);
1328 e->requiresConstraints = constraintList_addGeneratingExpr ( e->requiresConstraints, e);
1330 e->ensuresConstraints = constraintList_addGeneratingExpr ( e->ensuresConstraints, e);
1332 DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
1334 DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints) ) ));
1336 DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints) ) ));
1338 DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints) ) ));
1340 return; // handledExprNode;
1344 constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
1348 bool handledExprNode;
1353 if (exprNode_handleError (e))
1355 ret = constraintList_makeNew();
1358 ret = constraintList_copy (e->trueEnsuresConstraints );
1360 handledExprNode = TRUE;
1367 t1 = exprData_getSingle (data);
1368 ret = constraintList_addListFree ( ret, exprNode_traversTrueEnsuresConstraints (t1) );
1373 ret = constraintList_addListFree (ret,
1374 exprNode_traversTrueEnsuresConstraints
1375 (exprData_getPairA (data) ) );
1377 ret = constraintList_addListFree (ret,
1378 exprNode_traversTrueEnsuresConstraints
1379 (exprData_getPairB (data) ) );
1383 ret = constraintList_addListFree (ret,
1384 exprNode_traversTrueEnsuresConstraints
1385 (exprData_getUopNode (data) ) );
1389 ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
1390 (exprData_getUopNode (data) ) );
1394 ret = constraintList_addListFree (ret,
1395 exprNode_traversTrueEnsuresConstraints
1396 (exprData_getInitNode (data) ) );
1401 ret = constraintList_addListFree (ret,
1402 exprNode_traversTrueEnsuresConstraints
1403 (exprData_getOpA (data) ) );
1405 ret = constraintList_addListFree (ret,
1406 exprNode_traversTrueEnsuresConstraints
1407 (exprData_getOpB (data) ) );
1410 ret = constraintList_addListFree (ret,
1411 exprNode_traversTrueEnsuresConstraints
1412 (exprData_getOpA (data) ) );
1414 ret = constraintList_addListFree (ret,
1415 exprNode_traversTrueEnsuresConstraints
1416 (exprData_getOpB (data) ) );
1420 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1426 ret = constraintList_addListFree (ret,
1427 exprNode_traversTrueEnsuresConstraints
1428 (exprData_getSingle (data) ) );
1432 ret = constraintList_addListFree (ret,
1433 exprNode_traversTrueEnsuresConstraints
1434 (exprData_getFcn (data) ) );
1435 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1439 ret = constraintList_addListFree (ret,
1440 exprNode_traversTrueEnsuresConstraints
1441 (exprData_getSingle (data) ) );
1444 case XPR_NULLRETURN:
1445 // cstring_makeLiteral ("return");;
1449 ret = constraintList_addListFree (ret,
1450 exprNode_traversTrueEnsuresConstraints
1451 (exprData_getFieldNode (data) ) );
1452 //exprData_getFieldName (data) ;
1456 ret = constraintList_addListFree (ret,
1457 exprNode_traversTrueEnsuresConstraints
1458 (exprData_getFieldNode (data) ) );
1459 // exprData_getFieldName (data);
1462 case XPR_STRINGLITERAL:
1463 // cstring_copy (exprData_getLiteral (data));
1467 // cstring_copy (exprData_getLiteral (data));
1471 ret = constraintList_addListFree (ret,
1472 exprNode_traversTrueEnsuresConstraints
1473 (exprData_getUopNode (data) ) );
1478 ret = constraintList_addListFree (ret,
1479 exprNode_traversTrueEnsuresConstraints
1480 (exprData_getCastNode (data) ) );
1490 constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
1494 bool handledExprNode;
1499 if (exprNode_handleError (e))
1501 ret = constraintList_makeNew();
1504 ret = constraintList_copy (e->falseEnsuresConstraints );
1506 handledExprNode = TRUE;
1513 t1 = exprData_getSingle (data);
1514 ret = constraintList_addListFree ( ret,exprNode_traversFalseEnsuresConstraints (t1) );
1519 ret = constraintList_addListFree (ret,
1520 exprNode_traversFalseEnsuresConstraints
1521 (exprData_getPairA (data) ) );
1523 ret = constraintList_addListFree (ret,
1524 exprNode_traversFalseEnsuresConstraints
1525 (exprData_getPairB (data) ) );
1529 ret = constraintList_addListFree (ret,
1530 exprNode_traversFalseEnsuresConstraints
1531 (exprData_getUopNode (data) ) );
1535 ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
1536 (exprData_getUopNode (data) ) );
1539 ret = constraintList_addListFree (ret,
1540 exprNode_traversFalseEnsuresConstraints
1541 ( exprData_getInitNode (data) ) );
1545 ret = constraintList_addListFree (ret,
1546 exprNode_traversFalseEnsuresConstraints
1547 (exprData_getOpA (data) ) );
1549 ret = constraintList_addListFree (ret,
1550 exprNode_traversFalseEnsuresConstraints
1551 (exprData_getOpB (data) ) );
1554 ret = constraintList_addListFree (ret,
1555 exprNode_traversFalseEnsuresConstraints
1556 (exprData_getOpA (data) ) );
1558 ret = constraintList_addListFree (ret,
1559 exprNode_traversFalseEnsuresConstraints
1560 (exprData_getOpB (data) ) );
1564 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1570 ret = constraintList_addListFree (ret,
1571 exprNode_traversFalseEnsuresConstraints
1572 (exprData_getSingle (data) ) );
1576 ret = constraintList_addListFree (ret,
1577 exprNode_traversFalseEnsuresConstraints
1578 (exprData_getFcn (data) ) );
1579 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1583 ret = constraintList_addListFree (ret,
1584 exprNode_traversFalseEnsuresConstraints
1585 (exprData_getSingle (data) ) );
1588 case XPR_NULLRETURN:
1589 // cstring_makeLiteral ("return");;
1593 ret = constraintList_addListFree (ret,
1594 exprNode_traversFalseEnsuresConstraints
1595 (exprData_getFieldNode (data) ) );
1596 //exprData_getFieldName (data) ;
1600 ret = constraintList_addListFree (ret,
1601 exprNode_traversFalseEnsuresConstraints
1602 (exprData_getFieldNode (data) ) );
1603 // exprData_getFieldName (data);
1606 case XPR_STRINGLITERAL:
1607 // cstring_copy (exprData_getLiteral (data));
1611 // cstring_copy (exprData_getLiteral (data));
1615 ret = constraintList_addListFree (ret,
1616 exprNode_traversFalseEnsuresConstraints
1617 (exprData_getUopNode (data) ) );
1622 ret = constraintList_addListFree (ret,
1623 exprNode_traversFalseEnsuresConstraints
1624 (exprData_getCastNode (data) ) );
1635 /* walk down the tree and get all requires Constraints in each subexpression*/
1636 /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
1640 bool handledExprNode;
1645 if (exprNode_handleError (e))
1647 ret = constraintList_makeNew();
1650 ret = constraintList_copy (e->requiresConstraints );
1652 handledExprNode = TRUE;
1659 t1 = exprData_getSingle (data);
1660 ret = constraintList_addListFree ( ret, exprNode_traversRequiresConstraints (t1) );
1665 ret = constraintList_addListFree (ret,
1666 exprNode_traversRequiresConstraints
1667 (exprData_getPairA (data) ) );
1669 ret = constraintList_addListFree (ret,
1670 exprNode_traversRequiresConstraints
1671 (exprData_getPairB (data) ) );
1675 ret = constraintList_addListFree (ret,
1676 exprNode_traversRequiresConstraints
1677 (exprData_getUopNode (data) ) );
1681 ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
1682 (exprData_getUopNode (data) ) );
1685 ret = constraintList_addListFree (ret,
1686 exprNode_traversRequiresConstraints
1687 (exprData_getInitNode (data) ) );
1691 ret = constraintList_addListFree (ret,
1692 exprNode_traversRequiresConstraints
1693 (exprData_getOpA (data) ) );
1695 ret = constraintList_addListFree (ret,
1696 exprNode_traversRequiresConstraints
1697 (exprData_getOpB (data) ) );
1700 ret = constraintList_addListFree (ret,
1701 exprNode_traversRequiresConstraints
1702 (exprData_getOpA (data) ) );
1704 ret = constraintList_addListFree (ret,
1705 exprNode_traversRequiresConstraints
1706 (exprData_getOpB (data) ) );
1710 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1716 ret = constraintList_addListFree (ret,
1717 exprNode_traversRequiresConstraints
1718 (exprData_getSingle (data) ) );
1722 ret = constraintList_addListFree (ret,
1723 exprNode_traversRequiresConstraints
1724 (exprData_getFcn (data) ) );
1725 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1729 ret = constraintList_addListFree (ret,
1730 exprNode_traversRequiresConstraints
1731 (exprData_getSingle (data) ) );
1734 case XPR_NULLRETURN:
1735 // cstring_makeLiteral ("return");;
1739 ret = constraintList_addListFree (ret,
1740 exprNode_traversRequiresConstraints
1741 (exprData_getFieldNode (data) ) );
1742 //exprData_getFieldName (data) ;
1746 ret = constraintList_addListFree (ret,
1747 exprNode_traversRequiresConstraints
1748 (exprData_getFieldNode (data) ) );
1749 // exprData_getFieldName (data);
1752 case XPR_STRINGLITERAL:
1753 // cstring_copy (exprData_getLiteral (data));
1757 // cstring_copy (exprData_getLiteral (data));
1761 ret = constraintList_addListFree (ret,
1762 exprNode_traversRequiresConstraints
1763 (exprData_getUopNode (data) ) );
1768 ret = constraintList_addListFree (ret,
1769 exprNode_traversRequiresConstraints
1770 (exprData_getCastNode (data) ) );
1781 /* walk down the tree and get all Ensures Constraints in each subexpression*/
1782 /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
1786 bool handledExprNode;
1789 // constraintExpr tmp;
1794 if (exprNode_handleError (e))
1796 ret = constraintList_makeNew();
1800 ret = constraintList_copy (e->ensuresConstraints );
1801 handledExprNode = TRUE;
1806 "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
1807 exprNode_unparse (e),
1808 constraintList_print(e->ensuresConstraints)
1816 t1 = exprData_getSingle (data);
1817 ret = constraintList_addListFree ( ret,exprNode_traversEnsuresConstraints (t1) );
1822 ret = constraintList_addListFree (ret,
1823 exprNode_traversEnsuresConstraints
1824 (exprData_getPairA (data) ) );
1826 ret = constraintList_addListFree (ret,
1827 exprNode_traversEnsuresConstraints
1828 (exprData_getPairB (data) ) );
1832 ret = constraintList_addListFree (ret,
1833 exprNode_traversEnsuresConstraints
1834 (exprData_getUopNode (data) ) );
1838 ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
1839 (exprData_getUopNode (data) ) );
1843 ret = constraintList_addListFree (ret,
1844 exprNode_traversEnsuresConstraints
1845 (exprData_getInitNode (data) ) );
1850 ret = constraintList_addListFree (ret,
1851 exprNode_traversEnsuresConstraints
1852 (exprData_getOpA (data) ) );
1854 ret = constraintList_addListFree (ret,
1855 exprNode_traversEnsuresConstraints
1856 (exprData_getOpB (data) ) );
1859 ret = constraintList_addListFree (ret,
1860 exprNode_traversEnsuresConstraints
1861 (exprData_getOpA (data) ) );
1863 ret = constraintList_addListFree (ret,
1864 exprNode_traversEnsuresConstraints
1865 (exprData_getOpB (data) ) );
1869 // ctype_unparse (qtype_getType (exprData_getType (data) ) );
1875 ret = constraintList_addListFree (ret,
1876 exprNode_traversEnsuresConstraints
1877 (exprData_getSingle (data) ) );
1881 ret = constraintList_addListFree (ret,
1882 exprNode_traversEnsuresConstraints
1883 (exprData_getFcn (data) ) );
1884 /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
1888 ret = constraintList_addListFree (ret,
1889 exprNode_traversEnsuresConstraints
1890 (exprData_getSingle (data) ) );
1893 case XPR_NULLRETURN:
1894 // cstring_makeLiteral ("return");;
1898 ret = constraintList_addListFree (ret,
1899 exprNode_traversEnsuresConstraints
1900 (exprData_getFieldNode (data) ) );
1901 //exprData_getFieldName (data) ;
1905 ret = constraintList_addListFree (ret,
1906 exprNode_traversEnsuresConstraints
1907 (exprData_getFieldNode (data) ) );
1908 // exprData_getFieldName (data);
1911 case XPR_STRINGLITERAL:
1912 // cstring_copy (exprData_getLiteral (data));
1916 // cstring_copy (exprData_getLiteral (data));
1920 ret = constraintList_addListFree (ret,
1921 exprNode_traversEnsuresConstraints
1922 (exprData_getUopNode (data) ) );
1926 ret = constraintList_addListFree (ret,
1927 exprNode_traversEnsuresConstraints
1928 (exprData_getCastNode (data) ) );
1935 "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s",
1936 exprNode_unparse (e),
1937 // constraintList_print(e->ensuresConstraints),
1938 constraintList_print(ret)
1946 /*drl moved out of constraintResolve.c 07-02-001 */
1947 void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint)
1949 temp->requiresConstraints = constraintList_makeNew();
1950 temp->ensuresConstraints = constraintList_makeNew();
1951 temp->trueEnsuresConstraints = constraintList_makeNew();
1952 temp->falseEnsuresConstraints = constraintList_makeNew();
1954 exprNodeList_elements (arglist, el)
1956 constraintList temp2;
1957 exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
1958 temp2 = el->requiresConstraints;
1959 el->requiresConstraints = exprNode_traversRequiresConstraints(el);
1960 constraintList_free(temp2);
1962 temp2 = el->ensuresConstraints;
1963 el->ensuresConstraints = exprNode_traversEnsuresConstraints(el);
1964 constraintList_free(temp2);
1966 temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
1967 el->requiresConstraints);
1969 temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
1970 el->ensuresConstraints);
1972 end_exprNodeList_elements;
1976 /*drl moved out of constraintResolve.c 07-03-001 */
1977 constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
1979 constraintList postconditions;
1981 DPRINTF( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
1983 temp = exprNode_getUentry (fcn);
1985 postconditions = uentry_getFcnPostconditions (temp);
1987 if (constraintList_isDefined(postconditions) )
1989 postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
1990 postconditions = constraintList_doFixResult (postconditions, fcnCall);
1994 postconditions = constraintList_makeNew();
1997 return postconditions;
2001 /*drl moved out of constraintResolve.c 07-02-001 */
2002 constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
2004 constraintList preconditions;
2006 DPRINTF( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
2008 temp = exprNode_getUentry (fcn);
2010 preconditions = uentry_getFcnPreconditions (temp);
2012 if (constraintList_isDefined(preconditions) )
2014 preconditions = constraintList_togglePost (preconditions);
2015 preconditions = constraintList_preserveCallInfo(preconditions, fcn);
2016 preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
2020 if (constraintList_isUndefined(preconditions) )
2021 preconditions = constraintList_makeNew();
2023 DPRINTF (( message("Done checkCall\n") ));
2024 DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) ));
2025 return preconditions;