-void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoint)
-{
- temp->requiresConstraints = constraintList_makeNew();
- temp->ensuresConstraints = constraintList_makeNew();
- temp->trueEnsuresConstraints = constraintList_makeNew();
- temp->falseEnsuresConstraints = constraintList_makeNew();
-
- exprNodeList_elements (arglist, el)
- {
- exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
- el->requiresConstraints = exprNode_traversRequiresConstraints(el);
- el->ensuresConstraints = exprNode_traversEnsuresConstraints(el);
-
- temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
- el->requiresConstraints);
-
- temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
- el->ensuresConstraints);
- }
- end_exprNodeList_elements;
-
-}
-
-constraintList checkCall (exprNode fcn, exprNodeList arglist)
-{
- constraintList preconditions;
- uentry temp;
- DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
-
- temp = exprNode_getUentry (fcn);
-
- preconditions = uentry_getFcnPreconditions (temp);
-
- if (preconditions)
- {
- preconditions = constraintList_copy(preconditions);
- preconditions= constraintList_togglePost (preconditions);
- preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
- }
- else
- {
- preconditions = constraintList_makeNew();
- }
-
- return preconditions;
-}
-
-constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
-{
- constraintList postconditions;
- uentry temp;
- DPRINTF ( (message ("Got call that %s ( %s) ", exprNode_unparse(fcn), exprNodeList_unparse (arglist ) ) ) );
-
- temp = exprNode_getUentry (fcn);
-
- postconditions = uentry_getFcnPostconditions (temp);
-
- if (postconditions)
- {
- postconditions = constraintList_copy(postconditions);
- postconditions = constraintList_doFixResult (postconditions, fcnCall);
- postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
- }
- else
- {
- postconditions = constraintList_makeNew();
- }
-
- return postconditions;
-}
-
-void mergeResolve (exprNode parent, exprNode child1, exprNode child2)