return;
}
- /*@i22*/
DPRINTF((message("")));
if (body->kind == XPR_BLOCK)
body = exprData_getSingle(body->edata);
- /*
+
constraintsRequires = constraintList_undefined;
constraintsEnsures = constraintList_undefined;
lastRequires = constraintList_makeNew();
lastEnsures = constraintList_makeNew();
- */
+
/*@-mustfree@*/
- /*@i6534 - evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
+ /* evans 2002-01-01: spurious warnings for these becuase of stack allocated storage */
exprNode_doGenerateConstraintSwitch (switchExpr, body, &lastRequires,
&lastEnsures, &constraintsRequires, &constraintsEnsures);
/*@=mustfree@*/
exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
- /*@i325 Should check which is array/index. */
break;
case XPR_PARENS:
break;
case XPR_SIZEOFT:
- /*@i43 drl possible problem : warning make sure the case can be ignored.. */
+ /*drl 4-11-03 I think this is the same as the next case...*/
break;
ret = constraintList_addListFree (ret,
exprNode_traversTrueEnsuresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
exprNode_traversFalseEnsuresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
exprNode_traversRequiresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
exprNode_traversEnsuresConstraints
(exprData_getFcn (data)));
- /*@i11*/ /* exprNodeList_unparse (exprData_getArgs (data)); */
break;
case XPR_RETURN:
ret = constraintList_addListFree (ret,
I'm a bit nervous about modifying the exprNode
but this is the easy way to do this
If I have time I'd like to cause the exprNode to get created correctly in the first place */
-/*@i223*/
void exprNode_findValue(exprNode e)
{
exprData data;