2 ** Splint - annotation-assisted static program checker
3 ** Copyright (C) 1994-2003 University of Virginia,
4 ** Massachusetts Institute of Technology
6 ** This program is free software; you can redistribute it and/or modify it
7 ** under the terms of the GNU General Public License as published by the
8 ** Free Software Foundation; either version 2 of the License, or (at your
9 ** option) any later version.
11 ** This program is distributed in the hope that it will be useful, but
12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14 ** General Public License for more details.
16 ** The GNU General Public License is available from http://www.gnu.org/ or
17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
18 ** MA 02111-1307, USA.
20 ** For information on splint: info@splint.org
21 ** To report a bug: splint-bug@splint.org
22 ** For more information: http://www.splint.org
26 ** constraintGeneration.c
29 /* #define DEBUGPRINT 1 */
31 # include <ctype.h> /* for isdigit */
32 # include "splintMacros.nf"
35 # include "cgrammar_tokens.h"
37 # include "exprChecks.h"
38 # include "exprNodeSList.h"
40 /*drl We need to access the internal representation of exprNode
41 because these functions walk down the parse tree and need a richer
42 information than is accessible through the exprNode interface.*/
46 static /*@nullwhentrue@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e);
48 static void exprNode_stmt (/*@temp@*/ /*@temp@*/ exprNode p_e);
49 static void exprNode_multiStatement (/*@temp@*/ exprNode p_e);
51 static constraintList exprNode_traversTrueEnsuresConstraints (/*@temp@*/ exprNode p_e);
52 static constraintList exprNode_traversFalseEnsuresConstraints (/*@temp@*/ exprNode p_e);
54 static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/;
56 static constraintList checkCall (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist);
58 static bool exprNode_isUnhandled (/*@temp@*/ /*@observer@*/ exprNode e)
60 llassert(exprNode_isDefined(e));
86 DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e))));
98 /*@nullwhentrue@*/ bool exprNode_handleError (exprNode e)
100 if (exprNode_isError (e) || exprNode_isUnhandled (e))
108 /* evans 2002-03-2 - parameter was dependent */
109 bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
111 if (exprNode_isError (e))
114 if (exprNode_isUnhandled (e))
116 DPRINTF((message("Warning ignoring %s", exprNode_unparse (e))));
120 DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse(e),
121 fileloc_unparse(exprNode_getfileloc(e)))));
123 if (exprNode_isMultiStatement (e))
125 exprNode_multiStatement(e);
131 /* loc = exprNode_getNextSequencePoint(e); */
132 /* exprNode_exprTraverse(e, FALSE, FALSE, loc); */
134 /* fileloc_free(loc); */
144 c = constraintList_makeFixedArrayConstraints (e->uses);
145 e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, c);
146 constraintList_free(c);
149 DPRINTF ((message ("e->requiresConstraints %s", constraintList_printDetailed (e->requiresConstraints))));
153 static void exprNode_stmt (/*@temp@*/ exprNode e)
159 if (exprNode_isError(e))
164 /*e->requiresConstraints = constraintList_makeNew();
165 e->ensuresConstraints = constraintList_makeNew(); */
167 DPRINTF(("expNode_stmt: STMT:"));
168 s = exprNode_unparse(e);
169 DPRINTF ((message("exprNode_stmt: STMT: %s ", s)));
171 if (e->kind == XPR_INIT)
173 constraintList tempList;
175 DPRINTF ((message ("%s ", exprNode_unparse (e))));
176 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
177 exprNode_exprTraverse (e, FALSE, FALSE, loc);
180 tempList = e->requiresConstraints;
181 e->requiresConstraints = exprNode_traversRequiresConstraints(e);
182 constraintList_free(tempList);
184 tempList = e->ensuresConstraints;
185 e->ensuresConstraints = exprNode_traversEnsuresConstraints(e);
186 constraintList_free(tempList);
190 /*drl 2/13/002 patched bug so return statement will be checked*/
191 /*return is a stmt not not expression ...*/
192 if (e->kind == XPR_RETURN)
194 constraintList tempList;
196 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
198 exprNode_exprTraverse (exprData_getSingle (e->edata), FALSE, TRUE, loc);
201 tempList = e->requiresConstraints;
202 e->requiresConstraints = exprNode_traversRequiresConstraints(e);
203 constraintList_free(tempList);
206 if (e->kind != XPR_STMT)
209 DPRINTF (("Not Stmt"));
210 DPRINTF ((message ("%s ", exprNode_unparse (e))));
212 if (exprNode_isMultiStatement (e))
214 exprNode_multiStatement (e); /* evans 2001-08-21: spurious return removed */
218 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
220 exprNode_exprTraverse (e, FALSE, TRUE, loc);
228 DPRINTF ((message ("%s ", exprNode_unparse (e))));
230 snode = exprData_getUopNode (e->edata);
232 /* could be stmt involving multiple statements:
233 i.e. if, while for ect.
236 if (exprNode_isMultiStatement (snode))
238 exprNode_multiStatement (snode);
239 (void) exprNode_copyConstraints (e, snode);
243 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
244 exprNode_exprTraverse (snode, FALSE, FALSE, loc);
248 constraintList_free (e->requiresConstraints);
249 e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
251 constraintList_free (e->ensuresConstraints);
252 e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode);
254 DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
255 constraintList_print(e->requiresConstraints),
256 constraintList_print(e->ensuresConstraints))));
261 static void exprNode_stmtList (/*@dependent@*/ exprNode e)
263 exprNode stmt1, stmt2;
264 if (exprNode_isError (e))
270 Handle case of stmtList with only one statement:
271 The parse tree stores this as stmt instead of stmtList
274 if (e->kind != XPR_STMTLIST)
279 llassert (e->kind == XPR_STMTLIST);
280 DPRINTF(("exprNode_stmtList STMTLIST:"));
281 DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e))));
282 stmt1 = exprData_getPairA (e->edata);
283 stmt2 = exprData_getPairB (e->edata);
286 DPRINTF(("exprNode_stmtlist "));
287 DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2))));
289 exprNode_stmt (stmt1);
290 DPRINTF(("\nstmt after stmtList call "));
292 exprNode_stmt (stmt2);
293 exprNode_mergeResolve (e, stmt1, stmt2);
295 DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
296 constraintList_print(e->requiresConstraints),
297 constraintList_print(e->ensuresConstraints))));
301 static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
305 DPRINTF ((message ("doIf: %s ", exprNode_unparse(e))));
307 llassert(exprNode_isDefined(test));
308 llassert (exprNode_isDefined (e));
309 llassert (exprNode_isDefined (body));
312 DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints))));
314 DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints))));
316 DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints))));
318 DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints))));
322 DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints))));
324 DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->ensuresConstraints))));
326 DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->trueEnsuresConstraints))));
328 DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_printDetailed(test->falseEnsuresConstraints))));
332 temp = test->trueEnsuresConstraints;
333 test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
334 constraintList_free(temp);
336 temp = test->ensuresConstraints;
337 test->ensuresConstraints = exprNode_traversEnsuresConstraints (test);
338 constraintList_free(temp);
340 temp = test->requiresConstraints;
341 test->requiresConstraints = exprNode_traversRequiresConstraints (test);
342 constraintList_free(temp);
345 test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints);
347 DPRINTF ((message ("doIf: test ensures %s ", constraintList_print(test->ensuresConstraints))));
349 DPRINTF ((message ("doIf: test true ensures %s ", constraintList_print(test->trueEnsuresConstraints))));
351 constraintList_free(e->requiresConstraints);
354 e->requiresConstraints = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints);
356 e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints,
357 test->ensuresConstraints);
358 temp = e->requiresConstraints;
359 e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints);
360 constraintList_free(temp);
363 /* drl possible problem : warning bad */
364 constraintList_free(e->ensuresConstraints);
365 e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
367 if (exprNode_mayEscape (body))
369 DPRINTF ((message("doIf: the if statement body %s returns or exits", exprNode_unparse(body))));
370 e->ensuresConstraints = constraintList_mergeEnsuresFreeFirst (e->ensuresConstraints,
371 test->falseEnsuresConstraints);
374 DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints))));
380 Also used for condition i.e. ?: operation
383 This function assumes that p, trueBranch, falseBranch have have all been traversed
384 for constraints i.e. we assume that exprNode_traversEnsuresConstraints,
385 exprNode_traversRequiresConstraints, exprNode_traversTrueEnsuresConstraints,
386 exprNode_traversFalseEnsuresConstraints have all been run
389 static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch)
391 constraintList c1, cons, t, t2, f, f2;
393 llassert (exprNode_isDefined (e));
394 llassert (exprNode_isDefined (p));
395 llassert (exprNode_isDefined (trueBranch));
396 llassert (exprNode_isDefined (falseBranch));
397 DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e))));
399 /* do requires clauses */
400 c1 = constraintList_copy (p->ensuresConstraints);
402 t = constraintList_reflectChanges(trueBranch->requiresConstraints, p->trueEnsuresConstraints);
403 t = constraintList_reflectChangesFreePre (t, p->ensuresConstraints);
405 cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints);
406 cons = constraintList_reflectChangesFreePre (cons, c1);
408 constraintList_free (e->requiresConstraints);
409 e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons);
410 e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints);
412 /* do ensures clauses
413 find the the ensures lists for each subbranch
416 t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
418 t = constraintList_mergeEnsures (p->ensuresConstraints, t);
419 constraintList_free(t2);
421 f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
423 f = constraintList_mergeEnsures (p->ensuresConstraints, f);
424 constraintList_free(f2);
426 /* find ensures for whole if/else statement */
428 constraintList_free(e->ensuresConstraints);
430 e->ensuresConstraints = constraintList_logicalOr (t, f);
432 constraintList_free(t);
433 constraintList_free(f);
434 constraintList_free(cons);
435 constraintList_free(c1);
437 DPRINTF ((message ("doIfElse: if requires %q ", constraintList_print(e->requiresConstraints))));
438 DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_print(e->ensuresConstraints))));
443 static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
445 DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e))));
446 return doIf (e, test, body);
449 /*@only@*/ constraintList constraintList_makeFixedArrayConstraints (/*@observer@*/ sRefSet s)
453 ret = constraintList_makeNew();
455 sRefSet_elements (s, el)
457 if (sRef_isFixedArray(el))
460 DPRINTF((message("%s is a fixed array",
462 size = sRef_getArraySize(el);
463 DPRINTF((message("%s is a fixed array with size %d",
464 sRef_unparse(el), (int)size)));
465 con = constraint_makeSRefSetBufferSize (el, size_toLong (size - 1));
466 ret = constraintList_add(ret, con);
470 DPRINTF((message("%s is not a fixed array",
474 if (sRef_isExternallyVisible (el))
477 DPRINTF((message("%s is externally visible",
479 con = constraint_makeSRefWriteSafeInt(el, 0);
480 ret = constraintList_add(ret, con);
482 con = constraint_makeSRefReadSafeInt(el, 0);
484 ret = constraintList_add(ret, con);
489 end_sRefSet_elements ;
491 DPRINTF((message("constraintList_makeFixedArrayConstraints returning %s",
492 constraintList_print(ret))));
497 exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e)
500 DPRINTF(("makeDataTypeConstraints"));
502 c = constraintList_makeFixedArrayConstraints (e->uses);
504 e->ensuresConstraints = constraintList_addListFree (e->ensuresConstraints, c);
510 static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, /*@dependent@*/ exprNode forBody)
512 exprNode init, test, inc;
513 /* merge the constraints: modle as if statement */
520 llassert (exprNode_isDefined (e));
521 llassert (exprNode_isDefined (forPred));
522 llassert (exprNode_isDefined (forBody));
524 init = exprData_getTripleInit (forPred->edata);
525 test = exprData_getTripleTest (forPred->edata);
526 inc = exprData_getTripleInc (forPred->edata);
528 if (((exprNode_isError (test) /*|| (exprNode_isError(init))*/) || (exprNode_isError (inc))))
530 DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e))));
534 exprNode_forLoopHeuristics(e, forPred, forBody);
536 constraintList_free(e->requiresConstraints);
537 e->requiresConstraints = constraintList_reflectChanges(forBody->requiresConstraints, test->ensuresConstraints);
538 e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints);
539 e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints);
541 if (!forBody->canBreak)
543 e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints));
544 e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy(test->falseEnsuresConstraints));
548 DPRINTF(("Can break"));
552 static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/ exprNode e)
554 /* !!! DRL - this is ridiculous! Read the manual on memory annotations please! */
559 exprNode_doGenerateConstraintSwitch
560 (/*@dependent@*/ exprNode switchExpr,
561 /*@dependent@*/ exprNode body,
562 /*@special@*/ constraintList *currentRequires,
563 /*@special@*/ constraintList *currentEnsures,
564 /*@special@*/ constraintList *savedRequires,
565 /*@special@*/ constraintList *savedEnsures)
566 /*@post:only *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/
567 /*@sets *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/
569 exprNode stmt, stmtList;
571 DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s",
572 exprNode_unparse(switchExpr), exprNode_unparse(body)
575 if (exprNode_isError(body))
577 *currentRequires = constraintList_makeNew ();
578 *currentEnsures = constraintList_makeNew ();
580 *savedRequires = constraintList_makeNew ();
581 *savedEnsures = constraintList_makeNew ();
587 if (body->kind != XPR_STMTLIST)
589 DPRINTF((message("exprNode_doGenerateConstraintSwitch: non stmtlist: %s",
590 exprNode_unparse(body))));
592 stmtList = exprNode_undefined;
593 stmt = exprNode_makeDependent(stmt);
594 stmtList = exprNode_makeDependent(stmtList);
598 stmt = exprData_getPairB(body->edata);
599 stmtList = exprData_getPairA(body->edata);
600 stmt = exprNode_makeDependent(stmt);
601 stmtList = exprNode_makeDependent(stmtList);
604 DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s stmt: %s",
605 exprNode_unparse(stmtList), exprNode_unparse(stmt))
609 exprNode_doGenerateConstraintSwitch (switchExpr, stmtList, currentRequires, currentEnsures,
610 savedRequires, savedEnsures);
612 if (exprNode_isError(stmt))
619 switchExpr = exprNode_makeDependent (switchExpr);
621 if (! exprNode_isCaseMarker(stmt))
626 DPRINTF ((message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt),
627 constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints))));
629 temp = constraintList_reflectChanges (stmt->requiresConstraints,
632 *currentRequires = constraintList_mergeRequiresFreeFirst(
636 constraintList_free(temp);
638 *currentEnsures = constraintList_mergeEnsuresFreeFirst
640 stmt->ensuresConstraints);
641 DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
642 "%s currentEnsures:%s",
643 exprNode_unparse(switchExpr), exprNode_unparse(body),
644 constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
652 if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList))
655 ** merge current and saved constraint with Logical Or...
656 ** make a constraint for ensures
662 DPRINTF ((message("Got case marker")));
664 if (constraintList_isUndefined(*savedEnsures) &&
665 constraintList_isUndefined(*savedRequires))
667 llassert(constraintList_isUndefined(*savedEnsures));
668 llassert(constraintList_isUndefined(*savedRequires));
669 *savedEnsures = constraintList_copy(*currentEnsures);
670 *savedRequires = constraintList_copy(*currentRequires);
674 DPRINTF ((message("Doing logical or")));
675 temp = constraintList_logicalOr (*savedEnsures, *currentEnsures);
676 constraintList_free (*savedEnsures);
677 *savedEnsures = temp;
679 *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires);
682 con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
683 (stmt->edata), exprNode_getfileloc(stmt));
686 constraintList_free(*currentEnsures);
687 *currentEnsures = constraintList_makeNew();
688 *currentEnsures = constraintList_add(*currentEnsures, con);
690 constraintList_free(*currentRequires);
691 *currentRequires = constraintList_makeNew();
692 DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
693 "%s savedEnsures:%s",
694 exprNode_unparse(switchExpr), exprNode_unparse(body),
695 constraintList_print(*savedRequires), constraintList_print(*savedEnsures)
700 else if (exprNode_isCaseMarker(stmt))
701 /* prior case has no break. */
704 We don't do anything to the sved constraints because the case hasn't ended
705 The new ensures constraints for the case will be:
706 the constraint for the case statement (CASE_LABEL == SWITCH_EXPR) logicalOr currentEnsures
712 constraintList ensuresTemp;
714 DPRINTF ((message("Got case marker with no prior break")));
716 con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle
717 (stmt->edata), exprNode_getfileloc(stmt));
719 ensuresTemp = constraintList_makeNew();
721 ensuresTemp = constraintList_add (ensuresTemp, con);
723 if (exprNode_isError(stmtList))
725 constraintList_free(*currentEnsures);
727 *currentEnsures = constraintList_copy(ensuresTemp);
728 constraintList_free(ensuresTemp);
734 temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
736 constraintList_free(*currentEnsures);
737 constraintList_free(ensuresTemp);
739 *currentEnsures = temp;
741 constraintList_free(*currentRequires);
743 *currentRequires = constraintList_makeNew();
748 we handle the case of ! exprNode_isCaseMarker above
749 the else if clause should always be true.
754 DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
755 "%s currentEnsures:%s",
756 exprNode_unparse(switchExpr), exprNode_unparse(body),
757 constraintList_print(*currentRequires), constraintList_print(*currentEnsures)
765 static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt)
767 constraintList constraintsRequires;
768 constraintList constraintsEnsures;
769 constraintList lastRequires;
770 constraintList lastEnsures;
775 switchExpr = exprData_getPairA (switchStmt->edata);
776 body = exprData_getPairB (switchStmt->edata);
778 if (!exprNode_isDefined (body))
784 DPRINTF((message("")));
786 if (body->kind == XPR_BLOCK)
787 body = exprData_getSingle(body->edata);
790 constraintsRequires = constraintList_undefined;
791 constraintsEnsures = constraintList_undefined;
793 lastRequires = constraintList_makeNew();
794 lastEnsures = constraintList_makeNew();
798 /*@i6534 - evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
799 exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires,
800 &lastEnsures, &constraintsRequires, &constraintsEnsures);
804 merge current and saved constraint with Logical Or...
805 make a constraint for ensures
808 constraintList_free(switchStmt->requiresConstraints);
809 constraintList_free(switchStmt->ensuresConstraints);
811 if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires))
813 switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures);
814 switchStmt->requiresConstraints = constraintList_mergeRequires(constraintsRequires, lastRequires);
815 constraintList_free (constraintsRequires);
816 constraintList_free (constraintsEnsures);
820 switchStmt->ensuresConstraints = constraintList_copy(lastEnsures);
821 switchStmt->requiresConstraints = constraintList_copy(lastRequires);
824 constraintList_free (lastRequires);
825 constraintList_free (lastEnsures);
827 DPRINTF(((message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s",
828 constraintList_print(switchStmt->requiresConstraints),
829 constraintList_print(switchStmt->ensuresConstraints)
834 static exprNode doSwitch (/*@returned@*/ /*@notnull@*/ exprNode e)
840 DPRINTF ((message ("doSwitch for: switch (%s) %s",
841 exprNode_unparse (exprData_getPairA (data)),
842 exprNode_unparse (exprData_getPairB (data)))));
844 body = exprData_getPairB (data);
845 exprNode_generateConstraintSwitch (e);
849 void exprNode_multiStatement (/*@dependent@*/ exprNode e)
855 exprNode p, trueBranch, falseBranch;
856 exprNode forPred, forBody;
861 DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e),
862 fileloc_unparse(exprNode_getfileloc(e)))));
864 if (exprNode_handleError (e))
877 forPred = exprData_getPairA (data);
878 forBody = exprData_getPairB (data);
880 /* First generate the constraints */
881 exprNode_generateConstraints (forPred);
882 exprNode_generateConstraints (forBody);
885 doFor (e, forPred, forBody);
890 exprNode_generateConstraints (exprData_getTripleInit (data));
891 test = exprData_getTripleTest (data);
892 exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
893 exprNode_generateConstraints (exprData_getTripleInc (data));
895 if (!exprNode_isError(test))
897 constraintList temp2;
898 temp2 = test->trueEnsuresConstraints;
899 test->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(test);
900 constraintList_free(temp2);
903 exprNode_generateConstraints (exprData_getTripleInc (data));
907 e1 = exprData_getPairA (data);
908 e2 = exprData_getPairB (data);
910 exprNode_exprTraverse (e1,
911 FALSE, FALSE, exprNode_loc(e1));
913 exprNode_generateConstraints (e2);
915 e = doWhile (e, e1, e2);
921 DPRINTF ((exprNode_unparse(e)));
922 e1 = exprData_getPairA (data);
923 e2 = exprData_getPairB (data);
925 exprNode_exprTraverse (e1, FALSE, FALSE, exprNode_loc(e1));
927 exprNode_generateConstraints (e2);
928 e = doIf (e, e1, e2);
932 DPRINTF(("Starting IFELSE"));
933 p = exprData_getTriplePred (data);
935 trueBranch = exprData_getTripleTrue (data);
936 falseBranch = exprData_getTripleFalse (data);
938 exprNode_exprTraverse (p,
939 FALSE, FALSE, exprNode_loc(p));
940 exprNode_generateConstraints (trueBranch);
941 exprNode_generateConstraints (falseBranch);
943 llassert (exprNode_isDefined (p));
944 temp = p->ensuresConstraints;
945 p->ensuresConstraints = exprNode_traversEnsuresConstraints (p);
946 constraintList_free(temp);
948 temp = p->requiresConstraints;
949 p->requiresConstraints = exprNode_traversRequiresConstraints (p);
950 constraintList_free(temp);
952 temp = p->trueEnsuresConstraints;
953 p->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(p);
954 constraintList_free(temp);
958 DPRINTF((message("p->trueEnsuresConstraints before substitue %s", constraintList_print(p->trueEnsuresConstraints) )
961 /*drl 10/10/2002 this is a bit of a hack but the reason why we do this is so that any function post conditions or similar things get applied correctly to each branch. e.g. in strlen(s) < 5 we want the trueEnsures to be maxRead(s) < 5*/
963 p->trueEnsuresConstraints = constraintList_substituteFreeTarget (p->trueEnsuresConstraints,
964 p->ensuresConstraints);
966 DPRINTF(( message ("p->trueEnsuresConstraints after substitue %s", constraintList_print(p->trueEnsuresConstraints) )
969 temp = p->falseEnsuresConstraints;
970 p->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(p);
971 constraintList_free(temp);
973 /*See comment on trueEnsures*/
974 p->falseEnsuresConstraints = constraintList_substituteFreeTarget (p->falseEnsuresConstraints,
975 p->ensuresConstraints);
977 e = doIfElse (e, p, trueBranch, falseBranch);
978 DPRINTF(("Done IFELSE"));
983 e2 = (exprData_getPairB (data));
984 e1 = (exprData_getPairA (data));
986 DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1))));
987 exprNode_generateConstraints (e2);
988 exprNode_generateConstraints (e1);
989 e = exprNode_copyConstraints (e, e2);
990 DPRINTF ((message ("e = %s ", constraintList_print(e->requiresConstraints))));
998 tempExpr = exprData_getSingle (data);
1000 exprNode_generateConstraints (tempExpr);
1002 if (exprNode_isDefined(tempExpr) )
1004 constraintList_free(e->requiresConstraints);
1005 e->requiresConstraints = constraintList_copy (tempExpr->requiresConstraints);
1006 constraintList_free(e->ensuresConstraints);
1007 e->ensuresConstraints = constraintList_copy (tempExpr->ensuresConstraints);
1021 exprNode_stmtList (e);
1031 static bool lltok_isBoolean_Op (lltok tok)
1033 /*this should really be a switch statement but
1034 I don't want to violate the abstraction
1035 maybe this should go in lltok.c */
1037 if (lltok_isEqOp (tok))
1041 if (lltok_isAndOp (tok))
1047 if (lltok_isOrOp (tok))
1052 if (lltok_isGt_Op (tok))
1056 if (lltok_isLt_Op (tok))
1061 if (lltok_isLe_Op (tok))
1066 if (lltok_isGe_Op (tok))
1076 static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint)
1082 constraintList tempList, temp;
1084 if (exprNode_isUndefined(e) )
1086 llassert (exprNode_isDefined(e) );
1092 tok = exprData_getOpTok (data);
1093 t1 = exprData_getOpA (data);
1094 t2 = exprData_getOpB (data);
1096 /* drl 3/2/2003 we know this because of the type of expression*/
1097 llassert( exprNode_isDefined(t1) && exprNode_isDefined(t2) );
1100 tempList = constraintList_undefined;
1102 /* arithmetic tests */
1104 if (lltok_isEqOp (tok))
1106 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
1107 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1111 if (lltok_isLt_Op (tok))
1113 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1114 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1115 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1116 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1119 if (lltok_isGe_Op (tok))
1121 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1122 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1124 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1125 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1128 if (lltok_isGt_Op (tok))
1130 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1131 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1132 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1133 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1136 if (lltok_isLe_Op (tok))
1138 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1139 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1141 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1142 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1145 /* Logical operations */
1147 if (lltok_isAndOp (tok))
1150 tempList = constraintList_copy (t1->trueEnsuresConstraints);
1151 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1152 e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1154 /* false ensures: fens t1 or tens t1 and fens t2 */
1155 tempList = constraintList_copy (t1->trueEnsuresConstraints);
1156 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1158 tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
1159 constraintList_free (temp);
1161 /* evans - was constraintList_addList - memory leak detected by splint */
1162 e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList);
1164 else if (lltok_isOrOp (tok))
1167 tempList = constraintList_copy (t1->falseEnsuresConstraints);
1168 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1169 e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList);
1171 /* true ensures: tens t1 or fens t1 and tens t2 */
1172 tempList = constraintList_copy (t1->falseEnsuresConstraints);
1173 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1176 tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
1177 constraintList_free(temp);
1179 e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1180 tempList = constraintList_undefined;
1184 DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok))));
1188 void exprNode_exprTraverse (/*@dependent@*/ exprNode e, bool definatelv, bool definaterv, /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
1190 exprNode t1, t2, fcn;
1192 bool handledExprNode;
1196 constraintList temp;
1198 if (exprNode_isError(e))
1203 DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse(e),
1204 fileloc_unparse(exprNode_getfileloc(e)))));
1206 /*e->requiresConstraints = constraintList_makeNew();
1207 e->ensuresConstraints = constraintList_makeNew();
1208 e->trueEnsuresConstraints = constraintList_makeNew();;
1209 e->falseEnsuresConstraints = constraintList_makeNew();;
1212 if (exprNode_isUnhandled (e))
1217 handledExprNode = TRUE;
1224 t1 = exprData_getSingle (data);
1225 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
1226 e = exprNode_copyConstraints (e, t1);
1233 t1 = (exprData_getPairA (data));
1234 t2 = (exprData_getPairB (data));
1235 cons = constraint_makeWriteSafeExprNode (t1, t2);
1239 t1 = (exprData_getPairA (data));
1240 t2 = (exprData_getPairB (data));
1241 cons = constraint_makeReadSafeExprNode (t1, t2);
1244 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1245 cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
1246 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1248 cons = constraint_makeEnsureLteMaxRead (t2, t1);
1249 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1251 exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
1252 exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
1254 /*@i325 Should check which is array/index. */
1258 exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
1268 t = exprData_getInitId (data);
1269 ue = usymtab_lookup (idDecl_observeId (t));
1270 lhs = exprNode_createId (ue);
1272 t2 = exprData_getInitNode (data);
1274 /* DPRINTF(((message("initialization: %s = %s",
1275 exprNode_unparse(lhs),
1276 exprNode_unparse(t2)
1280 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1282 /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
1283 if ((!exprNode_isError (e)) && (!exprNode_isError(t2)))
1285 cons = constraint_makeEnsureEqual (e, t2, sequencePoint);
1286 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1292 t1 = exprData_getOpA (data);
1293 t2 = exprData_getOpB (data);
1294 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1295 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1297 /* this test is nessecary because some expressions generate a null expression node. function pointer do that -- drl */
1298 if ((!exprNode_isError (t1)) && (!exprNode_isError(t2)))
1300 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
1301 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1305 t1 = exprData_getOpA (data);
1306 t2 = exprData_getOpB (data);
1307 tok = exprData_getOpTok (data);
1309 if (lltok_getTok (tok) == ADD_ASSIGN)
1311 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1312 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1314 cons = constraint_makeAddAssign (t1, t2, sequencePoint);
1315 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1317 else if (lltok_getTok (tok) == SUB_ASSIGN)
1319 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1320 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1322 cons = constraint_makeSubtractAssign (t1, t2, sequencePoint);
1323 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1327 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
1328 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1331 if (lltok_isBoolean_Op (tok))
1332 exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
1336 /*@i43 drl possible problem : warning make sure the case can be ignored.. */
1342 C standard says operand to sizeof isn't evaluated unless
1343 its a variable length array. So we don't generate constraints.
1349 fcn = exprData_getFcn(data);
1351 exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint);
1352 DPRINTF ((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data)))));
1354 llassert( exprNode_isDefined(fcn) );
1356 fcn->requiresConstraints = constraintList_addListFree (fcn->requiresConstraints,
1357 checkCall (fcn, exprData_getArgs (data) ));
1359 fcn->ensuresConstraints = constraintList_addListFree (fcn->ensuresConstraints,
1360 exprNode_getPostConditions(fcn, exprData_getArgs (data),e ));
1362 t1 = exprNode_createNew (exprNode_getType (e));
1363 checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
1364 exprNode_mergeResolve (e, t1, fcn);
1369 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint);
1372 case XPR_NULLRETURN:
1378 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint);
1382 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint);
1385 case XPR_STRINGLITERAL:
1394 t1 = exprData_getUopNode(data);
1397 /* drl 3/2/2003 we know this because of the type of expression*/
1398 llassert( exprNode_isDefined(t1) );
1401 tok = (exprData_getUopTok (data));
1402 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
1403 /*handle * pointer access */
1404 if (lltok_isIncOp (tok))
1406 DPRINTF(("doing ++(var)"));
1407 t1 = exprData_getUopNode (data);
1408 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint);
1409 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1411 else if (lltok_isDecOp (tok))
1413 DPRINTF(("doing --(var)"));
1414 t1 = exprData_getUopNode (data);
1415 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint);
1416 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1418 else if (lltok_isMult(tok ))
1422 cons = constraint_makeWriteSafeInt (t1, 0);
1426 cons = constraint_makeReadSafeInt (t1, 0);
1428 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1430 else if (lltok_isNotOp (tok))
1433 constraintList_free(e->trueEnsuresConstraints);
1435 e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints);
1436 constraintList_free(e->falseEnsuresConstraints);
1437 e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
1440 else if (lltok_isAmpersand_Op (tok))
1444 else if (lltok_isMinus_Op (tok))
1448 else if (lltok_isExcl_Op (tok))
1452 else if (lltok_isTilde_Op (tok))
1458 llcontbug (message("Unsupported preop in %s", exprNode_unparse(e)));
1464 exprNode_exprTraverse (exprData_getUopNode (data), TRUE,
1465 definaterv, sequencePoint);
1467 if (lltok_isIncOp (exprData_getUopTok (data)))
1469 DPRINTF(("doing ++"));
1470 t1 = exprData_getUopNode (data);
1471 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint);
1472 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1474 if (lltok_isDecOp (exprData_getUopTok (data)))
1476 DPRINTF(("doing --"));
1477 t1 = exprData_getUopNode (data);
1478 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint);
1479 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1484 t2 = exprData_getCastNode (data);
1485 DPRINTF ((message ("Examining cast (%q)%s",
1486 qtype_unparse (exprData_getCastType (data)),
1487 exprNode_unparse (t2))
1489 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1495 exprNode pred, trueBranch, falseBranch;
1497 pred = exprData_getTriplePred (data);
1498 trueBranch = exprData_getTripleTrue (data);
1499 falseBranch = exprData_getTripleFalse (data);
1501 llassert (exprNode_isDefined (pred));
1502 llassert (exprNode_isDefined (trueBranch));
1503 llassert (exprNode_isDefined (falseBranch));
1505 exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint);
1507 temp = pred->ensuresConstraints;
1508 pred->ensuresConstraints = exprNode_traversEnsuresConstraints(pred);
1509 constraintList_free(temp);
1511 temp = pred->requiresConstraints;
1512 pred->requiresConstraints = exprNode_traversRequiresConstraints(pred);
1513 constraintList_free(temp);
1515 temp = pred->trueEnsuresConstraints;
1516 pred->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(pred);
1517 constraintList_free(temp);
1519 temp = pred->falseEnsuresConstraints;
1520 pred->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(pred);
1521 constraintList_free(temp);
1523 exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint);
1525 temp = trueBranch->ensuresConstraints;
1526 trueBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(trueBranch);
1527 constraintList_free(temp);
1529 temp = trueBranch->requiresConstraints;
1530 trueBranch->requiresConstraints = exprNode_traversRequiresConstraints(trueBranch);
1531 constraintList_free(temp);
1534 temp = trueBranch->trueEnsuresConstraints;
1535 trueBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(trueBranch);
1536 constraintList_free(temp);
1538 temp = trueBranch->falseEnsuresConstraints;
1539 trueBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(trueBranch);
1540 constraintList_free(temp);
1542 exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint);
1544 temp = falseBranch->ensuresConstraints;
1545 falseBranch->ensuresConstraints = exprNode_traversEnsuresConstraints(falseBranch);
1546 constraintList_free(temp);
1549 temp = falseBranch->requiresConstraints;
1550 falseBranch->requiresConstraints = exprNode_traversRequiresConstraints(falseBranch);
1551 constraintList_free(temp);
1553 temp = falseBranch->trueEnsuresConstraints;
1554 falseBranch->trueEnsuresConstraints = exprNode_traversTrueEnsuresConstraints(falseBranch);
1555 constraintList_free(temp);
1557 temp = falseBranch->falseEnsuresConstraints;
1558 falseBranch->falseEnsuresConstraints = exprNode_traversFalseEnsuresConstraints(falseBranch);
1559 constraintList_free(temp);
1561 /* if pred is true e equals true otherwise pred equals false */
1563 cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1564 trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
1566 cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1567 falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
1569 e = doIfElse (e, pred, trueBranch, falseBranch);
1574 t1 = exprData_getPairA (data);
1575 t2 = exprData_getPairB (data);
1576 /* we essiantially treat this like expr1; expr2
1577 of course sequencePoint isn't adjusted so this isn't completely accurate
1579 exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint);
1580 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1581 exprNode_mergeResolve (e, t1, t2);
1585 handledExprNode = FALSE;
1588 e->requiresConstraints = constraintList_preserveOrig (e->requiresConstraints);
1589 e->ensuresConstraints = constraintList_preserveOrig (e->ensuresConstraints);
1590 e->requiresConstraints = constraintList_addGeneratingExpr (e->requiresConstraints, e);
1592 e->ensuresConstraints = constraintList_addGeneratingExpr (e->ensuresConstraints, e);
1595 e->requiresConstraints = constraintList_removeSurpressed(e->requiresConstraints);
1597 DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints))));
1599 DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->ensuresConstraints))));
1601 DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->trueEnsuresConstraints))));
1603 DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_printDetailed(e->falseEnsuresConstraints))));
1609 constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
1613 bool handledExprNode;
1617 if (exprNode_handleError (e))
1619 ret = constraintList_makeNew();
1623 ret = constraintList_copy (e->trueEnsuresConstraints);
1625 handledExprNode = TRUE;
1632 t1 = exprData_getSingle (data);
1633 ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints (t1));
1638 ret = constraintList_addListFree (ret,
1639 exprNode_traversTrueEnsuresConstraints
1640 (exprData_getPairA (data)));
1642 ret = constraintList_addListFree (ret,
1643 exprNode_traversTrueEnsuresConstraints
1644 (exprData_getPairB (data)));
1648 ret = constraintList_addListFree (ret,
1649 exprNode_traversTrueEnsuresConstraints
1650 (exprData_getUopNode (data)));
1654 ret = constraintList_addListFree (ret, exprNode_traversTrueEnsuresConstraints
1655 (exprData_getUopNode (data)));
1659 ret = constraintList_addListFree (ret,
1660 exprNode_traversTrueEnsuresConstraints
1661 (exprData_getInitNode (data)));
1666 ret = constraintList_addListFree (ret,
1667 exprNode_traversTrueEnsuresConstraints
1668 (exprData_getOpA (data)));
1670 ret = constraintList_addListFree (ret,
1671 exprNode_traversTrueEnsuresConstraints
1672 (exprData_getOpB (data)));
1675 ret = constraintList_addListFree (ret,
1676 exprNode_traversTrueEnsuresConstraints
1677 (exprData_getOpA (data)));
1679 ret = constraintList_addListFree (ret,
1680 exprNode_traversTrueEnsuresConstraints
1681 (exprData_getOpB (data)));
1688 ret = constraintList_addListFree (ret,
1689 exprNode_traversTrueEnsuresConstraints
1690 (exprData_getSingle (data)));
1694 ret = constraintList_addListFree (ret,
1695 exprNode_traversTrueEnsuresConstraints
1696 (exprData_getFcn (data)));
1697 /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
1701 ret = constraintList_addListFree (ret,
1702 exprNode_traversTrueEnsuresConstraints
1703 (exprData_getSingle (data)));
1706 case XPR_NULLRETURN:
1710 ret = constraintList_addListFree (ret,
1711 exprNode_traversTrueEnsuresConstraints
1712 (exprData_getFieldNode (data)));
1716 ret = constraintList_addListFree (ret,
1717 exprNode_traversTrueEnsuresConstraints
1718 (exprData_getFieldNode (data)));
1721 case XPR_STRINGLITERAL:
1728 ret = constraintList_addListFree (ret,
1729 exprNode_traversTrueEnsuresConstraints
1730 (exprData_getUopNode (data)));
1735 ret = constraintList_addListFree (ret,
1736 exprNode_traversTrueEnsuresConstraints
1737 (exprData_getCastNode (data)));
1747 constraintList exprNode_traversFalseEnsuresConstraints (exprNode e)
1750 bool handledExprNode;
1754 if (exprNode_handleError (e))
1756 ret = constraintList_makeNew();
1760 ret = constraintList_copy (e->falseEnsuresConstraints);
1761 handledExprNode = TRUE;
1767 t1 = exprData_getSingle (data);
1768 ret = constraintList_addListFree (ret,exprNode_traversFalseEnsuresConstraints (t1));
1773 ret = constraintList_addListFree (ret,
1774 exprNode_traversFalseEnsuresConstraints
1775 (exprData_getPairA (data)));
1777 ret = constraintList_addListFree (ret,
1778 exprNode_traversFalseEnsuresConstraints
1779 (exprData_getPairB (data)));
1783 ret = constraintList_addListFree (ret,
1784 exprNode_traversFalseEnsuresConstraints
1785 (exprData_getUopNode (data)));
1789 ret = constraintList_addListFree (ret, exprNode_traversFalseEnsuresConstraints
1790 (exprData_getUopNode (data)));
1793 ret = constraintList_addListFree (ret,
1794 exprNode_traversFalseEnsuresConstraints
1795 ( exprData_getInitNode (data)));
1799 ret = constraintList_addListFree (ret,
1800 exprNode_traversFalseEnsuresConstraints
1801 (exprData_getOpA (data)));
1803 ret = constraintList_addListFree (ret,
1804 exprNode_traversFalseEnsuresConstraints
1805 (exprData_getOpB (data)));
1808 ret = constraintList_addListFree (ret,
1809 exprNode_traversFalseEnsuresConstraints
1810 (exprData_getOpA (data)));
1812 ret = constraintList_addListFree (ret,
1813 exprNode_traversFalseEnsuresConstraints
1814 (exprData_getOpB (data)));
1821 ret = constraintList_addListFree (ret,
1822 exprNode_traversFalseEnsuresConstraints
1823 (exprData_getSingle (data)));
1827 ret = constraintList_addListFree (ret,
1828 exprNode_traversFalseEnsuresConstraints
1829 (exprData_getFcn (data)));
1830 /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
1834 ret = constraintList_addListFree (ret,
1835 exprNode_traversFalseEnsuresConstraints
1836 (exprData_getSingle (data)));
1839 case XPR_NULLRETURN:
1843 ret = constraintList_addListFree (ret,
1844 exprNode_traversFalseEnsuresConstraints
1845 (exprData_getFieldNode (data)));
1849 ret = constraintList_addListFree (ret,
1850 exprNode_traversFalseEnsuresConstraints
1851 (exprData_getFieldNode (data)));
1854 case XPR_STRINGLITERAL:
1861 ret = constraintList_addListFree (ret,
1862 exprNode_traversFalseEnsuresConstraints
1863 (exprData_getUopNode (data)));
1868 ret = constraintList_addListFree (ret,
1869 exprNode_traversFalseEnsuresConstraints
1870 (exprData_getCastNode (data)));
1881 /* walk down the tree and get all requires Constraints in each subexpression*/
1882 /*@only@*/ constraintList exprNode_traversRequiresConstraints (exprNode e)
1886 bool handledExprNode;
1890 if (exprNode_handleError (e))
1892 ret = constraintList_makeNew();
1896 ret = constraintList_copy (e->requiresConstraints);
1897 handledExprNode = TRUE;
1903 t1 = exprData_getSingle (data);
1904 ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints (t1));
1909 ret = constraintList_addListFree (ret,
1910 exprNode_traversRequiresConstraints
1911 (exprData_getPairA (data)));
1913 ret = constraintList_addListFree (ret,
1914 exprNode_traversRequiresConstraints
1915 (exprData_getPairB (data)));
1919 ret = constraintList_addListFree (ret,
1920 exprNode_traversRequiresConstraints
1921 (exprData_getUopNode (data)));
1925 ret = constraintList_addListFree (ret, exprNode_traversRequiresConstraints
1926 (exprData_getUopNode (data)));
1929 ret = constraintList_addListFree (ret,
1930 exprNode_traversRequiresConstraints
1931 (exprData_getInitNode (data)));
1935 ret = constraintList_addListFree (ret,
1936 exprNode_traversRequiresConstraints
1937 (exprData_getOpA (data)));
1939 ret = constraintList_addListFree (ret,
1940 exprNode_traversRequiresConstraints
1941 (exprData_getOpB (data)));
1944 ret = constraintList_addListFree (ret,
1945 exprNode_traversRequiresConstraints
1946 (exprData_getOpA (data)));
1948 ret = constraintList_addListFree (ret,
1949 exprNode_traversRequiresConstraints
1950 (exprData_getOpB (data)));
1957 ret = constraintList_addListFree (ret,
1958 exprNode_traversRequiresConstraints
1959 (exprData_getSingle (data)));
1963 ret = constraintList_addListFree (ret,
1964 exprNode_traversRequiresConstraints
1965 (exprData_getFcn (data)));
1966 /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
1970 ret = constraintList_addListFree (ret,
1971 exprNode_traversRequiresConstraints
1972 (exprData_getSingle (data)));
1975 case XPR_NULLRETURN:
1979 ret = constraintList_addListFree (ret,
1980 exprNode_traversRequiresConstraints
1981 (exprData_getFieldNode (data)));
1985 ret = constraintList_addListFree (ret,
1986 exprNode_traversRequiresConstraints
1987 (exprData_getFieldNode (data)));
1990 case XPR_STRINGLITERAL:
1997 ret = constraintList_addListFree (ret,
1998 exprNode_traversRequiresConstraints
1999 (exprData_getUopNode (data)));
2004 ret = constraintList_addListFree (ret,
2005 exprNode_traversRequiresConstraints
2006 (exprData_getCastNode (data)));
2017 /* walk down the tree and get all Ensures Constraints in each subexpression*/
2018 /*@only@*/ constraintList exprNode_traversEnsuresConstraints (exprNode e)
2022 bool handledExprNode;
2026 if (exprNode_handleError (e))
2028 ret = constraintList_makeNew();
2032 ret = constraintList_copy (e->ensuresConstraints);
2033 handledExprNode = TRUE;
2037 DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with "
2038 "constraintList of %s",
2039 exprNode_unparse (e),
2040 constraintList_print(e->ensuresConstraints)
2048 t1 = exprData_getSingle (data);
2049 ret = constraintList_addListFree (ret,exprNode_traversEnsuresConstraints (t1));
2053 ret = constraintList_addListFree (ret,
2054 exprNode_traversEnsuresConstraints
2055 (exprData_getPairA (data)));
2057 ret = constraintList_addListFree (ret,
2058 exprNode_traversEnsuresConstraints
2059 (exprData_getPairB (data)));
2062 ret = constraintList_addListFree (ret,
2063 exprNode_traversEnsuresConstraints
2064 (exprData_getUopNode (data)));
2068 ret = constraintList_addListFree (ret, exprNode_traversEnsuresConstraints
2069 (exprData_getUopNode (data)));
2073 ret = constraintList_addListFree (ret,
2074 exprNode_traversEnsuresConstraints
2075 (exprData_getInitNode (data)));
2080 ret = constraintList_addListFree (ret,
2081 exprNode_traversEnsuresConstraints
2082 (exprData_getOpA (data)));
2084 ret = constraintList_addListFree (ret,
2085 exprNode_traversEnsuresConstraints
2086 (exprData_getOpB (data)));
2089 ret = constraintList_addListFree (ret,
2090 exprNode_traversEnsuresConstraints
2091 (exprData_getOpA (data)));
2093 ret = constraintList_addListFree (ret,
2094 exprNode_traversEnsuresConstraints
2095 (exprData_getOpB (data)));
2101 ret = constraintList_addListFree (ret,
2102 exprNode_traversEnsuresConstraints
2103 (exprData_getSingle (data)));
2106 ret = constraintList_addListFree (ret,
2107 exprNode_traversEnsuresConstraints
2108 (exprData_getFcn (data)));
2109 /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
2112 ret = constraintList_addListFree (ret,
2113 exprNode_traversEnsuresConstraints
2114 (exprData_getSingle (data)));
2116 case XPR_NULLRETURN:
2119 ret = constraintList_addListFree (ret,
2120 exprNode_traversEnsuresConstraints
2121 (exprData_getFieldNode (data)));
2124 ret = constraintList_addListFree (ret,
2125 exprNode_traversEnsuresConstraints
2126 (exprData_getFieldNode (data)));
2128 case XPR_STRINGLITERAL:
2133 ret = constraintList_addListFree (ret,
2134 exprNode_traversEnsuresConstraints
2135 (exprData_getUopNode (data)));
2138 ret = constraintList_addListFree (ret,
2139 exprNode_traversEnsuresConstraints
2140 (exprData_getCastNode (data)));
2146 DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with "
2147 "constraintList of is returning %s",
2148 exprNode_unparse (e),
2149 constraintList_print(ret))));
2154 /*drl moved out of constraintResolve.c 07-02-001 */
2155 void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist,
2156 fileloc sequencePoint)
2159 llassert(temp != NULL );
2161 temp->requiresConstraints = constraintList_makeNew();
2162 temp->ensuresConstraints = constraintList_makeNew();
2163 temp->trueEnsuresConstraints = constraintList_makeNew();
2164 temp->falseEnsuresConstraints = constraintList_makeNew();
2166 exprNodeList_elements (arglist, el)
2168 constraintList temp2;
2170 llassert(exprNode_isDefined(el) );
2172 exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
2173 temp2 = el->requiresConstraints;
2174 el->requiresConstraints = exprNode_traversRequiresConstraints(el);
2175 constraintList_free(temp2);
2177 temp2 = el->ensuresConstraints;
2178 el->ensuresConstraints = exprNode_traversEnsuresConstraints(el);
2179 constraintList_free(temp2);
2181 temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
2182 el->requiresConstraints);
2184 temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
2185 el->ensuresConstraints);
2187 end_exprNodeList_elements;
2191 /*drl moved out of constraintResolve.c 07-03-001 */
2192 constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
2194 constraintList postconditions;
2196 DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist))));
2198 temp = exprNode_getUentry (fcn);
2200 postconditions = uentry_getFcnPostconditions (temp);
2202 if (constraintList_isDefined (postconditions))
2204 postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
2205 postconditions = constraintList_doFixResult (postconditions, fcnCall);
2209 postconditions = constraintList_makeNew();
2212 return postconditions;
2216 comment this out for now
2217 we'll include it in a production release when its stable...
2219 void findStructs (exprNodeList arglist)
2225 message("doing findStructs: %s", exprNodeList_unparse(arglist))
2229 exprNodeList_elements(arglist, expr)
2231 ct = exprNode_getType(expr);
2233 rt = ctype_realType (ct);
2235 if (ctype_isStruct (rt))
2236 TPRINTF((message("Found structure %s", exprNode_unparse(expr))
2238 if (hasInvariants(ct))
2240 constraintList invars;
2242 invars = getInvariants(ct);
2245 TPRINTF((message ("findStructs has invariants %s ", constraintList_print (invars))
2248 invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct);
2251 TPRINTF((message ("findStructs finded invariants to be %s ", constraintList_print (invars))
2255 end_exprNodeList_elements;
2260 /*drl moved out of constraintResolve.c 07-02-001 */
2261 constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
2263 constraintList preconditions;
2265 DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist))));
2267 temp = exprNode_getUentry (fcn);
2269 preconditions = uentry_getFcnPreconditions (temp);
2271 if (constraintList_isDefined(preconditions))
2273 preconditions = constraintList_togglePost (preconditions);
2274 preconditions = constraintList_preserveCallInfo(preconditions, fcn);
2275 preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
2279 if (constraintList_isUndefined(preconditions))
2280 preconditions = constraintList_makeNew();
2283 if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
2287 uentryList_elements (arglist, el)
2290 TPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) ));
2292 s = uentry_getSref(el);
2293 if (sRef_isReference (s) )
2295 TPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
2299 TPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
2302 //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0
2303 c = constraint_makeSRefWriteSafeInt (s, 0);
2305 implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
2307 //drl 10/23/2002 added support for out
2308 if (!uentry_isOut(el) )
2310 c = constraint_makeSRefReadSafeInt (s, 0);
2311 implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
2319 DPRINTF ((message("Done checkCall\n")));
2320 DPRINTF ((message("Returning list %q ", constraintList_printDetailed(preconditions))));
2323 drl we're going to comment this out for now
2324 we'll include it if we're sure it's working
2326 findStructs(arglist);
2329 return preconditions;
2332 /*drl added this function 10.29.001
2333 takes an exprNode of the form const + const
2337 I'm a bit nervous about modifying the exprNode
2338 but this is the easy way to do this
2339 If I have time I'd like to cause the exprNode to get created correctly in the first place */
2341 void exprNode_findValue(exprNode e)
2348 llassert(exprNode_isDefined(e) );
2352 if (exprNode_hasValue(e))
2355 if (e->kind == XPR_OP)
2357 t1 = exprData_getOpA (data);
2358 t2 = exprData_getOpB (data);
2359 tok = exprData_getOpTok (data);
2361 exprNode_findValue(t1);
2362 exprNode_findValue(t2);
2364 if (!(exprNode_knownIntValue(t1) && (exprNode_knownIntValue(t2))))
2367 if (lltok_isPlus_Op (tok))
2371 v1 = exprNode_getLongValue(t1);
2372 v2 = exprNode_getLongValue(t2);
2374 if (multiVal_isDefined(e->val))
2375 multiVal_free (e->val);
2377 e->val = multiVal_makeInt (v1 + v2);
2380 if (lltok_isMinus_Op (tok))
2384 v1 = exprNode_getLongValue(t1);
2385 v2 = exprNode_getLongValue(t2);
2387 if (multiVal_isDefined(e->val))
2389 multiVal_free (e->val);
2392 e->val = multiVal_makeInt (v1 - v2);
2395 /*drl I should really do * and / at some point */