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_traverseTrueEnsuresConstraints (/*@temp@*/ exprNode p_e);
52 static constraintList exprNode_traverseFalseEnsuresConstraints (/*@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 Analyzing %s at %s", exprNode_unparse(e),
121 fileloc_unparse(exprNode_loc (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",
150 constraintList_unparseDetailed (e->requiresConstraints))));
154 static void exprNode_stmt (/*@temp@*/ exprNode e)
159 DPRINTF (("Generating constraint for: %s", exprNode_unparse (e)));
161 if (exprNode_isError(e))
166 /*e->requiresConstraints = constraintList_makeNew();
167 e->ensuresConstraints = constraintList_makeNew(); */
169 /*!! s = exprNode_unparse (e); */
171 if (e->kind == XPR_INIT)
173 constraintList tempList;
174 DPRINTF (("Init: %s ", exprNode_unparse (e)));
175 loc = exprNode_getNextSequencePoint (e); /* reduces to an expression */
176 DPRINTF (("Location: %s", fileloc_unparse (loc)));
177 DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints)));
178 exprNode_exprTraverse (e, FALSE, FALSE, loc);
179 DPRINTF (("Ensures after: %s", constraintList_unparse (e->ensuresConstraints)));
180 DPRINTF (("After traversing..."));
183 tempList = e->requiresConstraints;
184 DPRINTF (("Requires before: %s", constraintList_unparse (e->requiresConstraints)));
185 e->requiresConstraints = exprNode_traverseRequiresConstraints (e);
186 DPRINTF (("Requires after: %s", constraintList_unparse (e->requiresConstraints)));
187 constraintList_free(tempList);
189 tempList = e->ensuresConstraints;
190 DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints)));
191 e->ensuresConstraints = exprNode_traverseEnsuresConstraints(e);
192 DPRINTF (("Ensures before: %s", constraintList_unparse (e->ensuresConstraints)));
193 constraintList_free(tempList);
197 /*drl 2/13/002 patched bug so return statement will be checked*/
198 /*return is a stmt not not expression ...*/
199 if (e->kind == XPR_RETURN)
201 constraintList tempList;
203 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
205 exprNode_exprTraverse (exprData_getSingle (e->edata), FALSE, TRUE, loc);
208 tempList = e->requiresConstraints;
209 e->requiresConstraints = exprNode_traverseRequiresConstraints(e);
210 constraintList_free(tempList);
213 if (e->kind != XPR_STMT)
215 DPRINTF (("Not Stmt"));
216 DPRINTF ((message ("%s ", exprNode_unparse (e))));
218 if (exprNode_isMultiStatement (e))
220 exprNode_multiStatement (e); /* evans 2001-08-21: spurious return removed */
224 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
226 exprNode_exprTraverse (e, FALSE, TRUE, loc);
234 DPRINTF ((message ("%s ", exprNode_unparse (e))));
236 snode = exprData_getUopNode (e->edata);
238 /* could be stmt involving multiple statements:
239 i.e. if, while for ect.
242 if (exprNode_isMultiStatement (snode))
244 exprNode_multiStatement (snode);
245 (void) exprNode_copyConstraints (e, snode);
249 loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
250 exprNode_exprTraverse (snode, FALSE, FALSE, loc);
254 constraintList_free (e->requiresConstraints);
255 e->requiresConstraints = exprNode_traverseRequiresConstraints(snode);
257 constraintList_free (e->ensuresConstraints);
258 e->ensuresConstraints = exprNode_traverseEnsuresConstraints(snode);
260 DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
261 constraintList_unparse(e->requiresConstraints),
262 constraintList_unparse(e->ensuresConstraints))));
267 static void exprNode_stmtList (/*@dependent@*/ exprNode e)
269 exprNode stmt1, stmt2;
270 if (exprNode_isError (e))
276 Handle case of stmtList with only one statement:
277 The parse tree stores this as stmt instead of stmtList
280 if (e->kind != XPR_STMTLIST)
285 llassert (e->kind == XPR_STMTLIST);
286 DPRINTF(("exprNode_stmtList STMTLIST:"));
287 DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e))));
288 stmt1 = exprData_getPairA (e->edata);
289 stmt2 = exprData_getPairB (e->edata);
292 DPRINTF(("exprNode_stmtlist "));
293 DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2))));
295 exprNode_stmt (stmt1);
296 DPRINTF(("\nstmt after stmtList call "));
298 exprNode_stmt (stmt2);
299 exprNode_mergeResolve (e, stmt1, stmt2);
301 DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
302 constraintList_unparse(e->requiresConstraints),
303 constraintList_unparse(e->ensuresConstraints))));
307 static exprNode doIf (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
311 DPRINTF ((message ("doIf: %s ", exprNode_unparse(e))));
313 llassert (exprNode_isDefined(test));
314 llassert (exprNode_isDefined (e));
315 llassert (exprNode_isDefined (body));
317 DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
319 DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->ensuresConstraints))));
321 DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->trueEnsuresConstraints))));
323 DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e), constraintList_unparseDetailed(e->falseEnsuresConstraints))));
327 DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->ensuresConstraints))));
329 DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->ensuresConstraints))));
331 DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->trueEnsuresConstraints))));
333 DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test), constraintList_unparseDetailed(test->falseEnsuresConstraints))));
337 temp = test->trueEnsuresConstraints;
338 test->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(test);
339 constraintList_free(temp);
341 temp = test->ensuresConstraints;
342 test->ensuresConstraints = exprNode_traverseEnsuresConstraints (test);
343 constraintList_free(temp);
345 temp = test->requiresConstraints;
346 test->requiresConstraints = exprNode_traverseRequiresConstraints (test);
347 constraintList_free(temp);
350 test->trueEnsuresConstraints = constraintList_substituteFreeTarget(test->trueEnsuresConstraints, test->ensuresConstraints);
352 DPRINTF ((message ("doIf: test ensures %s ", constraintList_unparse(test->ensuresConstraints))));
354 DPRINTF ((message ("doIf: test true ensures %s ", constraintList_unparse(test->trueEnsuresConstraints))));
356 constraintList_free(e->requiresConstraints);
359 e->requiresConstraints = constraintList_reflectChanges(body->requiresConstraints, test->trueEnsuresConstraints);
361 e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints,
362 test->ensuresConstraints);
363 temp = e->requiresConstraints;
364 e->requiresConstraints = constraintList_mergeRequires (e->requiresConstraints, test->requiresConstraints);
365 constraintList_free(temp);
368 /* drl possible problem : warning bad */
369 constraintList_free(e->ensuresConstraints);
370 e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
372 if (exprNode_mayEscape (body))
374 DPRINTF ((message("doIf: the if statement body %s returns or exits", exprNode_unparse(body))));
375 e->ensuresConstraints = constraintList_mergeEnsuresFreeFirst (e->ensuresConstraints,
376 test->falseEnsuresConstraints);
379 DPRINTF ((message ("doIf: if requiers %s ", constraintList_unparse(e->requiresConstraints))));
385 Also used for condition i.e. ?: operation
388 This function assumes that p, trueBranch, falseBranch have have all been traversed
389 for constraints i.e. we assume that exprNode_traverseEnsuresConstraints,
390 exprNode_traverseRequiresConstraints, exprNode_traverseTrueEnsuresConstraints,
391 exprNode_traverseFalseEnsuresConstraints have all been run
394 static exprNode doIfElse (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode p, /*@dependent@*/ exprNode trueBranch, /*@dependent@*/ exprNode falseBranch)
396 constraintList c1, cons, t, t2, f, f2;
398 llassert (exprNode_isDefined (e));
399 llassert (exprNode_isDefined (p));
400 llassert (exprNode_isDefined (trueBranch));
401 llassert (exprNode_isDefined (falseBranch));
402 DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e))));
404 /* do requires clauses */
405 c1 = constraintList_copy (p->ensuresConstraints);
407 t = constraintList_reflectChanges(trueBranch->requiresConstraints, p->trueEnsuresConstraints);
408 t = constraintList_reflectChangesFreePre (t, p->ensuresConstraints);
410 cons = constraintList_reflectChanges(falseBranch->requiresConstraints, p->falseEnsuresConstraints);
411 cons = constraintList_reflectChangesFreePre (cons, c1);
413 constraintList_free (e->requiresConstraints);
414 e->requiresConstraints = constraintList_mergeRequiresFreeFirst (t, cons);
415 e->requiresConstraints = constraintList_mergeRequiresFreeFirst (e->requiresConstraints, p->requiresConstraints);
417 /* do ensures clauses
418 find the the ensures lists for each subbranch
421 t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
423 t = constraintList_mergeEnsures (p->ensuresConstraints, t);
424 constraintList_free(t2);
426 f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
428 f = constraintList_mergeEnsures (p->ensuresConstraints, f);
429 constraintList_free(f2);
431 /* find ensures for whole if/else statement */
433 constraintList_free(e->ensuresConstraints);
435 e->ensuresConstraints = constraintList_logicalOr (t, f);
437 constraintList_free(t);
438 constraintList_free(f);
439 constraintList_free(cons);
440 constraintList_free(c1);
442 DPRINTF ((message ("doIfElse: if requires %q ", constraintList_unparse(e->requiresConstraints))));
443 DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_unparse(e->ensuresConstraints))));
448 static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode test, /*@dependent@*/ exprNode body)
450 DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e))));
451 return doIf (e, test, body);
454 /*@only@*/ constraintList constraintList_makeFixedArrayConstraints (/*@observer@*/ sRefSet s)
458 ret = constraintList_makeNew();
460 sRefSet_elements (s, el)
462 if (sRef_isFixedArray(el))
465 DPRINTF((message("%s is a fixed array",
467 size = sRef_getArraySize(el);
468 DPRINTF((message("%s is a fixed array with size %d",
469 sRef_unparse(el), (int)size)));
470 con = constraint_makeSRefSetBufferSize (el, size_toLong (size - 1));
471 ret = constraintList_add(ret, con);
475 DPRINTF((message("%s is not a fixed array",
479 if (sRef_isExternallyVisible (el))
482 DPRINTF((message("%s is externally visible",
484 con = constraint_makeSRefWriteSafeInt(el, 0);
485 ret = constraintList_add(ret, con);
487 con = constraint_makeSRefReadSafeInt(el, 0);
489 ret = constraintList_add(ret, con);
494 end_sRefSet_elements ;
496 DPRINTF((message("constraintList_makeFixedArrayConstraints returning %s",
497 constraintList_unparse(ret))));
502 exprNode makeDataTypeConstraints (/*@returned@*/ exprNode e)
505 DPRINTF(("makeDataTypeConstraints"));
507 c = constraintList_makeFixedArrayConstraints (e->uses);
509 e->ensuresConstraints = constraintList_addListFree (e->ensuresConstraints, c);
515 static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred, /*@dependent@*/ exprNode forBody)
517 exprNode init, test, inc;
518 /* merge the constraints: modle as if statement */
525 llassert (exprNode_isDefined (e));
526 llassert (exprNode_isDefined (forPred));
527 llassert (exprNode_isDefined (forBody));
529 init = exprData_getTripleInit (forPred->edata);
530 test = exprData_getTripleTest (forPred->edata);
531 inc = exprData_getTripleInc (forPred->edata);
533 if (((exprNode_isError (test) /*|| (exprNode_isError(init))*/) || (exprNode_isError (inc))))
535 DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e))));
539 exprNode_forLoopHeuristics(e, forPred, forBody);
541 constraintList_free(e->requiresConstraints);
542 e->requiresConstraints = constraintList_reflectChanges(forBody->requiresConstraints, test->ensuresConstraints);
543 e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, test->trueEnsuresConstraints);
544 e->requiresConstraints = constraintList_reflectChangesFreePre (e->requiresConstraints, forPred->ensuresConstraints);
546 if (!forBody->canBreak)
548 e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints, constraintList_copy(forPred->ensuresConstraints));
549 e->ensuresConstraints = constraintList_addListFree(e->ensuresConstraints,constraintList_copy(test->falseEnsuresConstraints));
553 DPRINTF(("Can break"));
557 static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/ exprNode e)
559 /* !!! DRL - this is ridiculous! Read the manual on memory annotations please! */
564 exprNode_doGenerateConstraintSwitch
565 (/*@dependent@*/ exprNode switchExpr,
566 /*@dependent@*/ exprNode body,
567 /*@special@*/ constraintList *currentRequires,
568 /*@special@*/ constraintList *currentEnsures,
569 /*@special@*/ constraintList *savedRequires,
570 /*@special@*/ constraintList *savedEnsures)
571 /*@post:only *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/
572 /*@sets *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/
574 exprNode stmt, stmtList;
576 DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s",
577 exprNode_unparse(switchExpr), exprNode_unparse(body)
580 if (exprNode_isError(body))
582 *currentRequires = constraintList_makeNew ();
583 *currentEnsures = constraintList_makeNew ();
585 *savedRequires = constraintList_makeNew ();
586 *savedEnsures = constraintList_makeNew ();
592 if (body->kind != XPR_STMTLIST)
594 DPRINTF((message("exprNode_doGenerateConstraintSwitch: non stmtlist: %s",
595 exprNode_unparse(body))));
597 stmtList = exprNode_undefined;
598 stmt = exprNode_makeDependent(stmt);
599 stmtList = exprNode_makeDependent(stmtList);
603 stmt = exprData_getPairB(body->edata);
604 stmtList = exprData_getPairA(body->edata);
605 stmt = exprNode_makeDependent(stmt);
606 stmtList = exprNode_makeDependent(stmtList);
609 DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s stmt: %s",
610 exprNode_unparse(stmtList), exprNode_unparse(stmt))
614 exprNode_doGenerateConstraintSwitch (switchExpr, stmtList, currentRequires, currentEnsures,
615 savedRequires, savedEnsures);
617 if (exprNode_isError(stmt))
624 switchExpr = exprNode_makeDependent (switchExpr);
626 if (! exprNode_isCaseMarker(stmt))
631 DPRINTF ((message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt),
632 constraintList_unparse(stmt->requiresConstraints), constraintList_unparse(stmt->ensuresConstraints))));
634 temp = constraintList_reflectChanges (stmt->requiresConstraints,
637 *currentRequires = constraintList_mergeRequiresFreeFirst(
641 constraintList_free(temp);
643 *currentEnsures = constraintList_mergeEnsuresFreeFirst
645 stmt->ensuresConstraints);
646 DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
647 "%s currentEnsures:%s",
648 exprNode_unparse(switchExpr), exprNode_unparse(body),
649 constraintList_unparse(*currentRequires), constraintList_unparse(*currentEnsures)
657 if (exprNode_isCaseMarker(stmt) && exprNode_mustEscape(stmtList))
660 ** merge current and saved constraint with Logical Or...
661 ** make a constraint for ensures
667 DPRINTF ((message("Got case marker")));
669 if (constraintList_isUndefined(*savedEnsures) &&
670 constraintList_isUndefined(*savedRequires))
672 llassert(constraintList_isUndefined(*savedEnsures));
673 llassert(constraintList_isUndefined(*savedRequires));
674 *savedEnsures = constraintList_copy(*currentEnsures);
675 *savedRequires = constraintList_copy(*currentRequires);
679 DPRINTF ((message("Doing logical or")));
680 temp = constraintList_logicalOr (*savedEnsures, *currentEnsures);
681 constraintList_free (*savedEnsures);
682 *savedEnsures = temp;
684 *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires);
687 con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle (stmt->edata), exprNode_loc (stmt));
689 constraintList_free (*currentEnsures);
690 *currentEnsures = constraintList_makeNew();
691 *currentEnsures = constraintList_add(*currentEnsures, con);
693 constraintList_free(*currentRequires);
694 *currentRequires = constraintList_makeNew();
695 DPRINTF (("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
696 "%s savedEnsures:%s",
697 exprNode_unparse(switchExpr), exprNode_unparse(body),
698 constraintList_unparse(*savedRequires), constraintList_unparse(*savedEnsures)
701 else if (exprNode_isCaseMarker(stmt)) /* 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
711 constraintList ensuresTemp;
713 con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle (stmt->edata), exprNode_loc (stmt));
715 ensuresTemp = constraintList_makeNew ();
716 ensuresTemp = constraintList_add (ensuresTemp, con);
718 if (exprNode_isError (stmtList))
720 constraintList_free (*currentEnsures);
721 *currentEnsures = constraintList_copy (ensuresTemp);
722 constraintList_free (ensuresTemp);
726 temp = constraintList_logicalOr (*currentEnsures, ensuresTemp);
727 constraintList_free (*currentEnsures);
728 constraintList_free (ensuresTemp);
729 *currentEnsures = temp;
732 constraintList_free (*currentRequires);
733 *currentRequires = constraintList_makeNew();
738 we handle the case of ! exprNode_isCaseMarker above
739 the else if clause should always be true.
744 DPRINTF (("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
745 "%s currentEnsures:%s",
746 exprNode_unparse(switchExpr), exprNode_unparse(body),
747 constraintList_unparse(*currentRequires), constraintList_unparse(*currentEnsures)
756 static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt)
758 constraintList constraintsRequires;
759 constraintList constraintsEnsures;
760 constraintList lastRequires;
761 constraintList lastEnsures;
766 switchExpr = exprData_getPairA (switchStmt->edata);
767 body = exprData_getPairB (switchStmt->edata);
769 if (!exprNode_isDefined (body))
774 DPRINTF((message("")));
776 if (body->kind == XPR_BLOCK)
777 body = exprData_getSingle(body->edata);
780 constraintsRequires = constraintList_undefined;
781 constraintsEnsures = constraintList_undefined;
783 lastRequires = constraintList_makeNew();
784 lastEnsures = constraintList_makeNew();
788 /* evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
789 exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires,
790 &lastEnsures, &constraintsRequires, &constraintsEnsures);
794 merge current and saved constraint with Logical Or...
795 make a constraint for ensures
798 constraintList_free(switchStmt->requiresConstraints);
799 constraintList_free(switchStmt->ensuresConstraints);
801 if (constraintList_isDefined(constraintsEnsures) && constraintList_isDefined(constraintsRequires))
803 switchStmt->ensuresConstraints = constraintList_logicalOr(constraintsEnsures, lastEnsures);
804 switchStmt->requiresConstraints = constraintList_mergeRequires(constraintsRequires, lastRequires);
805 constraintList_free (constraintsRequires);
806 constraintList_free (constraintsEnsures);
810 switchStmt->ensuresConstraints = constraintList_copy(lastEnsures);
811 switchStmt->requiresConstraints = constraintList_copy(lastRequires);
814 constraintList_free (lastRequires);
815 constraintList_free (lastEnsures);
817 DPRINTF(((message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s",
818 constraintList_unparse(switchStmt->requiresConstraints),
819 constraintList_unparse(switchStmt->ensuresConstraints)
824 static exprNode doSwitch (/*@returned@*/ /*@notnull@*/ exprNode e)
830 DPRINTF ((message ("doSwitch for: switch (%s) %s",
831 exprNode_unparse (exprData_getPairA (data)),
832 exprNode_unparse (exprData_getPairB (data)))));
834 body = exprData_getPairB (data);
835 exprNode_generateConstraintSwitch (e);
839 void exprNode_multiStatement (/*@dependent@*/ exprNode e)
845 exprNode p, trueBranch, falseBranch;
846 exprNode forPred, forBody;
851 DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e),
852 fileloc_unparse(exprNode_getfileloc(e)))));
854 if (exprNode_handleError (e))
867 forPred = exprData_getPairA (data);
868 forBody = exprData_getPairB (data);
870 /* First generate the constraints */
871 exprNode_generateConstraints (forPred);
872 exprNode_generateConstraints (forBody);
875 doFor (e, forPred, forBody);
880 exprNode_generateConstraints (exprData_getTripleInit (data));
881 test = exprData_getTripleTest (data);
882 exprNode_exprTraverse (test,FALSE, FALSE, exprNode_loc(e));
883 exprNode_generateConstraints (exprData_getTripleInc (data));
885 if (!exprNode_isError(test))
887 constraintList temp2;
888 temp2 = test->trueEnsuresConstraints;
889 test->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(test);
890 constraintList_free(temp2);
893 exprNode_generateConstraints (exprData_getTripleInc (data));
897 e1 = exprData_getPairA (data);
898 e2 = exprData_getPairB (data);
900 exprNode_exprTraverse (e1,
901 FALSE, FALSE, exprNode_loc(e1));
903 exprNode_generateConstraints (e2);
905 e = doWhile (e, e1, e2);
911 DPRINTF ((exprNode_unparse(e)));
912 e1 = exprData_getPairA (data);
913 e2 = exprData_getPairB (data);
915 exprNode_exprTraverse (e1, FALSE, FALSE, exprNode_loc(e1));
917 exprNode_generateConstraints (e2);
918 e = doIf (e, e1, e2);
922 DPRINTF(("Starting IFELSE"));
923 p = exprData_getTriplePred (data);
925 trueBranch = exprData_getTripleTrue (data);
926 falseBranch = exprData_getTripleFalse (data);
928 exprNode_exprTraverse (p,
929 FALSE, FALSE, exprNode_loc(p));
930 exprNode_generateConstraints (trueBranch);
931 exprNode_generateConstraints (falseBranch);
933 llassert (exprNode_isDefined (p));
934 temp = p->ensuresConstraints;
935 p->ensuresConstraints = exprNode_traverseEnsuresConstraints (p);
936 constraintList_free(temp);
938 temp = p->requiresConstraints;
939 p->requiresConstraints = exprNode_traverseRequiresConstraints (p);
940 constraintList_free(temp);
942 temp = p->trueEnsuresConstraints;
943 p->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(p);
944 constraintList_free(temp);
948 DPRINTF((message("p->trueEnsuresConstraints before substitue %s", constraintList_unparse(p->trueEnsuresConstraints) )
951 /*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*/
953 p->trueEnsuresConstraints = constraintList_substituteFreeTarget (p->trueEnsuresConstraints,
954 p->ensuresConstraints);
956 DPRINTF(( message ("p->trueEnsuresConstraints after substitue %s", constraintList_unparse(p->trueEnsuresConstraints) )
959 temp = p->falseEnsuresConstraints;
960 p->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(p);
961 constraintList_free(temp);
963 /*See comment on trueEnsures*/
964 p->falseEnsuresConstraints = constraintList_substituteFreeTarget (p->falseEnsuresConstraints,
965 p->ensuresConstraints);
967 e = doIfElse (e, p, trueBranch, falseBranch);
968 DPRINTF(("Done IFELSE"));
973 e2 = (exprData_getPairB (data));
974 e1 = (exprData_getPairA (data));
976 DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2), exprNode_unparse(e1))));
977 exprNode_generateConstraints (e2);
978 exprNode_generateConstraints (e1);
979 e = exprNode_copyConstraints (e, e2);
980 DPRINTF ((message ("e = %s ", constraintList_unparse(e->requiresConstraints))));
988 tempExpr = exprData_getSingle (data);
990 exprNode_generateConstraints (tempExpr);
992 if (exprNode_isDefined(tempExpr) )
994 constraintList_free(e->requiresConstraints);
995 e->requiresConstraints = constraintList_copy (tempExpr->requiresConstraints);
996 constraintList_free(e->ensuresConstraints);
997 e->ensuresConstraints = constraintList_copy (tempExpr->ensuresConstraints);
1011 exprNode_stmtList (e);
1021 static bool lltok_isBoolean_Op (lltok tok)
1023 /*this should really be a switch statement but
1024 I don't want to violate the abstraction
1025 maybe this should go in lltok.c */
1027 if (lltok_isEqOp (tok))
1031 if (lltok_isAndOp (tok))
1037 if (lltok_isOrOp (tok))
1042 if (lltok_isGt_Op (tok))
1046 if (lltok_isLt_Op (tok))
1051 if (lltok_isLe_Op (tok))
1056 if (lltok_isGe_Op (tok))
1066 static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e, /*@unused@*/ bool definatelv, /*@unused@*/ bool definaterv, fileloc sequencePoint)
1072 constraintList tempList, temp;
1074 if (exprNode_isUndefined(e) )
1076 llassert (exprNode_isDefined(e) );
1082 tok = exprData_getOpTok (data);
1083 t1 = exprData_getOpA (data);
1084 t2 = exprData_getOpB (data);
1086 /* drl 3/2/2003 we know this because of the type of expression*/
1087 llassert( exprNode_isDefined(t1) && exprNode_isDefined(t2) );
1090 tempList = constraintList_undefined;
1092 /* arithmetic tests */
1094 if (lltok_isEqOp (tok))
1096 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
1097 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1101 if (lltok_isLt_Op (tok))
1103 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1104 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1105 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1106 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1109 if (lltok_isGe_Op (tok))
1111 cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
1112 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1114 cons = constraint_makeEnsureLessThan (t1, t2, sequencePoint);
1115 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1118 if (lltok_isGt_Op (tok))
1120 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1121 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1122 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1123 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1126 if (lltok_isLe_Op (tok))
1128 cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
1129 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1131 cons = constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
1132 e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
1135 /* Logical operations */
1137 if (lltok_isAndOp (tok))
1140 tempList = constraintList_copy (t1->trueEnsuresConstraints);
1141 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1142 e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1144 /* false ensures: fens t1 or tens t1 and fens t2 */
1145 tempList = constraintList_copy (t1->trueEnsuresConstraints);
1146 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1148 tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
1149 constraintList_free (temp);
1151 /* evans - was constraintList_addList - memory leak detected by splint */
1152 e->falseEnsuresConstraints = constraintList_addListFree (e->falseEnsuresConstraints, tempList);
1154 else if (lltok_isOrOp (tok))
1157 tempList = constraintList_copy (t1->falseEnsuresConstraints);
1158 tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
1159 e->falseEnsuresConstraints = constraintList_addListFree(e->falseEnsuresConstraints, tempList);
1161 /* true ensures: tens t1 or fens t1 and tens t2 */
1162 tempList = constraintList_copy (t1->falseEnsuresConstraints);
1163 tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
1166 tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
1167 constraintList_free(temp);
1169 e->trueEnsuresConstraints = constraintList_addListFree(e->trueEnsuresConstraints, tempList);
1170 tempList = constraintList_undefined;
1174 DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok))));
1178 void exprNode_exprTraverse (/*@dependent@*/ exprNode e,
1179 bool definatelv, bool definaterv,
1180 /*@observer@*/ /*@temp@*/ fileloc sequencePoint)
1182 exprNode t1, t2, fcn;
1186 constraintList temp;
1188 if (exprNode_isError(e))
1193 DPRINTF (("exprNode_exprTraverse analyzing %s at %s",
1194 exprNode_unparse (e),
1195 fileloc_unparse (exprNode_loc (e))));
1197 if (exprNode_isUnhandled (e))
1207 t1 = exprData_getSingle (data);
1208 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
1209 e = exprNode_copyConstraints (e, t1);
1216 t1 = (exprData_getPairA (data));
1217 t2 = (exprData_getPairB (data));
1218 cons = constraint_makeWriteSafeExprNode (t1, t2);
1222 t1 = (exprData_getPairA (data));
1223 t2 = (exprData_getPairB (data));
1224 cons = constraint_makeReadSafeExprNode (t1, t2);
1227 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1228 cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
1229 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1231 cons = constraint_makeEnsureLteMaxRead (t2, t1);
1232 e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
1234 exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
1235 exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
1240 exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
1244 t2 = exprData_getInitNode (data);
1246 DPRINTF (("initialization ==> %s",exprNode_unparse (t2)));
1248 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1250 /* This test is nessecary because some expressions generate a null expression node.
1251 function pointer do that -- drl */
1253 if (!exprNode_isError (e) && !exprNode_isError (t2))
1255 cons = constraint_makeEnsureEqual (e, t2, sequencePoint);
1256 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1262 t1 = exprData_getOpA (data);
1263 t2 = exprData_getOpB (data);
1264 DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints)));
1265 DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints)));
1266 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1267 DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints)));
1268 DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints)));
1269 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1270 DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1->ensuresConstraints)));
1271 DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2->ensuresConstraints)));
1273 /* this test is nessecary because some expressions generate a null expression node.
1274 function pointer do that -- drl */
1276 if ((!exprNode_isError (t1)) && (!exprNode_isError(t2)))
1278 cons = constraint_makeEnsureEqual (t1, t2, sequencePoint);
1279 DPRINTF (("Ensure equal constraint: %s", constraint_unparse (cons)));
1280 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1281 DPRINTF (("Assignment constraints: %s", constraintList_unparse (e->ensuresConstraints)));
1285 t1 = exprData_getOpA (data);
1286 t2 = exprData_getOpB (data);
1287 tok = exprData_getOpTok (data);
1289 if (lltok_getTok (tok) == ADD_ASSIGN)
1291 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1292 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1294 cons = constraint_makeAddAssign (t1, t2, sequencePoint);
1295 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1297 else if (lltok_getTok (tok) == SUB_ASSIGN)
1299 exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
1300 exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
1302 cons = constraint_makeSubtractAssign (t1, t2, sequencePoint);
1303 e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
1307 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
1308 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1311 if (lltok_isBoolean_Op (tok))
1312 exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
1316 /*drl 4-11-03 I think this is the same as the next case...*/
1322 C standard says operand to sizeof isn't evaluated unless
1323 its a variable length array. So we don't generate constraints.
1329 fcn = exprData_getFcn(data);
1331 exprNode_exprTraverse (fcn, definatelv, definaterv, sequencePoint);
1332 DPRINTF (("Got call that %s (%s)",
1333 exprNode_unparse(fcn), exprNodeList_unparse (exprData_getArgs (data))));
1335 llassert( exprNode_isDefined(fcn) );
1337 fcn->requiresConstraints =
1338 constraintList_addListFree (fcn->requiresConstraints,
1339 checkCall (fcn, exprData_getArgs (data)));
1341 fcn->ensuresConstraints =
1342 constraintList_addListFree (fcn->ensuresConstraints,
1343 exprNode_getPostConditions(fcn, exprData_getArgs (data),e ));
1345 t1 = exprNode_createNew (exprNode_getType (e));
1346 checkArgumentList (t1, exprData_getArgs(data), sequencePoint);
1347 exprNode_mergeResolve (e, t1, fcn);
1352 exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint);
1355 case XPR_NULLRETURN:
1361 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint);
1365 exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint);
1368 case XPR_STRINGLITERAL:
1377 t1 = exprData_getUopNode(data);
1380 /* drl 3/2/2003 we know this because of the type of expression*/
1381 llassert( exprNode_isDefined(t1) );
1384 tok = (exprData_getUopTok (data));
1385 exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint);
1386 /*handle * pointer access */
1387 if (lltok_isIncOp (tok))
1389 DPRINTF(("doing ++(var)"));
1390 t1 = exprData_getUopNode (data);
1391 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint);
1392 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1394 else if (lltok_isDecOp (tok))
1396 DPRINTF(("doing --(var)"));
1397 t1 = exprData_getUopNode (data);
1398 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint);
1399 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1401 else if (lltok_isMult(tok ))
1405 cons = constraint_makeWriteSafeInt (t1, 0);
1409 cons = constraint_makeReadSafeInt (t1, 0);
1411 e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
1413 else if (lltok_isNotOp (tok))
1416 constraintList_free(e->trueEnsuresConstraints);
1418 e->trueEnsuresConstraints = constraintList_copy (t1->falseEnsuresConstraints);
1419 constraintList_free(e->falseEnsuresConstraints);
1420 e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
1423 else if (lltok_isAmpersand_Op (tok))
1427 else if (lltok_isMinus_Op (tok))
1431 else if (lltok_isExcl_Op (tok))
1435 else if (lltok_isTilde_Op (tok))
1441 llcontbug (message("Unsupported preop in %s", exprNode_unparse(e)));
1447 exprNode_exprTraverse (exprData_getUopNode (data), TRUE,
1448 definaterv, sequencePoint);
1450 if (lltok_isIncOp (exprData_getUopTok (data)))
1452 DPRINTF(("doing ++"));
1453 t1 = exprData_getUopNode (data);
1454 cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint);
1455 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1457 if (lltok_isDecOp (exprData_getUopTok (data)))
1459 DPRINTF(("doing --"));
1460 t1 = exprData_getUopNode (data);
1461 cons = constraint_makeMaxSetSideEffectPostDecrement (t1, sequencePoint);
1462 e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
1467 t2 = exprData_getCastNode (data);
1468 DPRINTF ((message ("Examining cast (%q)%s",
1469 qtype_unparse (exprData_getCastType (data)),
1470 exprNode_unparse (t2))
1472 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1478 exprNode pred, trueBranch, falseBranch;
1480 pred = exprData_getTriplePred (data);
1481 trueBranch = exprData_getTripleTrue (data);
1482 falseBranch = exprData_getTripleFalse (data);
1484 llassert (exprNode_isDefined (pred));
1485 llassert (exprNode_isDefined (trueBranch));
1486 llassert (exprNode_isDefined (falseBranch));
1488 exprNode_exprTraverse (pred, FALSE, TRUE, sequencePoint);
1490 temp = pred->ensuresConstraints;
1491 pred->ensuresConstraints = exprNode_traverseEnsuresConstraints(pred);
1492 constraintList_free(temp);
1494 temp = pred->requiresConstraints;
1495 pred->requiresConstraints = exprNode_traverseRequiresConstraints(pred);
1496 constraintList_free(temp);
1498 temp = pred->trueEnsuresConstraints;
1499 pred->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(pred);
1500 constraintList_free(temp);
1502 temp = pred->falseEnsuresConstraints;
1503 pred->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(pred);
1504 constraintList_free(temp);
1506 exprNode_exprTraverse (trueBranch, FALSE, TRUE, sequencePoint);
1508 temp = trueBranch->ensuresConstraints;
1509 trueBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(trueBranch);
1510 constraintList_free(temp);
1512 temp = trueBranch->requiresConstraints;
1513 trueBranch->requiresConstraints = exprNode_traverseRequiresConstraints(trueBranch);
1514 constraintList_free(temp);
1516 temp = trueBranch->trueEnsuresConstraints;
1517 trueBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(trueBranch);
1518 constraintList_free(temp);
1520 temp = trueBranch->falseEnsuresConstraints;
1521 trueBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(trueBranch);
1522 constraintList_free(temp);
1524 exprNode_exprTraverse (falseBranch, FALSE, TRUE, sequencePoint);
1526 temp = falseBranch->ensuresConstraints;
1527 falseBranch->ensuresConstraints = exprNode_traverseEnsuresConstraints(falseBranch);
1528 constraintList_free(temp);
1531 temp = falseBranch->requiresConstraints;
1532 falseBranch->requiresConstraints = exprNode_traverseRequiresConstraints(falseBranch);
1533 constraintList_free(temp);
1535 temp = falseBranch->trueEnsuresConstraints;
1536 falseBranch->trueEnsuresConstraints = exprNode_traverseTrueEnsuresConstraints(falseBranch);
1537 constraintList_free(temp);
1539 temp = falseBranch->falseEnsuresConstraints;
1540 falseBranch->falseEnsuresConstraints = exprNode_traverseFalseEnsuresConstraints(falseBranch);
1541 constraintList_free(temp);
1543 /* if pred is true e equals true otherwise pred equals false */
1545 cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1546 trueBranch->ensuresConstraints = constraintList_add(trueBranch->ensuresConstraints, cons);
1548 cons = constraint_makeEnsureEqual (e, trueBranch, sequencePoint);
1549 falseBranch->ensuresConstraints = constraintList_add(falseBranch->ensuresConstraints, cons);
1551 e = doIfElse (e, pred, trueBranch, falseBranch);
1556 t1 = exprData_getPairA (data);
1557 t2 = exprData_getPairB (data);
1558 /* we essiantially treat this like expr1; expr2
1559 of course sequencePoint isn't adjusted so this isn't completely accurate
1562 exprNode_exprTraverse (t1, FALSE, FALSE, sequencePoint);
1563 exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint);
1564 exprNode_mergeResolve (e, t1, t2);
1571 e->requiresConstraints = constraintList_preserveOrig (e->requiresConstraints);
1572 e->ensuresConstraints = constraintList_preserveOrig (e->ensuresConstraints);
1573 e->requiresConstraints = constraintList_addGeneratingExpr (e->requiresConstraints, e);
1574 e->ensuresConstraints = constraintList_addGeneratingExpr (e->ensuresConstraints, e);
1575 e->requiresConstraints = constraintList_removeSurpressed (e->requiresConstraints);
1577 DPRINTF (("ensures constraints for %s are %s",
1578 exprNode_unparse(e), constraintList_unparseDetailed (e->ensuresConstraints)));
1580 DPRINTF (("Requires constraints for %s are %s", exprNode_unparse(e),
1581 constraintList_unparseDetailed(e->ensuresConstraints)));
1583 DPRINTF (("trueEnsures constraints for %s are %s", exprNode_unparse(e),
1584 constraintList_unparseDetailed(e->trueEnsuresConstraints)));
1586 DPRINTF (("falseEnsures constraints for %s are %s", exprNode_unparse(e),
1587 constraintList_unparseDetailed(e->falseEnsuresConstraints)));
1592 constraintList exprNode_traverseTrueEnsuresConstraints (exprNode e)
1596 bool handledExprNode;
1600 if (exprNode_handleError (e))
1602 ret = constraintList_makeNew();
1606 ret = constraintList_copy (e->trueEnsuresConstraints);
1608 handledExprNode = TRUE;
1615 t1 = exprData_getSingle (data);
1616 ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints (t1));
1621 ret = constraintList_addListFree (ret,
1622 exprNode_traverseTrueEnsuresConstraints
1623 (exprData_getPairA (data)));
1625 ret = constraintList_addListFree (ret,
1626 exprNode_traverseTrueEnsuresConstraints
1627 (exprData_getPairB (data)));
1631 ret = constraintList_addListFree (ret,
1632 exprNode_traverseTrueEnsuresConstraints
1633 (exprData_getUopNode (data)));
1637 ret = constraintList_addListFree (ret, exprNode_traverseTrueEnsuresConstraints
1638 (exprData_getUopNode (data)));
1642 ret = constraintList_addListFree (ret,
1643 exprNode_traverseTrueEnsuresConstraints
1644 (exprData_getInitNode (data)));
1649 ret = constraintList_addListFree (ret,
1650 exprNode_traverseTrueEnsuresConstraints
1651 (exprData_getOpA (data)));
1653 ret = constraintList_addListFree (ret,
1654 exprNode_traverseTrueEnsuresConstraints
1655 (exprData_getOpB (data)));
1658 ret = constraintList_addListFree (ret,
1659 exprNode_traverseTrueEnsuresConstraints
1660 (exprData_getOpA (data)));
1662 ret = constraintList_addListFree (ret,
1663 exprNode_traverseTrueEnsuresConstraints
1664 (exprData_getOpB (data)));
1671 ret = constraintList_addListFree (ret,
1672 exprNode_traverseTrueEnsuresConstraints
1673 (exprData_getSingle (data)));
1677 ret = constraintList_addListFree (ret,
1678 exprNode_traverseTrueEnsuresConstraints
1679 (exprData_getFcn (data)));
1683 ret = constraintList_addListFree (ret,
1684 exprNode_traverseTrueEnsuresConstraints
1685 (exprData_getSingle (data)));
1688 case XPR_NULLRETURN:
1692 ret = constraintList_addListFree (ret,
1693 exprNode_traverseTrueEnsuresConstraints
1694 (exprData_getFieldNode (data)));
1698 ret = constraintList_addListFree (ret,
1699 exprNode_traverseTrueEnsuresConstraints
1700 (exprData_getFieldNode (data)));
1703 case XPR_STRINGLITERAL:
1710 ret = constraintList_addListFree (ret,
1711 exprNode_traverseTrueEnsuresConstraints
1712 (exprData_getUopNode (data)));
1717 ret = constraintList_addListFree (ret,
1718 exprNode_traverseTrueEnsuresConstraints
1719 (exprData_getCastNode (data)));
1729 constraintList exprNode_traverseFalseEnsuresConstraints (exprNode e)
1732 bool handledExprNode;
1736 if (exprNode_handleError (e))
1738 ret = constraintList_makeNew();
1742 ret = constraintList_copy (e->falseEnsuresConstraints);
1743 handledExprNode = TRUE;
1749 t1 = exprData_getSingle (data);
1750 ret = constraintList_addListFree (ret,exprNode_traverseFalseEnsuresConstraints (t1));
1755 ret = constraintList_addListFree (ret,
1756 exprNode_traverseFalseEnsuresConstraints
1757 (exprData_getPairA (data)));
1759 ret = constraintList_addListFree (ret,
1760 exprNode_traverseFalseEnsuresConstraints
1761 (exprData_getPairB (data)));
1765 ret = constraintList_addListFree (ret,
1766 exprNode_traverseFalseEnsuresConstraints
1767 (exprData_getUopNode (data)));
1771 ret = constraintList_addListFree (ret, exprNode_traverseFalseEnsuresConstraints
1772 (exprData_getUopNode (data)));
1775 ret = constraintList_addListFree (ret,
1776 exprNode_traverseFalseEnsuresConstraints
1777 ( exprData_getInitNode (data)));
1781 ret = constraintList_addListFree (ret,
1782 exprNode_traverseFalseEnsuresConstraints
1783 (exprData_getOpA (data)));
1785 ret = constraintList_addListFree (ret,
1786 exprNode_traverseFalseEnsuresConstraints
1787 (exprData_getOpB (data)));
1790 ret = constraintList_addListFree (ret,
1791 exprNode_traverseFalseEnsuresConstraints
1792 (exprData_getOpA (data)));
1794 ret = constraintList_addListFree (ret,
1795 exprNode_traverseFalseEnsuresConstraints
1796 (exprData_getOpB (data)));
1803 ret = constraintList_addListFree (ret,
1804 exprNode_traverseFalseEnsuresConstraints
1805 (exprData_getSingle (data)));
1809 ret = constraintList_addListFree (ret,
1810 exprNode_traverseFalseEnsuresConstraints
1811 (exprData_getFcn (data)));
1815 ret = constraintList_addListFree (ret,
1816 exprNode_traverseFalseEnsuresConstraints
1817 (exprData_getSingle (data)));
1820 case XPR_NULLRETURN:
1824 ret = constraintList_addListFree (ret,
1825 exprNode_traverseFalseEnsuresConstraints
1826 (exprData_getFieldNode (data)));
1830 ret = constraintList_addListFree (ret,
1831 exprNode_traverseFalseEnsuresConstraints
1832 (exprData_getFieldNode (data)));
1835 case XPR_STRINGLITERAL:
1842 ret = constraintList_addListFree (ret,
1843 exprNode_traverseFalseEnsuresConstraints
1844 (exprData_getUopNode (data)));
1849 ret = constraintList_addListFree (ret,
1850 exprNode_traverseFalseEnsuresConstraints
1851 (exprData_getCastNode (data)));
1862 /* walk down the tree and get all requires Constraints in each subexpression*/
1863 /*@only@*/ constraintList exprNode_traverseRequiresConstraints (exprNode e)
1867 bool handledExprNode;
1871 if (exprNode_handleError (e))
1873 ret = constraintList_makeNew();
1877 ret = constraintList_copy (e->requiresConstraints);
1878 handledExprNode = TRUE;
1884 t1 = exprData_getSingle (data);
1885 ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints (t1));
1890 ret = constraintList_addListFree (ret,
1891 exprNode_traverseRequiresConstraints
1892 (exprData_getPairA (data)));
1894 ret = constraintList_addListFree (ret,
1895 exprNode_traverseRequiresConstraints
1896 (exprData_getPairB (data)));
1900 ret = constraintList_addListFree (ret,
1901 exprNode_traverseRequiresConstraints
1902 (exprData_getUopNode (data)));
1906 ret = constraintList_addListFree (ret, exprNode_traverseRequiresConstraints
1907 (exprData_getUopNode (data)));
1910 ret = constraintList_addListFree (ret,
1911 exprNode_traverseRequiresConstraints
1912 (exprData_getInitNode (data)));
1916 ret = constraintList_addListFree (ret,
1917 exprNode_traverseRequiresConstraints
1918 (exprData_getOpA (data)));
1920 ret = constraintList_addListFree (ret,
1921 exprNode_traverseRequiresConstraints
1922 (exprData_getOpB (data)));
1925 ret = constraintList_addListFree (ret,
1926 exprNode_traverseRequiresConstraints
1927 (exprData_getOpA (data)));
1929 ret = constraintList_addListFree (ret,
1930 exprNode_traverseRequiresConstraints
1931 (exprData_getOpB (data)));
1938 ret = constraintList_addListFree (ret,
1939 exprNode_traverseRequiresConstraints
1940 (exprData_getSingle (data)));
1944 ret = constraintList_addListFree (ret,
1945 exprNode_traverseRequiresConstraints
1946 (exprData_getFcn (data)));
1950 ret = constraintList_addListFree (ret,
1951 exprNode_traverseRequiresConstraints
1952 (exprData_getSingle (data)));
1955 case XPR_NULLRETURN:
1959 ret = constraintList_addListFree (ret,
1960 exprNode_traverseRequiresConstraints
1961 (exprData_getFieldNode (data)));
1965 ret = constraintList_addListFree (ret,
1966 exprNode_traverseRequiresConstraints
1967 (exprData_getFieldNode (data)));
1970 case XPR_STRINGLITERAL:
1977 ret = constraintList_addListFree (ret,
1978 exprNode_traverseRequiresConstraints
1979 (exprData_getUopNode (data)));
1984 ret = constraintList_addListFree (ret,
1985 exprNode_traverseRequiresConstraints
1986 (exprData_getCastNode (data)));
1997 /* walk down the tree and get all Ensures Constraints in each subexpression*/
1998 /*@only@*/ constraintList exprNode_traverseEnsuresConstraints (exprNode e)
2002 bool handledExprNode;
2006 if (exprNode_handleError (e))
2008 ret = constraintList_makeNew();
2012 ret = constraintList_copy (e->ensuresConstraints);
2013 handledExprNode = TRUE;
2017 DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with "
2018 "constraintList of %s",
2019 exprNode_unparse (e),
2020 constraintList_unparse(e->ensuresConstraints)
2028 t1 = exprData_getSingle (data);
2029 ret = constraintList_addListFree (ret,exprNode_traverseEnsuresConstraints (t1));
2033 ret = constraintList_addListFree (ret,
2034 exprNode_traverseEnsuresConstraints
2035 (exprData_getPairA (data)));
2037 ret = constraintList_addListFree (ret,
2038 exprNode_traverseEnsuresConstraints
2039 (exprData_getPairB (data)));
2042 ret = constraintList_addListFree (ret,
2043 exprNode_traverseEnsuresConstraints
2044 (exprData_getUopNode (data)));
2048 ret = constraintList_addListFree (ret, exprNode_traverseEnsuresConstraints
2049 (exprData_getUopNode (data)));
2053 ret = constraintList_addListFree (ret,
2054 exprNode_traverseEnsuresConstraints
2055 (exprData_getInitNode (data)));
2060 ret = constraintList_addListFree (ret,
2061 exprNode_traverseEnsuresConstraints
2062 (exprData_getOpA (data)));
2064 ret = constraintList_addListFree (ret,
2065 exprNode_traverseEnsuresConstraints
2066 (exprData_getOpB (data)));
2069 ret = constraintList_addListFree (ret,
2070 exprNode_traverseEnsuresConstraints
2071 (exprData_getOpA (data)));
2073 ret = constraintList_addListFree (ret,
2074 exprNode_traverseEnsuresConstraints
2075 (exprData_getOpB (data)));
2081 ret = constraintList_addListFree (ret,
2082 exprNode_traverseEnsuresConstraints
2083 (exprData_getSingle (data)));
2086 ret = constraintList_addListFree (ret,
2087 exprNode_traverseEnsuresConstraints
2088 (exprData_getFcn (data)));
2091 ret = constraintList_addListFree (ret,
2092 exprNode_traverseEnsuresConstraints
2093 (exprData_getSingle (data)));
2095 case XPR_NULLRETURN:
2098 ret = constraintList_addListFree (ret,
2099 exprNode_traverseEnsuresConstraints
2100 (exprData_getFieldNode (data)));
2103 ret = constraintList_addListFree (ret,
2104 exprNode_traverseEnsuresConstraints
2105 (exprData_getFieldNode (data)));
2107 case XPR_STRINGLITERAL:
2112 ret = constraintList_addListFree (ret,
2113 exprNode_traverseEnsuresConstraints
2114 (exprData_getUopNode (data)));
2117 ret = constraintList_addListFree (ret,
2118 exprNode_traverseEnsuresConstraints
2119 (exprData_getCastNode (data)));
2125 DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with "
2126 "constraintList of is returning %s",
2127 exprNode_unparse (e),
2128 constraintList_unparse(ret))));
2133 /*drl moved out of constraintResolve.c 07-02-001 */
2134 void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist,
2135 fileloc sequencePoint)
2138 llassert(temp != NULL );
2140 temp->requiresConstraints = constraintList_makeNew();
2141 temp->ensuresConstraints = constraintList_makeNew();
2142 temp->trueEnsuresConstraints = constraintList_makeNew();
2143 temp->falseEnsuresConstraints = constraintList_makeNew();
2145 exprNodeList_elements (arglist, el)
2147 constraintList temp2;
2149 llassert(exprNode_isDefined(el) );
2151 exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
2152 temp2 = el->requiresConstraints;
2153 el->requiresConstraints = exprNode_traverseRequiresConstraints(el);
2154 constraintList_free(temp2);
2156 temp2 = el->ensuresConstraints;
2157 el->ensuresConstraints = exprNode_traverseEnsuresConstraints(el);
2158 constraintList_free(temp2);
2160 temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
2161 el->requiresConstraints);
2163 temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
2164 el->ensuresConstraints);
2166 end_exprNodeList_elements;
2170 /*drl moved out of constraintResolve.c 07-03-001 */
2171 constraintList exprNode_getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
2173 constraintList postconditions;
2175 DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist))));
2177 temp = exprNode_getUentry (fcn);
2179 postconditions = uentry_getFcnPostconditions (temp);
2181 if (constraintList_isDefined (postconditions))
2183 postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
2184 postconditions = constraintList_doFixResult (postconditions, fcnCall);
2188 postconditions = constraintList_makeNew();
2191 return postconditions;
2195 comment this out for now
2196 we'll include it in a production release when its stable...
2198 void findStructs (exprNodeList arglist)
2204 message("doing findStructs: %s", exprNodeList_unparse(arglist))
2208 exprNodeList_elements(arglist, expr)
2210 ct = exprNode_getType(expr);
2212 rt = ctype_realType (ct);
2214 if (ctype_isStruct (rt))
2215 TPRINTF((message("Found structure %s", exprNode_unparse(expr))
2217 if (hasInvariants(ct))
2219 constraintList invars;
2221 invars = getInvariants(ct);
2224 TPRINTF((message ("findStructs has invariants %s ", constraintList_unparse (invars))
2227 invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct);
2230 TPRINTF((message ("findStructs finded invariants to be %s ", constraintList_unparse (invars))
2234 end_exprNodeList_elements;
2239 /*drl moved out of constraintResolve.c 07-02-001 */
2240 constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
2242 constraintList preconditions;
2244 DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist))));
2246 temp = exprNode_getUentry (fcn);
2248 preconditions = uentry_getFcnPreconditions (temp);
2250 if (constraintList_isDefined(preconditions))
2252 preconditions = constraintList_togglePost (preconditions);
2253 preconditions = constraintList_preserveCallInfo(preconditions, fcn);
2254 preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
2258 if (constraintList_isUndefined(preconditions))
2259 preconditions = constraintList_makeNew();
2262 if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS))
2266 uentryList_elements (arglist, el)
2269 TPRINTF((message("setImplicitfcnConstraints doing: %s", uentry_unparse(el) ) ));
2271 s = uentry_getSref(el);
2272 if (sRef_isReference (s) )
2274 TPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
2278 TPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
2281 //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0
2282 c = constraint_makeSRefWriteSafeInt (s, 0);
2284 implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
2286 //drl 10/23/2002 added support for out
2287 if (!uentry_isOut(el) )
2289 c = constraint_makeSRefReadSafeInt (s, 0);
2290 implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
2298 DPRINTF ((message("Done checkCall\n")));
2299 DPRINTF ((message("Returning list %q ", constraintList_unparseDetailed(preconditions))));
2302 drl we're going to comment this out for now
2303 we'll include it if we're sure it's working
2305 findStructs(arglist);
2308 return preconditions;
2311 /*drl added this function 10.29.001
2312 takes an exprNode of the form const + const
2316 I'm a bit nervous about modifying the exprNode
2317 but this is the easy way to do this
2318 If I have time I'd like to cause the exprNode to get created correctly in the first place */
2319 void exprNode_findValue(exprNode e)
2326 llassert(exprNode_isDefined(e) );
2330 if (exprNode_hasValue(e))
2333 if (e->kind == XPR_OP)
2335 t1 = exprData_getOpA (data);
2336 t2 = exprData_getOpB (data);
2337 tok = exprData_getOpTok (data);
2339 exprNode_findValue(t1);
2340 exprNode_findValue(t2);
2342 if (!(exprNode_knownIntValue(t1) && (exprNode_knownIntValue(t2))))
2345 if (lltok_isPlus_Op (tok))
2349 v1 = exprNode_getLongValue(t1);
2350 v2 = exprNode_getLongValue(t2);
2352 if (multiVal_isDefined(e->val))
2353 multiVal_free (e->val);
2355 e->val = multiVal_makeInt (v1 + v2);
2358 if (lltok_isMinus_Op (tok))
2362 v1 = exprNode_getLongValue(t1);
2363 v2 = exprNode_getLongValue(t2);
2365 if (multiVal_isDefined(e->val))
2367 multiVal_free (e->val);
2370 e->val = multiVal_makeInt (v1 - v2);
2373 /*drl I should really do * and / at some point */