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 "splintMacros.nf"
34 # include "cgrammar.h"
36 /*drl We need to access the internal representation of exprNode
37 because these functions walk down the parse tree and need a richer
38 information than is accessible through the exprNode interface.*/
42 static /*@nullwhentrue@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e
);
44 static void exprNode_stmt (/*@temp@*/ /*@temp@*/ exprNode p_e
);
45 static void exprNode_multiStatement (/*@temp@*/ exprNode p_e
);
47 static constraintList
exprNode_traverseTrueEnsuresConstraints (/*@temp@*/ exprNode p_e
);
48 static constraintList
exprNode_traverseFalseEnsuresConstraints (/*@temp@*/ exprNode p_e
);
50 static void checkArgumentList (/*@out@*/ exprNode p_temp
, exprNodeList p_arglist
, fileloc p_sequencePoint
) /*@modifies p_temp @*/;
52 static constraintList
checkCall (/*@temp@*/ exprNode p_fcn
, exprNodeList p_arglist
);
54 static void exprNode_exprTraverse (exprNode p_e
, bool p_definatelv
, bool p_definaterv
,
55 /*@temp@*/ /*@observer@*/ fileloc p_sequencePoint
);
56 static /*@only@*/ constraintList
exprNode_traverseRequiresConstraints (exprNode p_e
);
57 static constraintList
exprNode_getPostConditions (
58 /*@dependent@*/ /*@observer@*/ exprNode p_fcn
, exprNodeList p_arglist
,
59 /*@dependent@*/ /*@observer@*/ exprNode p_fcnCall
) /*@*/;
60 static /*@only@*/ constraintList
exprNode_traverseEnsuresConstraints (exprNode p_e
);
63 static bool exprNode_isUnhandled (/*@temp@*/ /*@observer@*/ exprNode e
)
65 llassert(exprNode_isDefined(e
));
91 DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e
))));
103 /*@nullwhentrue@*/ bool exprNode_handleError (exprNode e
)
105 if (exprNode_isError (e
) || exprNode_isUnhandled (e
))
113 /* evans 2002-03-2 - parameter was dependent */
114 void exprNode_generateConstraints (/*@temp@*/ exprNode e
)
116 if (exprNode_isError (e
))
119 if (exprNode_isUnhandled (e
))
121 DPRINTF((message("Warning ignoring %s", exprNode_unparse (e
))));
125 DPRINTF ((message ("exprNode_generateConstraints Analyzing %s at %s", exprNode_unparse(e
),
126 fileloc_unparse(exprNode_loc (e
)))));
128 if (exprNode_isMultiStatement (e
))
130 exprNode_multiStatement(e
);
136 /* loc = exprNode_getNextSequencePoint(e); */
137 /* exprNode_exprTraverse(e, FALSE, FALSE, loc); */
139 /* fileloc_free(loc); */
149 c
= constraintList_makeFixedArrayConstraints (e
->uses
);
150 e
->requiresConstraints
= constraintList_reflectChangesFreePre (e
->requiresConstraints
, c
);
151 constraintList_free(c
);
154 DPRINTF ((message ("e->requiresConstraints %s",
155 constraintList_unparseDetailed (e
->requiresConstraints
))));
159 static void exprNode_stmt (/*@temp@*/ exprNode e
)
164 DPRINTF (("Generating constraint for: %s", exprNode_unparse (e
)));
166 if (exprNode_isError(e
))
171 /*e->requiresConstraints = constraintList_makeNew();
172 e->ensuresConstraints = constraintList_makeNew(); */
174 /*!! s = exprNode_unparse (e); */
176 if (e
->kind
== XPR_INIT
)
178 constraintList tempList
;
179 DPRINTF (("Init: %s ", exprNode_unparse (e
)));
180 loc
= exprNode_getNextSequencePoint (e
); /* reduces to an expression */
181 DPRINTF (("Location: %s", fileloc_unparse (loc
)));
182 DPRINTF (("Ensures before: %s", constraintList_unparse (e
->ensuresConstraints
)));
183 exprNode_exprTraverse (e
, FALSE
, FALSE
, loc
);
184 DPRINTF (("Ensures after: %s", constraintList_unparse (e
->ensuresConstraints
)));
185 DPRINTF (("After traversing..."));
188 tempList
= e
->requiresConstraints
;
189 DPRINTF (("Requires before: %s", constraintList_unparse (e
->requiresConstraints
)));
190 e
->requiresConstraints
= exprNode_traverseRequiresConstraints (e
);
191 DPRINTF (("Requires after: %s", constraintList_unparse (e
->requiresConstraints
)));
192 constraintList_free(tempList
);
194 tempList
= e
->ensuresConstraints
;
195 DPRINTF (("Ensures before: %s", constraintList_unparse (e
->ensuresConstraints
)));
196 e
->ensuresConstraints
= exprNode_traverseEnsuresConstraints(e
);
197 DPRINTF (("Ensures before: %s", constraintList_unparse (e
->ensuresConstraints
)));
198 constraintList_free(tempList
);
202 /*drl 2/13/002 patched bug so return statement will be checked*/
203 /*return is a stmt not not expression ...*/
204 if (e
->kind
== XPR_RETURN
)
206 constraintList tempList
;
208 loc
= exprNode_getNextSequencePoint(e
); /* reduces to an expression */
210 exprNode_exprTraverse (exprData_getSingle (e
->edata
), FALSE
, TRUE
, loc
);
213 tempList
= e
->requiresConstraints
;
214 e
->requiresConstraints
= exprNode_traverseRequiresConstraints(e
);
215 constraintList_free(tempList
);
218 if (e
->kind
!= XPR_STMT
)
220 DPRINTF (("Not Stmt"));
221 DPRINTF ((message ("%s ", exprNode_unparse (e
))));
223 if (exprNode_isMultiStatement (e
))
225 exprNode_multiStatement (e
); /* evans 2001-08-21: spurious return removed */
229 loc
= exprNode_getNextSequencePoint(e
); /* reduces to an expression */
231 exprNode_exprTraverse (e
, FALSE
, TRUE
, loc
);
239 DPRINTF ((message ("%s ", exprNode_unparse (e
))));
241 snode
= exprData_getUopNode (e
->edata
);
243 /* could be stmt involving multiple statements:
244 i.e. if, while for ect.
247 if (exprNode_isMultiStatement (snode
))
249 exprNode_multiStatement (snode
);
250 (void) exprNode_copyConstraints (e
, snode
);
254 loc
= exprNode_getNextSequencePoint(e
); /* reduces to an expression */
255 exprNode_exprTraverse (snode
, FALSE
, FALSE
, loc
);
259 constraintList_free (e
->requiresConstraints
);
260 e
->requiresConstraints
= exprNode_traverseRequiresConstraints(snode
);
262 constraintList_free (e
->ensuresConstraints
);
263 e
->ensuresConstraints
= exprNode_traverseEnsuresConstraints(snode
);
265 DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
266 constraintList_unparse(e
->requiresConstraints
),
267 constraintList_unparse(e
->ensuresConstraints
))));
272 static void exprNode_stmtList (/*@dependent@*/ exprNode e
)
274 exprNode stmt1
, stmt2
;
275 if (exprNode_isError (e
))
281 Handle case of stmtList with only one statement:
282 The parse tree stores this as stmt instead of stmtList
285 if (e
->kind
!= XPR_STMTLIST
)
290 llassert (e
->kind
== XPR_STMTLIST
);
291 DPRINTF(("exprNode_stmtList STMTLIST:"));
292 DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e
))));
293 stmt1
= exprData_getPairA (e
->edata
);
294 stmt2
= exprData_getPairB (e
->edata
);
297 DPRINTF(("exprNode_stmtlist "));
298 DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1
), exprNode_unparse(stmt2
))));
300 exprNode_stmt (stmt1
);
301 DPRINTF(("\nstmt after stmtList call "));
303 exprNode_stmt (stmt2
);
304 exprNode_mergeResolve (e
, stmt1
, stmt2
);
306 DPRINTF ((message ("smtlist constraints are: pre: %s \n and \t post %s\n",
307 constraintList_unparse(e
->requiresConstraints
),
308 constraintList_unparse(e
->ensuresConstraints
))));
312 static exprNode
doIf (/*@returned@*/ exprNode e
, /*@dependent@*/ exprNode test
, /*@dependent@*/ exprNode body
)
316 DPRINTF ((message ("doIf: %s ", exprNode_unparse(e
))));
318 llassert (exprNode_isDefined(test
));
319 llassert (exprNode_isDefined (e
));
320 llassert (exprNode_isDefined (body
));
322 DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(e
), constraintList_unparseDetailed(e
->ensuresConstraints
))));
324 DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(e
), constraintList_unparseDetailed(e
->ensuresConstraints
))));
326 DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(e
), constraintList_unparseDetailed(e
->trueEnsuresConstraints
))));
328 DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(e
), constraintList_unparseDetailed(e
->falseEnsuresConstraints
))));
332 DPRINTF((message ("ensures constraints for %s are %s", exprNode_unparse(test
), constraintList_unparseDetailed(test
->ensuresConstraints
))));
334 DPRINTF((message ("Requires constraints for %s are %s", exprNode_unparse(test
), constraintList_unparseDetailed(test
->ensuresConstraints
))));
336 DPRINTF((message ("trueEnsures constraints for %s are %s", exprNode_unparse(test
), constraintList_unparseDetailed(test
->trueEnsuresConstraints
))));
338 DPRINTF((message ("falseEnsures constraints for %s are %s", exprNode_unparse(test
), constraintList_unparseDetailed(test
->falseEnsuresConstraints
))));
342 temp
= test
->trueEnsuresConstraints
;
343 test
->trueEnsuresConstraints
= exprNode_traverseTrueEnsuresConstraints(test
);
344 constraintList_free(temp
);
346 temp
= test
->ensuresConstraints
;
347 test
->ensuresConstraints
= exprNode_traverseEnsuresConstraints (test
);
348 constraintList_free(temp
);
350 temp
= test
->requiresConstraints
;
351 test
->requiresConstraints
= exprNode_traverseRequiresConstraints (test
);
352 constraintList_free(temp
);
355 test
->trueEnsuresConstraints
= constraintList_substituteFreeTarget(test
->trueEnsuresConstraints
, test
->ensuresConstraints
);
357 DPRINTF ((message ("doIf: test ensures %s ", constraintList_unparse(test
->ensuresConstraints
))));
359 DPRINTF ((message ("doIf: test true ensures %s ", constraintList_unparse(test
->trueEnsuresConstraints
))));
361 constraintList_free(e
->requiresConstraints
);
364 e
->requiresConstraints
= constraintList_reflectChanges(body
->requiresConstraints
, test
->trueEnsuresConstraints
);
366 e
->requiresConstraints
= constraintList_reflectChangesFreePre (e
->requiresConstraints
,
367 test
->ensuresConstraints
);
368 temp
= e
->requiresConstraints
;
369 e
->requiresConstraints
= constraintList_mergeRequires (e
->requiresConstraints
, test
->requiresConstraints
);
370 constraintList_free(temp
);
373 /* drl possible problem : warning bad */
374 constraintList_free(e
->ensuresConstraints
);
375 e
->ensuresConstraints
= constraintList_copy (test
->ensuresConstraints
);
377 if (exprNode_mayEscape (body
))
379 DPRINTF ((message("doIf: the if statement body %s returns or exits", exprNode_unparse(body
))));
380 e
->ensuresConstraints
= constraintList_mergeEnsuresFreeFirst (e
->ensuresConstraints
,
381 test
->falseEnsuresConstraints
);
384 DPRINTF ((message ("doIf: if requiers %s ", constraintList_unparse(e
->requiresConstraints
))));
390 Also used for condition i.e. ?: operation
393 This function assumes that p, trueBranch, falseBranch have have all been traversed
394 for constraints i.e. we assume that exprNode_traverseEnsuresConstraints,
395 exprNode_traverseRequiresConstraints, exprNode_traverseTrueEnsuresConstraints,
396 exprNode_traverseFalseEnsuresConstraints have all been run
399 static exprNode
doIfElse (/*@returned@*/ exprNode e
, /*@dependent@*/ exprNode p
, /*@dependent@*/ exprNode trueBranch
, /*@dependent@*/ exprNode falseBranch
)
401 constraintList c1
, cons
, t
, t2
, f
, f2
;
403 llassert (exprNode_isDefined (e
));
404 llassert (exprNode_isDefined (p
));
405 llassert (exprNode_isDefined (trueBranch
));
406 llassert (exprNode_isDefined (falseBranch
));
407 DPRINTF ((message ("doIfElse: %s ", exprNode_unparse(e
))));
409 /* do requires clauses */
410 c1
= constraintList_copy (p
->ensuresConstraints
);
412 t
= constraintList_reflectChanges(trueBranch
->requiresConstraints
, p
->trueEnsuresConstraints
);
413 t
= constraintList_reflectChangesFreePre (t
, p
->ensuresConstraints
);
415 cons
= constraintList_reflectChanges(falseBranch
->requiresConstraints
, p
->falseEnsuresConstraints
);
416 cons
= constraintList_reflectChangesFreePre (cons
, c1
);
418 constraintList_free (e
->requiresConstraints
);
419 e
->requiresConstraints
= constraintList_mergeRequiresFreeFirst (t
, cons
);
420 e
->requiresConstraints
= constraintList_mergeRequiresFreeFirst (e
->requiresConstraints
, p
->requiresConstraints
);
422 /* do ensures clauses
423 find the the ensures lists for each subbranch
426 t
= constraintList_mergeEnsures (p
->trueEnsuresConstraints
, trueBranch
->ensuresConstraints
);
428 t
= constraintList_mergeEnsures (p
->ensuresConstraints
, t
);
429 constraintList_free(t2
);
431 f
= constraintList_mergeEnsures (p
->falseEnsuresConstraints
, falseBranch
->ensuresConstraints
);
433 f
= constraintList_mergeEnsures (p
->ensuresConstraints
, f
);
434 constraintList_free(f2
);
436 /* find ensures for whole if/else statement */
438 constraintList_free(e
->ensuresConstraints
);
440 e
->ensuresConstraints
= constraintList_logicalOr (t
, f
);
442 constraintList_free(t
);
443 constraintList_free(f
);
444 constraintList_free(cons
);
445 constraintList_free(c1
);
447 DPRINTF ((message ("doIfElse: if requires %q ", constraintList_unparse(e
->requiresConstraints
))));
448 DPRINTF ((message ("doIfElse: if ensures %q ", constraintList_unparse(e
->ensuresConstraints
))));
453 static exprNode
doWhile (/*@returned@*/ exprNode e
, /*@dependent@*/ exprNode test
, /*@dependent@*/ exprNode body
)
455 DPRINTF ((message ("doWhile: %s ", exprNode_unparse(e
))));
456 return doIf (e
, test
, body
);
459 /*@only@*/ constraintList
constraintList_makeFixedArrayConstraints (/*@observer@*/ sRefSet s
)
463 ret
= constraintList_makeNew();
465 sRefSet_elements (s
, el
)
467 if (sRef_isFixedArray(el
))
470 DPRINTF((message("%s is a fixed array",
472 size
= sRef_getArraySize(el
);
473 DPRINTF((message("%s is a fixed array with size %d",
474 sRef_unparse(el
), (int)size
)));
475 con
= constraint_makeSRefSetBufferSize (el
, size_toLong (size
- 1));
476 ret
= constraintList_add(ret
, con
);
480 DPRINTF((message("%s is not a fixed array",
484 if (sRef_isExternallyVisible (el
))
487 DPRINTF((message("%s is externally visible",
489 con = constraint_makeSRefWriteSafeInt(el, 0);
490 ret = constraintList_add(ret, con);
492 con = constraint_makeSRefReadSafeInt(el, 0);
494 ret = constraintList_add(ret, con);
499 end_sRefSet_elements
;
501 DPRINTF((message("constraintList_makeFixedArrayConstraints returning %s",
502 constraintList_unparse(ret
))));
507 exprNode
makeDataTypeConstraints (/*@returned@*/ exprNode e
)
510 DPRINTF(("makeDataTypeConstraints"));
512 c
= constraintList_makeFixedArrayConstraints (e
->uses
);
514 e
->ensuresConstraints
= constraintList_addListFree (e
->ensuresConstraints
, c
);
520 static void doFor (/*@dependent@*/ exprNode e
, /*@dependent@*/ exprNode forPred
, /*@dependent@*/ exprNode forBody
)
522 exprNode
/* init,*/ test
, inc
;
523 /* merge the constraints: modle as if statement */
530 llassert (exprNode_isDefined (e
));
531 llassert (exprNode_isDefined (forPred
));
532 llassert (exprNode_isDefined (forBody
));
534 /* init = exprData_getTripleInit (forPred->edata); */
535 test
= exprData_getTripleTest (forPred
->edata
);
536 inc
= exprData_getTripleInc (forPred
->edata
);
538 if (((exprNode_isError (test
) /*|| (exprNode_isError(init))*/) || (exprNode_isError (inc
))))
540 DPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e
))));
544 exprNode_forLoopHeuristics(e
, forPred
, forBody
);
546 constraintList_free(e
->requiresConstraints
);
547 e
->requiresConstraints
= constraintList_reflectChanges(forBody
->requiresConstraints
, test
->ensuresConstraints
);
548 e
->requiresConstraints
= constraintList_reflectChangesFreePre (e
->requiresConstraints
, test
->trueEnsuresConstraints
);
549 e
->requiresConstraints
= constraintList_reflectChangesFreePre (e
->requiresConstraints
, forPred
->ensuresConstraints
);
551 if (!forBody
->canBreak
)
553 e
->ensuresConstraints
= constraintList_addListFree(e
->ensuresConstraints
, constraintList_copy(forPred
->ensuresConstraints
));
554 e
->ensuresConstraints
= constraintList_addListFree(e
->ensuresConstraints
,constraintList_copy(test
->falseEnsuresConstraints
));
558 DPRINTF(("Can break"));
562 static /*@dependent@*/ exprNode
exprNode_makeDependent(/*@returned@*/ exprNode e
)
564 /* !!! DRL - this is ridiculous! Read the manual on memory annotations please! */
569 exprNode_doGenerateConstraintSwitch
570 (/*@dependent@*/ exprNode switchExpr
,
571 /*@dependent@*/ exprNode body
,
572 /*@special@*/ constraintList
*currentRequires
,
573 /*@special@*/ constraintList
*currentEnsures
,
574 /*@special@*/ constraintList
*savedRequires
,
575 /*@special@*/ constraintList
*savedEnsures
)
576 /*@post:only *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/
577 /*@sets *currentRequires, *currentEnsures, *savedRequires, *savedEnsures @*/
579 exprNode stmt
, stmtList
;
581 DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s",
582 exprNode_unparse(switchExpr
), exprNode_unparse(body
)
585 if (exprNode_isError(body
))
587 *currentRequires
= constraintList_makeNew ();
588 *currentEnsures
= constraintList_makeNew ();
590 *savedRequires
= constraintList_makeNew ();
591 *savedEnsures
= constraintList_makeNew ();
597 if (body
->kind
!= XPR_STMTLIST
)
599 DPRINTF((message("exprNode_doGenerateConstraintSwitch: non stmtlist: %s",
600 exprNode_unparse(body
))));
602 stmtList
= exprNode_undefined
;
603 stmt
= exprNode_makeDependent(stmt
);
604 stmtList
= exprNode_makeDependent(stmtList
);
608 stmt
= exprData_getPairB(body
->edata
);
609 stmtList
= exprData_getPairA(body
->edata
);
610 stmt
= exprNode_makeDependent(stmt
);
611 stmtList
= exprNode_makeDependent(stmtList
);
614 DPRINTF((message("exprNode_doGenerateConstraintSwitch: stmtlist: %s stmt: %s",
615 exprNode_unparse(stmtList
), exprNode_unparse(stmt
))
619 exprNode_doGenerateConstraintSwitch (switchExpr
, stmtList
, currentRequires
, currentEnsures
,
620 savedRequires
, savedEnsures
);
622 if (exprNode_isError(stmt
))
629 switchExpr
= exprNode_makeDependent (switchExpr
);
631 if (! exprNode_isCaseMarker(stmt
))
636 DPRINTF ((message("Got normal statement %s (requires %s ensures %s)", exprNode_unparse(stmt
),
637 constraintList_unparse(stmt
->requiresConstraints
), constraintList_unparse(stmt
->ensuresConstraints
))));
639 temp
= constraintList_reflectChanges (stmt
->requiresConstraints
,
642 *currentRequires
= constraintList_mergeRequiresFreeFirst(
646 constraintList_free(temp
);
648 *currentEnsures
= constraintList_mergeEnsuresFreeFirst
650 stmt
->ensuresConstraints
);
651 DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
652 "%s currentEnsures:%s",
653 exprNode_unparse(switchExpr
), exprNode_unparse(body
),
654 constraintList_unparse(*currentRequires
), constraintList_unparse(*currentEnsures
)
662 if (exprNode_isCaseMarker(stmt
) && exprNode_mustEscape(stmtList
))
665 ** merge current and saved constraint with Logical Or...
666 ** make a constraint for ensures
672 DPRINTF ((message("Got case marker")));
674 if (constraintList_isUndefined(*savedEnsures
) &&
675 constraintList_isUndefined(*savedRequires
))
677 llassert(constraintList_isUndefined(*savedEnsures
));
678 llassert(constraintList_isUndefined(*savedRequires
));
679 *savedEnsures
= constraintList_copy(*currentEnsures
);
680 *savedRequires
= constraintList_copy(*currentRequires
);
684 DPRINTF ((message("Doing logical or")));
685 temp
= constraintList_logicalOr (*savedEnsures
, *currentEnsures
);
686 constraintList_free (*savedEnsures
);
687 *savedEnsures
= temp
;
689 *savedRequires
= constraintList_mergeRequiresFreeFirst (*savedRequires
, *currentRequires
);
692 con
= constraint_makeEnsureEqual (switchExpr
, exprData_getSingle (stmt
->edata
), exprNode_loc (stmt
));
694 constraintList_free (*currentEnsures
);
695 *currentEnsures
= constraintList_makeNew();
696 *currentEnsures
= constraintList_add(*currentEnsures
, con
);
698 constraintList_free(*currentRequires
);
699 *currentRequires
= constraintList_makeNew();
700 DPRINTF (("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:"
701 "%s savedEnsures:%s",
702 exprNode_unparse(switchExpr
), exprNode_unparse(body
),
703 constraintList_unparse(*savedRequires
), constraintList_unparse(*savedEnsures
)
706 else if (exprNode_isCaseMarker(stmt
)) /* prior case has no break. */
709 We don't do anything to the sved constraints because the case hasn't ended
710 The new ensures constraints for the case will be:
711 the constraint for the case statement (CASE_LABEL == SWITCH_EXPR) logicalOr currentEnsures
716 constraintList ensuresTemp
;
718 con
= constraint_makeEnsureEqual (switchExpr
, exprData_getSingle (stmt
->edata
), exprNode_loc (stmt
));
720 ensuresTemp
= constraintList_makeNew ();
721 ensuresTemp
= constraintList_add (ensuresTemp
, con
);
723 if (exprNode_isError (stmtList
))
725 constraintList_free (*currentEnsures
);
726 *currentEnsures
= constraintList_copy (ensuresTemp
);
727 constraintList_free (ensuresTemp
);
731 temp
= constraintList_logicalOr (*currentEnsures
, ensuresTemp
);
732 constraintList_free (*currentEnsures
);
733 constraintList_free (ensuresTemp
);
734 *currentEnsures
= temp
;
737 constraintList_free (*currentRequires
);
738 *currentRequires
= constraintList_makeNew();
743 we handle the case of ! exprNode_isCaseMarker above
744 the else if clause should always be true.
749 DPRINTF (("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:"
750 "%s currentEnsures:%s",
751 exprNode_unparse(switchExpr
), exprNode_unparse(body
),
752 constraintList_unparse(*currentRequires
), constraintList_unparse(*currentEnsures
)
761 static void exprNode_generateConstraintSwitch (/*@notnull@*/ exprNode switchStmt
)
763 constraintList constraintsRequires
;
764 constraintList constraintsEnsures
;
765 constraintList lastRequires
;
766 constraintList lastEnsures
;
771 switchExpr
= exprData_getPairA (switchStmt
->edata
);
772 body
= exprData_getPairB (switchStmt
->edata
);
774 if (!exprNode_isDefined (body
))
779 DPRINTF((message("")));
781 if (body
->kind
== XPR_BLOCK
)
782 body
= exprData_getSingle(body
->edata
);
785 constraintsRequires
= constraintList_undefined
;
786 constraintsEnsures
= constraintList_undefined
;
788 lastRequires
= constraintList_makeNew();
789 lastEnsures
= constraintList_makeNew();
793 /* evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
794 exprNode_doGenerateConstraintSwitch (switchExpr
, body
, &lastRequires
,
795 &lastEnsures
, &constraintsRequires
, &constraintsEnsures
);
799 merge current and saved constraint with Logical Or...
800 make a constraint for ensures
803 constraintList_free(switchStmt
->requiresConstraints
);
804 constraintList_free(switchStmt
->ensuresConstraints
);
806 if (constraintList_isDefined(constraintsEnsures
) && constraintList_isDefined(constraintsRequires
))
808 switchStmt
->ensuresConstraints
= constraintList_logicalOr(constraintsEnsures
, lastEnsures
);
809 switchStmt
->requiresConstraints
= constraintList_mergeRequires(constraintsRequires
, lastRequires
);
810 constraintList_free (constraintsRequires
);
811 constraintList_free (constraintsEnsures
);
815 switchStmt
->ensuresConstraints
= constraintList_copy(lastEnsures
);
816 switchStmt
->requiresConstraints
= constraintList_copy(lastRequires
);
819 constraintList_free (lastRequires
);
820 constraintList_free (lastEnsures
);
822 DPRINTF(((message(" exprNode_generateConstraintSwitch returning requires: %s and ensures %s",
823 constraintList_unparse(switchStmt
->requiresConstraints
),
824 constraintList_unparse(switchStmt
->ensuresConstraints
)
829 static exprNode
doSwitch (/*@returned@*/ /*@notnull@*/ exprNode e
)
834 DPRINTF ((message ("doSwitch for: switch (%s) %s",
835 exprNode_unparse (exprData_getPairA (data
)),
836 exprNode_unparse (exprData_getPairB (data
)))));
838 exprNode_generateConstraintSwitch (e
);
842 void exprNode_multiStatement (/*@dependent@*/ exprNode e
)
846 exprNode p
, trueBranch
, falseBranch
;
847 exprNode forPred
, forBody
;
852 DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e
),
853 fileloc_unparse(exprNode_loc(e
)))));
855 if (exprNode_handleError (e
))
866 forPred
= exprData_getPairA (data
);
867 forBody
= exprData_getPairB (data
);
869 /* First generate the constraints */
870 exprNode_generateConstraints (forPred
);
871 exprNode_generateConstraints (forBody
);
874 doFor (e
, forPred
, forBody
);
879 exprNode_generateConstraints (exprData_getTripleInit (data
));
880 test
= exprData_getTripleTest (data
);
881 exprNode_exprTraverse (test
,FALSE
, FALSE
, exprNode_loc(e
));
882 exprNode_generateConstraints (exprData_getTripleInc (data
));
884 if (!exprNode_isError(test
))
886 constraintList temp2
;
887 temp2
= test
->trueEnsuresConstraints
;
888 test
->trueEnsuresConstraints
= exprNode_traverseTrueEnsuresConstraints(test
);
889 constraintList_free(temp2
);
892 exprNode_generateConstraints (exprData_getTripleInc (data
));
896 e1
= exprData_getPairA (data
);
897 e2
= exprData_getPairB (data
);
899 exprNode_exprTraverse (e1
,
900 FALSE
, FALSE
, exprNode_loc(e1
));
902 exprNode_generateConstraints (e2
);
904 e
= doWhile (e
, e1
, e2
);
910 DPRINTF ((exprNode_unparse(e
)));
911 e1
= exprData_getPairA (data
);
912 e2
= exprData_getPairB (data
);
914 exprNode_exprTraverse (e1
, FALSE
, FALSE
, exprNode_loc(e1
));
916 exprNode_generateConstraints (e2
);
917 e
= doIf (e
, e1
, e2
);
921 DPRINTF(("Starting IFELSE"));
922 p
= exprData_getTriplePred (data
);
924 trueBranch
= exprData_getTripleTrue (data
);
925 falseBranch
= exprData_getTripleFalse (data
);
927 exprNode_exprTraverse (p
,
928 FALSE
, FALSE
, exprNode_loc(p
));
929 exprNode_generateConstraints (trueBranch
);
930 exprNode_generateConstraints (falseBranch
);
932 llassert (exprNode_isDefined (p
));
933 temp
= p
->ensuresConstraints
;
934 p
->ensuresConstraints
= exprNode_traverseEnsuresConstraints (p
);
935 constraintList_free(temp
);
937 temp
= p
->requiresConstraints
;
938 p
->requiresConstraints
= exprNode_traverseRequiresConstraints (p
);
939 constraintList_free(temp
);
941 temp
= p
->trueEnsuresConstraints
;
942 p
->trueEnsuresConstraints
= exprNode_traverseTrueEnsuresConstraints(p
);
943 constraintList_free(temp
);
947 DPRINTF((message("p->trueEnsuresConstraints before substitue %s", constraintList_unparse(p
->trueEnsuresConstraints
) )
950 /*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*/
952 p
->trueEnsuresConstraints
= constraintList_substituteFreeTarget (p
->trueEnsuresConstraints
,
953 p
->ensuresConstraints
);
955 DPRINTF(( message ("p->trueEnsuresConstraints after substitue %s", constraintList_unparse(p
->trueEnsuresConstraints
) )
958 temp
= p
->falseEnsuresConstraints
;
959 p
->falseEnsuresConstraints
= exprNode_traverseFalseEnsuresConstraints(p
);
960 constraintList_free(temp
);
962 /*See comment on trueEnsures*/
963 p
->falseEnsuresConstraints
= constraintList_substituteFreeTarget (p
->falseEnsuresConstraints
,
964 p
->ensuresConstraints
);
966 e
= doIfElse (e
, p
, trueBranch
, falseBranch
);
967 DPRINTF(("Done IFELSE"));
972 e2
= (exprData_getPairB (data
));
973 e1
= (exprData_getPairA (data
));
975 DPRINTF((message ("do { %s } while (%s)", exprNode_unparse(e2
), exprNode_unparse(e1
))));
976 exprNode_generateConstraints (e2
);
977 exprNode_generateConstraints (e1
);
978 e
= exprNode_copyConstraints (e
, e2
);
979 DPRINTF ((message ("e = %s ", constraintList_unparse(e
->requiresConstraints
))));
987 tempExpr
= exprData_getSingle (data
);
989 exprNode_generateConstraints (tempExpr
);
991 if (exprNode_isDefined(tempExpr
) )
993 constraintList_free(e
->requiresConstraints
);
994 e
->requiresConstraints
= constraintList_copy (tempExpr
->requiresConstraints
);
995 constraintList_free(e
->ensuresConstraints
);
996 e
->ensuresConstraints
= constraintList_copy (tempExpr
->ensuresConstraints
);
1010 exprNode_stmtList (e
);
1020 static bool lltok_isBoolean_Op (lltok tok
)
1022 /*this should really be a switch statement but
1023 I don't want to violate the abstraction
1024 maybe this should go in lltok.c */
1026 if (lltok_isEqOp (tok
))
1030 if (lltok_isAndOp (tok
))
1036 if (lltok_isOrOp (tok
))
1041 if (lltok_isGt_Op (tok
))
1045 if (lltok_isLt_Op (tok
))
1050 if (lltok_isLe_Op (tok
))
1055 if (lltok_isGe_Op (tok
))
1065 static void exprNode_booleanTraverse (/*@dependent@*/ exprNode e
, /*@unused@*/ bool definatelv
, /*@unused@*/ bool definaterv
, fileloc sequencePoint
)
1071 constraintList tempList
, temp
;
1073 if (exprNode_isUndefined(e
) )
1075 llassert (exprNode_isDefined(e
) );
1081 tok
= exprData_getOpTok (data
);
1082 t1
= exprData_getOpA (data
);
1083 t2
= exprData_getOpB (data
);
1085 /* drl 3/2/2003 we know this because of the type of expression*/
1086 llassert( exprNode_isDefined(t1
) && exprNode_isDefined(t2
) );
1089 tempList
= constraintList_undefined
;
1091 /* arithmetic tests */
1093 if (lltok_isEqOp (tok
))
1095 cons
= constraint_makeEnsureEqual (t1
, t2
, sequencePoint
);
1096 e
->trueEnsuresConstraints
= constraintList_add(e
->trueEnsuresConstraints
, cons
);
1100 if (lltok_isLt_Op (tok
))
1102 cons
= constraint_makeEnsureLessThan (t1
, t2
, sequencePoint
);
1103 e
->trueEnsuresConstraints
= constraintList_add(e
->trueEnsuresConstraints
, cons
);
1104 cons
= constraint_makeEnsureGreaterThanEqual (t1
, t2
, sequencePoint
);
1105 e
->falseEnsuresConstraints
= constraintList_add(e
->falseEnsuresConstraints
, cons
);
1108 if (lltok_isGe_Op (tok
))
1110 cons
= constraint_makeEnsureGreaterThanEqual (t1
, t2
, sequencePoint
);
1111 e
->trueEnsuresConstraints
= constraintList_add(e
->trueEnsuresConstraints
, cons
);
1113 cons
= constraint_makeEnsureLessThan (t1
, t2
, sequencePoint
);
1114 e
->falseEnsuresConstraints
= constraintList_add(e
->falseEnsuresConstraints
, cons
);
1117 if (lltok_isGt_Op (tok
))
1119 cons
= constraint_makeEnsureGreaterThan (t1
, t2
, sequencePoint
);
1120 e
->trueEnsuresConstraints
= constraintList_add(e
->trueEnsuresConstraints
, cons
);
1121 cons
= constraint_makeEnsureLessThanEqual (t1
, t2
, sequencePoint
);
1122 e
->falseEnsuresConstraints
= constraintList_add(e
->falseEnsuresConstraints
, cons
);
1125 if (lltok_isLe_Op (tok
))
1127 cons
= constraint_makeEnsureLessThanEqual (t1
, t2
, sequencePoint
);
1128 e
->trueEnsuresConstraints
= constraintList_add(e
->trueEnsuresConstraints
, cons
);
1130 cons
= constraint_makeEnsureGreaterThan (t1
, t2
, sequencePoint
);
1131 e
->falseEnsuresConstraints
= constraintList_add(e
->falseEnsuresConstraints
, cons
);
1134 /* Logical operations */
1136 if (lltok_isAndOp (tok
))
1139 tempList
= constraintList_copy (t1
->trueEnsuresConstraints
);
1140 tempList
= constraintList_addList (tempList
, t2
->trueEnsuresConstraints
);
1141 e
->trueEnsuresConstraints
= constraintList_addListFree(e
->trueEnsuresConstraints
, tempList
);
1143 /* false ensures: fens t1 or tens t1 and fens t2 */
1144 tempList
= constraintList_copy (t1
->trueEnsuresConstraints
);
1145 tempList
= constraintList_addList (tempList
, t2
->falseEnsuresConstraints
);
1147 tempList
= constraintList_logicalOr (tempList
, t1
->falseEnsuresConstraints
);
1148 constraintList_free (temp
);
1150 /* evans - was constraintList_addList - memory leak detected by splint */
1151 e
->falseEnsuresConstraints
= constraintList_addListFree (e
->falseEnsuresConstraints
, tempList
);
1153 else if (lltok_isOrOp (tok
))
1156 tempList
= constraintList_copy (t1
->falseEnsuresConstraints
);
1157 tempList
= constraintList_addList (tempList
, t2
->falseEnsuresConstraints
);
1158 e
->falseEnsuresConstraints
= constraintList_addListFree(e
->falseEnsuresConstraints
, tempList
);
1160 /* true ensures: tens t1 or fens t1 and tens t2 */
1161 tempList
= constraintList_copy (t1
->falseEnsuresConstraints
);
1162 tempList
= constraintList_addList (tempList
, t2
->trueEnsuresConstraints
);
1165 tempList
= constraintList_logicalOr (tempList
, t1
->trueEnsuresConstraints
);
1166 constraintList_free(temp
);
1168 e
->trueEnsuresConstraints
= constraintList_addListFree(e
->trueEnsuresConstraints
, tempList
);
1169 tempList
= constraintList_undefined
;
1173 DPRINTF((message("%s is not a boolean operation", lltok_unparse(tok
))));
1177 static void exprNode_exprTraverse (/*@dependent@*/ exprNode e
,
1178 bool definatelv
, bool definaterv
,
1179 /*@observer@*/ /*@temp@*/ fileloc sequencePoint
)
1181 exprNode t1
, t2
, fcn
;
1185 constraintList temp
;
1187 if (exprNode_isError(e
))
1192 DPRINTF (("exprNode_exprTraverse analyzing %s at %s",
1193 exprNode_unparse (e
),
1194 fileloc_unparse (exprNode_loc (e
))));
1196 if (exprNode_isUnhandled (e
))
1206 t1
= exprData_getSingle (data
);
1207 exprNode_exprTraverse (t1
, definatelv
, definaterv
, sequencePoint
);
1208 e
= exprNode_copyConstraints (e
, t1
);
1215 t1
= (exprData_getPairA (data
));
1216 t2
= (exprData_getPairB (data
));
1217 cons
= constraint_makeWriteSafeExprNode (t1
, t2
);
1221 t1
= (exprData_getPairA (data
));
1222 t2
= (exprData_getPairB (data
));
1223 cons
= constraint_makeReadSafeExprNode (t1
, t2
);
1226 e
->requiresConstraints
= constraintList_add(e
->requiresConstraints
, cons
);
1227 cons
= constraint_makeEnsureMaxReadAtLeast (t1
, t2
, sequencePoint
);
1228 e
->ensuresConstraints
= constraintList_add(e
->ensuresConstraints
, cons
);
1230 cons
= constraint_makeEnsureLteMaxRead (t2
, t1
);
1231 e
->trueEnsuresConstraints
= constraintList_add(e
->trueEnsuresConstraints
, cons
);
1233 exprNode_exprTraverse (exprData_getPairA (data
), FALSE
, TRUE
, sequencePoint
);
1234 exprNode_exprTraverse (exprData_getPairB (data
), FALSE
, TRUE
, sequencePoint
);
1239 exprNode_exprTraverse (exprData_getUopNode (e
->edata
), definatelv
, definaterv
, sequencePoint
);
1243 t2
= exprData_getInitNode (data
);
1245 DPRINTF (("initialization ==> %s",exprNode_unparse (t2
)));
1247 exprNode_exprTraverse (t2
, definatelv
, TRUE
, sequencePoint
);
1249 /* This test is nessecary because some expressions generate a null expression node.
1250 function pointer do that -- drl */
1252 if (!exprNode_isError (e
) && !exprNode_isError (t2
))
1254 cons
= constraint_makeEnsureEqual (e
, t2
, sequencePoint
);
1255 e
->ensuresConstraints
= constraintList_add(e
->ensuresConstraints
, cons
);
1261 t1
= exprData_getOpA (data
);
1262 t2
= exprData_getOpB (data
);
1263 DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1
->ensuresConstraints
)));
1264 DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2
->ensuresConstraints
)));
1265 exprNode_exprTraverse (t1
, TRUE
, definaterv
, sequencePoint
);
1266 DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1
->ensuresConstraints
)));
1267 DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2
->ensuresConstraints
)));
1268 exprNode_exprTraverse (t2
, definatelv
, TRUE
, sequencePoint
);
1269 DPRINTF (("Assignment constraints t1: %s", constraintList_unparse (t1
->ensuresConstraints
)));
1270 DPRINTF (("Assignment constraints t2: %s", constraintList_unparse (t2
->ensuresConstraints
)));
1272 /* this test is nessecary because some expressions generate a null expression node.
1273 function pointer do that -- drl */
1275 if ((!exprNode_isError (t1
)) && (!exprNode_isError(t2
)))
1277 cons
= constraint_makeEnsureEqual (t1
, t2
, sequencePoint
);
1278 DPRINTF (("Ensure equal constraint: %s", constraint_unparse (cons
)));
1279 e
->ensuresConstraints
= constraintList_add (e
->ensuresConstraints
, cons
);
1280 DPRINTF (("Assignment constraints: %s", constraintList_unparse (e
->ensuresConstraints
)));
1284 t1
= exprData_getOpA (data
);
1285 t2
= exprData_getOpB (data
);
1286 tok
= exprData_getOpTok (data
);
1288 if (lltok_getTok (tok
) == ADD_ASSIGN
)
1290 exprNode_exprTraverse (t1
, TRUE
, definaterv
, sequencePoint
);
1291 exprNode_exprTraverse (t2
, definatelv
, TRUE
, sequencePoint
);
1293 cons
= constraint_makeAddAssign (t1
, t2
, sequencePoint
);
1294 e
->ensuresConstraints
= constraintList_add(e
->ensuresConstraints
, cons
);
1296 else if (lltok_getTok (tok
) == SUB_ASSIGN
)
1298 exprNode_exprTraverse (t1
, TRUE
, definaterv
, sequencePoint
);
1299 exprNode_exprTraverse (t2
, definatelv
, TRUE
, sequencePoint
);
1301 cons
= constraint_makeSubtractAssign (t1
, t2
, sequencePoint
);
1302 e
->ensuresConstraints
= constraintList_add(e
->ensuresConstraints
, cons
);
1306 exprNode_exprTraverse (t1
, definatelv
, definaterv
, sequencePoint
);
1307 exprNode_exprTraverse (t2
, definatelv
, definaterv
, sequencePoint
);
1310 if (lltok_isBoolean_Op (tok
))
1311 exprNode_booleanTraverse (e
, definatelv
, definaterv
, sequencePoint
);
1315 /*drl 4-11-03 I think this is the same as the next case...*/
1321 C standard says operand to sizeof isn't evaluated unless
1322 its a variable length array. So we don't generate constraints.
1328 fcn
= exprData_getFcn(data
);
1330 exprNode_exprTraverse (fcn
, definatelv
, definaterv
, sequencePoint
);
1331 DPRINTF (("Got call that %s (%s)",
1332 exprNode_unparse(fcn
), exprNodeList_unparse (exprData_getArgs (data
))));
1334 llassert( exprNode_isDefined(fcn
) );
1336 fcn
->requiresConstraints
=
1337 constraintList_addListFree (fcn
->requiresConstraints
,
1338 checkCall (fcn
, exprData_getArgs (data
)));
1340 fcn
->ensuresConstraints
=
1341 constraintList_addListFree (fcn
->ensuresConstraints
,
1342 exprNode_getPostConditions(fcn
, exprData_getArgs (data
),e
));
1344 t1
= exprNode_createNew (exprNode_getType (e
));
1345 checkArgumentList (t1
, exprData_getArgs(data
), sequencePoint
);
1346 exprNode_mergeResolve (e
, t1
, fcn
);
1351 exprNode_exprTraverse (exprData_getSingle (data
), definatelv
, definaterv
, sequencePoint
);
1354 case XPR_NULLRETURN
:
1360 exprNode_exprTraverse (exprData_getFieldNode (data
), definatelv
, definaterv
, sequencePoint
);
1364 exprNode_exprTraverse (exprData_getFieldNode (data
), definatelv
, definaterv
, sequencePoint
);
1367 case XPR_STRINGLITERAL
:
1376 t1
= exprData_getUopNode(data
);
1379 /* drl 3/2/2003 we know this because of the type of expression*/
1380 llassert( exprNode_isDefined(t1
) );
1383 tok
= (exprData_getUopTok (data
));
1384 exprNode_exprTraverse (t1
, definatelv
, definaterv
, sequencePoint
);
1385 /*handle * pointer access */
1386 if (lltok_isIncOp (tok
))
1388 DPRINTF(("doing ++(var)"));
1389 t1
= exprData_getUopNode (data
);
1390 cons
= constraint_makeMaxSetSideEffectPostIncrement (t1
, sequencePoint
);
1391 e
->ensuresConstraints
= constraintList_add (e
->ensuresConstraints
, cons
);
1393 else if (lltok_isDecOp (tok
))
1395 DPRINTF(("doing --(var)"));
1396 t1
= exprData_getUopNode (data
);
1397 cons
= constraint_makeMaxSetSideEffectPostDecrement (t1
, sequencePoint
);
1398 e
->ensuresConstraints
= constraintList_add (e
->ensuresConstraints
, cons
);
1400 else if (lltok_isMult(tok
))
1404 cons
= constraint_makeWriteSafeInt (t1
, 0);
1408 cons
= constraint_makeReadSafeInt (t1
, 0);
1410 e
->requiresConstraints
= constraintList_add(e
->requiresConstraints
, cons
);
1412 else if (lltok_isNotOp (tok
))
1415 constraintList_free(e
->trueEnsuresConstraints
);
1417 e
->trueEnsuresConstraints
= constraintList_copy (t1
->falseEnsuresConstraints
);
1418 constraintList_free(e
->falseEnsuresConstraints
);
1419 e
->falseEnsuresConstraints
= constraintList_copy (t1
->trueEnsuresConstraints
);
1422 else if (lltok_isAmpersand_Op (tok
))
1426 else if (lltok_isMinus_Op (tok
))
1430 else if (lltok_isExcl_Op (tok
))
1434 else if (lltok_isTilde_Op (tok
))
1440 llcontbug (message("Unsupported preop in %s", exprNode_unparse(e
)));
1446 exprNode_exprTraverse (exprData_getUopNode (data
), TRUE
,
1447 definaterv
, sequencePoint
);
1449 if (lltok_isIncOp (exprData_getUopTok (data
)))
1451 DPRINTF(("doing ++"));
1452 t1
= exprData_getUopNode (data
);
1453 cons
= constraint_makeMaxSetSideEffectPostIncrement (t1
, sequencePoint
);
1454 e
->ensuresConstraints
= constraintList_add (e
->ensuresConstraints
, cons
);
1456 if (lltok_isDecOp (exprData_getUopTok (data
)))
1458 DPRINTF(("doing --"));
1459 t1
= exprData_getUopNode (data
);
1460 cons
= constraint_makeMaxSetSideEffectPostDecrement (t1
, sequencePoint
);
1461 e
->ensuresConstraints
= constraintList_add (e
->ensuresConstraints
, cons
);
1466 t2
= exprData_getCastNode (data
);
1467 DPRINTF ((message ("Examining cast (%q)%s",
1468 qtype_unparse (exprData_getCastType (data
)),
1469 exprNode_unparse (t2
))
1471 exprNode_exprTraverse (t2
, definatelv
, definaterv
, sequencePoint
);
1477 exprNode pred
, trueBranch
, falseBranch
;
1479 pred
= exprData_getTriplePred (data
);
1480 trueBranch
= exprData_getTripleTrue (data
);
1481 falseBranch
= exprData_getTripleFalse (data
);
1483 llassert (exprNode_isDefined (pred
));
1484 llassert (exprNode_isDefined (trueBranch
));
1485 llassert (exprNode_isDefined (falseBranch
));
1487 exprNode_exprTraverse (pred
, FALSE
, TRUE
, sequencePoint
);
1489 temp
= pred
->ensuresConstraints
;
1490 pred
->ensuresConstraints
= exprNode_traverseEnsuresConstraints(pred
);
1491 constraintList_free(temp
);
1493 temp
= pred
->requiresConstraints
;
1494 pred
->requiresConstraints
= exprNode_traverseRequiresConstraints(pred
);
1495 constraintList_free(temp
);
1497 temp
= pred
->trueEnsuresConstraints
;
1498 pred
->trueEnsuresConstraints
= exprNode_traverseTrueEnsuresConstraints(pred
);
1499 constraintList_free(temp
);
1501 temp
= pred
->falseEnsuresConstraints
;
1502 pred
->falseEnsuresConstraints
= exprNode_traverseFalseEnsuresConstraints(pred
);
1503 constraintList_free(temp
);
1505 exprNode_exprTraverse (trueBranch
, FALSE
, TRUE
, sequencePoint
);
1507 temp
= trueBranch
->ensuresConstraints
;
1508 trueBranch
->ensuresConstraints
= exprNode_traverseEnsuresConstraints(trueBranch
);
1509 constraintList_free(temp
);
1511 temp
= trueBranch
->requiresConstraints
;
1512 trueBranch
->requiresConstraints
= exprNode_traverseRequiresConstraints(trueBranch
);
1513 constraintList_free(temp
);
1515 temp
= trueBranch
->trueEnsuresConstraints
;
1516 trueBranch
->trueEnsuresConstraints
= exprNode_traverseTrueEnsuresConstraints(trueBranch
);
1517 constraintList_free(temp
);
1519 temp
= trueBranch
->falseEnsuresConstraints
;
1520 trueBranch
->falseEnsuresConstraints
= exprNode_traverseFalseEnsuresConstraints(trueBranch
);
1521 constraintList_free(temp
);
1523 exprNode_exprTraverse (falseBranch
, FALSE
, TRUE
, sequencePoint
);
1525 temp
= falseBranch
->ensuresConstraints
;
1526 falseBranch
->ensuresConstraints
= exprNode_traverseEnsuresConstraints(falseBranch
);
1527 constraintList_free(temp
);
1530 temp
= falseBranch
->requiresConstraints
;
1531 falseBranch
->requiresConstraints
= exprNode_traverseRequiresConstraints(falseBranch
);
1532 constraintList_free(temp
);
1534 temp
= falseBranch
->trueEnsuresConstraints
;
1535 falseBranch
->trueEnsuresConstraints
= exprNode_traverseTrueEnsuresConstraints(falseBranch
);
1536 constraintList_free(temp
);
1538 temp
= falseBranch
->falseEnsuresConstraints
;
1539 falseBranch
->falseEnsuresConstraints
= exprNode_traverseFalseEnsuresConstraints(falseBranch
);
1540 constraintList_free(temp
);
1542 /* if pred is true e equals true otherwise pred equals false */
1544 cons
= constraint_makeEnsureEqual (e
, trueBranch
, sequencePoint
);
1545 trueBranch
->ensuresConstraints
= constraintList_add(trueBranch
->ensuresConstraints
, cons
);
1547 cons
= constraint_makeEnsureEqual (e
, trueBranch
, sequencePoint
);
1548 falseBranch
->ensuresConstraints
= constraintList_add(falseBranch
->ensuresConstraints
, cons
);
1550 e
= doIfElse (e
, pred
, trueBranch
, falseBranch
);
1555 t1
= exprData_getPairA (data
);
1556 t2
= exprData_getPairB (data
);
1557 /* we essiantially treat this like expr1; expr2
1558 of course sequencePoint isn't adjusted so this isn't completely accurate
1561 exprNode_exprTraverse (t1
, FALSE
, FALSE
, sequencePoint
);
1562 exprNode_exprTraverse (t2
, definatelv
, definaterv
, sequencePoint
);
1563 exprNode_mergeResolve (e
, t1
, t2
);
1570 e
->requiresConstraints
= constraintList_preserveOrig (e
->requiresConstraints
);
1571 e
->ensuresConstraints
= constraintList_preserveOrig (e
->ensuresConstraints
);
1572 e
->requiresConstraints
= constraintList_addGeneratingExpr (e
->requiresConstraints
, e
);
1573 e
->ensuresConstraints
= constraintList_addGeneratingExpr (e
->ensuresConstraints
, e
);
1574 e
->requiresConstraints
= constraintList_removeSurpressed (e
->requiresConstraints
);
1576 DPRINTF (("ensures constraints for %s are %s",
1577 exprNode_unparse(e
), constraintList_unparseDetailed (e
->ensuresConstraints
)));
1579 DPRINTF (("Requires constraints for %s are %s", exprNode_unparse(e
),
1580 constraintList_unparseDetailed(e
->ensuresConstraints
)));
1582 DPRINTF (("trueEnsures constraints for %s are %s", exprNode_unparse(e
),
1583 constraintList_unparseDetailed(e
->trueEnsuresConstraints
)));
1585 DPRINTF (("falseEnsures constraints for %s are %s", exprNode_unparse(e
),
1586 constraintList_unparseDetailed(e
->falseEnsuresConstraints
)));
1591 constraintList
exprNode_traverseTrueEnsuresConstraints (exprNode e
)
1597 if (exprNode_handleError (e
))
1599 ret
= constraintList_makeNew();
1603 ret
= constraintList_copy (e
->trueEnsuresConstraints
);
1610 t1
= exprData_getSingle (data
);
1611 ret
= constraintList_addListFree (ret
, exprNode_traverseTrueEnsuresConstraints (t1
));
1616 ret
= constraintList_addListFree (ret
,
1617 exprNode_traverseTrueEnsuresConstraints
1618 (exprData_getPairA (data
)));
1620 ret
= constraintList_addListFree (ret
,
1621 exprNode_traverseTrueEnsuresConstraints
1622 (exprData_getPairB (data
)));
1626 ret
= constraintList_addListFree (ret
,
1627 exprNode_traverseTrueEnsuresConstraints
1628 (exprData_getUopNode (data
)));
1632 ret
= constraintList_addListFree (ret
, exprNode_traverseTrueEnsuresConstraints
1633 (exprData_getUopNode (data
)));
1637 ret
= constraintList_addListFree (ret
,
1638 exprNode_traverseTrueEnsuresConstraints
1639 (exprData_getInitNode (data
)));
1644 ret
= constraintList_addListFree (ret
,
1645 exprNode_traverseTrueEnsuresConstraints
1646 (exprData_getOpA (data
)));
1648 ret
= constraintList_addListFree (ret
,
1649 exprNode_traverseTrueEnsuresConstraints
1650 (exprData_getOpB (data
)));
1653 ret
= constraintList_addListFree (ret
,
1654 exprNode_traverseTrueEnsuresConstraints
1655 (exprData_getOpA (data
)));
1657 ret
= constraintList_addListFree (ret
,
1658 exprNode_traverseTrueEnsuresConstraints
1659 (exprData_getOpB (data
)));
1666 ret
= constraintList_addListFree (ret
,
1667 exprNode_traverseTrueEnsuresConstraints
1668 (exprData_getSingle (data
)));
1672 ret
= constraintList_addListFree (ret
,
1673 exprNode_traverseTrueEnsuresConstraints
1674 (exprData_getFcn (data
)));
1678 ret
= constraintList_addListFree (ret
,
1679 exprNode_traverseTrueEnsuresConstraints
1680 (exprData_getSingle (data
)));
1683 case XPR_NULLRETURN
:
1687 ret
= constraintList_addListFree (ret
,
1688 exprNode_traverseTrueEnsuresConstraints
1689 (exprData_getFieldNode (data
)));
1693 ret
= constraintList_addListFree (ret
,
1694 exprNode_traverseTrueEnsuresConstraints
1695 (exprData_getFieldNode (data
)));
1698 case XPR_STRINGLITERAL
:
1705 ret
= constraintList_addListFree (ret
,
1706 exprNode_traverseTrueEnsuresConstraints
1707 (exprData_getUopNode (data
)));
1712 ret
= constraintList_addListFree (ret
,
1713 exprNode_traverseTrueEnsuresConstraints
1714 (exprData_getCastNode (data
)));
1724 constraintList
exprNode_traverseFalseEnsuresConstraints (exprNode e
)
1730 if (exprNode_handleError (e
))
1732 ret
= constraintList_makeNew();
1736 ret
= constraintList_copy (e
->falseEnsuresConstraints
);
1742 t1
= exprData_getSingle (data
);
1743 ret
= constraintList_addListFree (ret
,exprNode_traverseFalseEnsuresConstraints (t1
));
1748 ret
= constraintList_addListFree (ret
,
1749 exprNode_traverseFalseEnsuresConstraints
1750 (exprData_getPairA (data
)));
1752 ret
= constraintList_addListFree (ret
,
1753 exprNode_traverseFalseEnsuresConstraints
1754 (exprData_getPairB (data
)));
1758 ret
= constraintList_addListFree (ret
,
1759 exprNode_traverseFalseEnsuresConstraints
1760 (exprData_getUopNode (data
)));
1764 ret
= constraintList_addListFree (ret
, exprNode_traverseFalseEnsuresConstraints
1765 (exprData_getUopNode (data
)));
1768 ret
= constraintList_addListFree (ret
,
1769 exprNode_traverseFalseEnsuresConstraints
1770 ( exprData_getInitNode (data
)));
1774 ret
= constraintList_addListFree (ret
,
1775 exprNode_traverseFalseEnsuresConstraints
1776 (exprData_getOpA (data
)));
1778 ret
= constraintList_addListFree (ret
,
1779 exprNode_traverseFalseEnsuresConstraints
1780 (exprData_getOpB (data
)));
1783 ret
= constraintList_addListFree (ret
,
1784 exprNode_traverseFalseEnsuresConstraints
1785 (exprData_getOpA (data
)));
1787 ret
= constraintList_addListFree (ret
,
1788 exprNode_traverseFalseEnsuresConstraints
1789 (exprData_getOpB (data
)));
1796 ret
= constraintList_addListFree (ret
,
1797 exprNode_traverseFalseEnsuresConstraints
1798 (exprData_getSingle (data
)));
1802 ret
= constraintList_addListFree (ret
,
1803 exprNode_traverseFalseEnsuresConstraints
1804 (exprData_getFcn (data
)));
1808 ret
= constraintList_addListFree (ret
,
1809 exprNode_traverseFalseEnsuresConstraints
1810 (exprData_getSingle (data
)));
1813 case XPR_NULLRETURN
:
1817 ret
= constraintList_addListFree (ret
,
1818 exprNode_traverseFalseEnsuresConstraints
1819 (exprData_getFieldNode (data
)));
1823 ret
= constraintList_addListFree (ret
,
1824 exprNode_traverseFalseEnsuresConstraints
1825 (exprData_getFieldNode (data
)));
1828 case XPR_STRINGLITERAL
:
1835 ret
= constraintList_addListFree (ret
,
1836 exprNode_traverseFalseEnsuresConstraints
1837 (exprData_getUopNode (data
)));
1842 ret
= constraintList_addListFree (ret
,
1843 exprNode_traverseFalseEnsuresConstraints
1844 (exprData_getCastNode (data
)));
1855 /* walk down the tree and get all requires Constraints in each subexpression*/
1856 static /*@only@*/ constraintList
exprNode_traverseRequiresConstraints (exprNode e
)
1862 if (exprNode_handleError (e
))
1864 ret
= constraintList_makeNew();
1868 ret
= constraintList_copy (e
->requiresConstraints
);
1874 t1
= exprData_getSingle (data
);
1875 ret
= constraintList_addListFree (ret
, exprNode_traverseRequiresConstraints (t1
));
1880 ret
= constraintList_addListFree (ret
,
1881 exprNode_traverseRequiresConstraints
1882 (exprData_getPairA (data
)));
1884 ret
= constraintList_addListFree (ret
,
1885 exprNode_traverseRequiresConstraints
1886 (exprData_getPairB (data
)));
1890 ret
= constraintList_addListFree (ret
,
1891 exprNode_traverseRequiresConstraints
1892 (exprData_getUopNode (data
)));
1896 ret
= constraintList_addListFree (ret
, exprNode_traverseRequiresConstraints
1897 (exprData_getUopNode (data
)));
1900 ret
= constraintList_addListFree (ret
,
1901 exprNode_traverseRequiresConstraints
1902 (exprData_getInitNode (data
)));
1906 ret
= constraintList_addListFree (ret
,
1907 exprNode_traverseRequiresConstraints
1908 (exprData_getOpA (data
)));
1910 ret
= constraintList_addListFree (ret
,
1911 exprNode_traverseRequiresConstraints
1912 (exprData_getOpB (data
)));
1915 ret
= constraintList_addListFree (ret
,
1916 exprNode_traverseRequiresConstraints
1917 (exprData_getOpA (data
)));
1919 ret
= constraintList_addListFree (ret
,
1920 exprNode_traverseRequiresConstraints
1921 (exprData_getOpB (data
)));
1928 ret
= constraintList_addListFree (ret
,
1929 exprNode_traverseRequiresConstraints
1930 (exprData_getSingle (data
)));
1934 ret
= constraintList_addListFree (ret
,
1935 exprNode_traverseRequiresConstraints
1936 (exprData_getFcn (data
)));
1940 ret
= constraintList_addListFree (ret
,
1941 exprNode_traverseRequiresConstraints
1942 (exprData_getSingle (data
)));
1945 case XPR_NULLRETURN
:
1949 ret
= constraintList_addListFree (ret
,
1950 exprNode_traverseRequiresConstraints
1951 (exprData_getFieldNode (data
)));
1955 ret
= constraintList_addListFree (ret
,
1956 exprNode_traverseRequiresConstraints
1957 (exprData_getFieldNode (data
)));
1960 case XPR_STRINGLITERAL
:
1967 ret
= constraintList_addListFree (ret
,
1968 exprNode_traverseRequiresConstraints
1969 (exprData_getUopNode (data
)));
1974 ret
= constraintList_addListFree (ret
,
1975 exprNode_traverseRequiresConstraints
1976 (exprData_getCastNode (data
)));
1987 /* walk down the tree and get all Ensures Constraints in each subexpression*/
1988 static /*@only@*/ constraintList
exprNode_traverseEnsuresConstraints (exprNode e
)
1994 if (exprNode_handleError (e
))
1996 ret
= constraintList_makeNew();
2000 ret
= constraintList_copy (e
->ensuresConstraints
);
2004 DPRINTF ((message ("exprnode_traversEnsuresConstraints call for %s with "
2005 "constraintList of %s",
2006 exprNode_unparse (e
),
2007 constraintList_unparse(e
->ensuresConstraints
)
2015 t1
= exprData_getSingle (data
);
2016 ret
= constraintList_addListFree (ret
,exprNode_traverseEnsuresConstraints (t1
));
2020 ret
= constraintList_addListFree (ret
,
2021 exprNode_traverseEnsuresConstraints
2022 (exprData_getPairA (data
)));
2024 ret
= constraintList_addListFree (ret
,
2025 exprNode_traverseEnsuresConstraints
2026 (exprData_getPairB (data
)));
2029 ret
= constraintList_addListFree (ret
,
2030 exprNode_traverseEnsuresConstraints
2031 (exprData_getUopNode (data
)));
2035 ret
= constraintList_addListFree (ret
, exprNode_traverseEnsuresConstraints
2036 (exprData_getUopNode (data
)));
2040 ret
= constraintList_addListFree (ret
,
2041 exprNode_traverseEnsuresConstraints
2042 (exprData_getInitNode (data
)));
2047 ret
= constraintList_addListFree (ret
,
2048 exprNode_traverseEnsuresConstraints
2049 (exprData_getOpA (data
)));
2051 ret
= constraintList_addListFree (ret
,
2052 exprNode_traverseEnsuresConstraints
2053 (exprData_getOpB (data
)));
2056 ret
= constraintList_addListFree (ret
,
2057 exprNode_traverseEnsuresConstraints
2058 (exprData_getOpA (data
)));
2060 ret
= constraintList_addListFree (ret
,
2061 exprNode_traverseEnsuresConstraints
2062 (exprData_getOpB (data
)));
2068 ret
= constraintList_addListFree (ret
,
2069 exprNode_traverseEnsuresConstraints
2070 (exprData_getSingle (data
)));
2073 ret
= constraintList_addListFree (ret
,
2074 exprNode_traverseEnsuresConstraints
2075 (exprData_getFcn (data
)));
2078 ret
= constraintList_addListFree (ret
,
2079 exprNode_traverseEnsuresConstraints
2080 (exprData_getSingle (data
)));
2082 case XPR_NULLRETURN
:
2085 ret
= constraintList_addListFree (ret
,
2086 exprNode_traverseEnsuresConstraints
2087 (exprData_getFieldNode (data
)));
2090 ret
= constraintList_addListFree (ret
,
2091 exprNode_traverseEnsuresConstraints
2092 (exprData_getFieldNode (data
)));
2094 case XPR_STRINGLITERAL
:
2099 ret
= constraintList_addListFree (ret
,
2100 exprNode_traverseEnsuresConstraints
2101 (exprData_getUopNode (data
)));
2104 ret
= constraintList_addListFree (ret
,
2105 exprNode_traverseEnsuresConstraints
2106 (exprData_getCastNode (data
)));
2112 DPRINTF((message ("exprnode_traversEnsuresConstraints call for %s with "
2113 "constraintList of is returning %s",
2114 exprNode_unparse (e
),
2115 constraintList_unparse(ret
))));
2120 /*drl moved out of constraintResolve.c 07-02-001 */
2121 void checkArgumentList (/*@out@*/ exprNode temp
, exprNodeList arglist
,
2122 fileloc sequencePoint
)
2125 llassert(temp
!= NULL
);
2127 temp
->requiresConstraints
= constraintList_makeNew();
2128 temp
->ensuresConstraints
= constraintList_makeNew();
2129 temp
->trueEnsuresConstraints
= constraintList_makeNew();
2130 temp
->falseEnsuresConstraints
= constraintList_makeNew();
2132 exprNodeList_elements (arglist
, el
)
2134 constraintList temp2
;
2136 llassert(exprNode_isDefined(el
) );
2138 exprNode_exprTraverse (el
, FALSE
, FALSE
, sequencePoint
);
2139 temp2
= el
->requiresConstraints
;
2140 el
->requiresConstraints
= exprNode_traverseRequiresConstraints(el
);
2141 constraintList_free(temp2
);
2143 temp2
= el
->ensuresConstraints
;
2144 el
->ensuresConstraints
= exprNode_traverseEnsuresConstraints(el
);
2145 constraintList_free(temp2
);
2147 temp
->requiresConstraints
= constraintList_addList(temp
->requiresConstraints
,
2148 el
->requiresConstraints
);
2150 temp
->ensuresConstraints
= constraintList_addList(temp
->ensuresConstraints
,
2151 el
->ensuresConstraints
);
2153 end_exprNodeList_elements
;
2157 /*drl moved out of constraintResolve.c 07-03-001 */
2158 static constraintList
exprNode_getPostConditions (exprNode fcn
, exprNodeList arglist
, exprNode fcnCall
)
2160 constraintList postconditions
;
2162 DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn
), exprNodeList_unparse (arglist
))));
2164 temp
= exprNode_getUentry (fcn
);
2166 postconditions
= uentry_getFcnPostconditions (temp
);
2168 if (constraintList_isDefined (postconditions
))
2170 postconditions
= constraintList_doSRefFixConstraintParam (postconditions
, arglist
);
2171 postconditions
= constraintList_doFixResult (postconditions
, fcnCall
);
2175 postconditions
= constraintList_makeNew();
2178 return postconditions
;
2182 comment this out for now
2183 we'll include it in a production release when its stable...
2185 void findStructs (exprNodeList arglist)
2191 message("doing findStructs: %s", exprNodeList_unparse(arglist))
2195 exprNodeList_elements(arglist, expr)
2197 ct = exprNode_getType(expr);
2199 rt = ctype_realType (ct);
2201 if (ctype_isStruct (rt))
2202 DPRINTF((message("Found structure %s", exprNode_unparse(expr))
2204 if (hasInvariants(ct))
2206 constraintList invars;
2208 invars = getInvariants(ct);
2211 DPRINTF((message ("findStructs has invariants %s ", constraintList_unparse (invars))
2214 invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct);
2217 DPRINTF((message ("findStructs finded invariants to be %s ", constraintList_unparse (invars))
2221 end_exprNodeList_elements;
2226 /*drl moved out of constraintResolve.c 07-02-001 */
2227 constraintList
checkCall (/*@dependent@*/ exprNode fcn
, exprNodeList arglist
)
2229 constraintList preconditions
;
2231 DPRINTF((message ("Got call that %s (%s) ", exprNode_unparse(fcn
), exprNodeList_unparse (arglist
))));
2233 temp
= exprNode_getUentry (fcn
);
2235 preconditions
= uentry_getFcnPreconditions (temp
);
2237 if (constraintList_isDefined(preconditions
))
2239 preconditions
= constraintList_togglePost (preconditions
);
2240 preconditions
= constraintList_preserveCallInfo(preconditions
, fcn
);
2241 preconditions
= constraintList_doSRefFixConstraintParam (preconditions
, arglist
);
2245 if (constraintList_isUndefined(preconditions
))
2246 preconditions
= constraintList_makeNew();
2249 if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS
))
2253 uentryList_elements (arglist, el)
2256 DPRINTF((message("setImplicitfcnConstraints doing: %s", uentry_unparse(el) ) ));
2258 s = uentry_getSref(el);
2259 if (sRef_isReference (s) )
2261 DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
2265 DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
2268 //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0
2269 c = constraint_makeSRefWriteSafeInt (s, 0);
2271 implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
2273 //drl 10/23/2002 added support for out
2274 if (!uentry_isOut(el) )
2276 c = constraint_makeSRefReadSafeInt (s, 0);
2277 implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
2285 DPRINTF ((message("Done checkCall\n")));
2286 DPRINTF ((message("Returning list %q ", constraintList_unparseDetailed(preconditions
))));
2289 drl we're going to comment this out for now
2290 we'll include it if we're sure it's working
2292 findStructs(arglist);
2295 return preconditions
;
2298 /*drl added this function 10.29.001
2299 takes an exprNode of the form const + const
2303 I'm a bit nervous about modifying the exprNode
2304 but this is the easy way to do this
2305 If I have time I'd like to cause the exprNode to get created correctly in the first place */
2306 void exprNode_findValue(exprNode e
)
2313 llassert(exprNode_isDefined(e
) );
2317 if (exprNode_hasValue(e
))
2320 if (e
->kind
== XPR_OP
)
2322 t1
= exprData_getOpA (data
);
2323 t2
= exprData_getOpB (data
);
2324 tok
= exprData_getOpTok (data
);
2326 exprNode_findValue(t1
);
2327 exprNode_findValue(t2
);
2329 if (!(exprNode_knownIntValue(t1
) && (exprNode_knownIntValue(t2
))))
2332 if (lltok_isPlus_Op (tok
))
2336 v1
= exprNode_getLongValue(t1
);
2337 v2
= exprNode_getLongValue(t2
);
2339 if (multiVal_isDefined(e
->val
))
2340 multiVal_free (e
->val
);
2342 e
->val
= multiVal_makeInt (v1
+ v2
);
2345 if (lltok_isMinus_Op (tok
))
2349 v1
= exprNode_getLongValue(t1
);
2350 v2
= exprNode_getLongValue(t2
);
2352 if (multiVal_isDefined(e
->val
))
2354 multiVal_free (e
->val
);
2357 e
->val
= multiVal_makeInt (v1
- v2
);
2360 /*drl I should really do * and / at some point */