+ DPRINTF((message ("constraintList_mergeRequires: merging %s and %s ", constraintList_print (list1), constraintList_print(list2) ) ) );
+
+ /* get constraints in list1 not satified by list2 */
+ temp = reflectChanges (list1, list2);
+ DPRINTF((message ("constraintList_mergeRequires: temp = %s", constraintList_print(temp) ) ) );
+
+/*get constraints in list2 not satified by temp*/
+ ret = reflectChanges (list2, temp);
+
+ DPRINTF((message ("constraintList_mergeRequires: ret = %s", constraintList_print(ret) ) ) );
+
+ ret = constraintList_addListFree (ret, temp);
+
+ DPRINTF((message ("constraintList_mergeRequires: returning %s", constraintList_print(ret) ) ) );
+
+ return ret;
+}
+
+void checkArgumentList (/*@out@*/ 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)
+ {
+ constraintList temp2;
+ exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
+ temp2 = el->requiresConstraints;
+ el->requiresConstraints = exprNode_traversRequiresConstraints(el);
+ constraintList_free(temp2);
+
+ temp2 = el->ensuresConstraints;
+ el->ensuresConstraints = exprNode_traversEnsuresConstraints(el);
+ constraintList_free(temp2);
+
+ 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 != constraintList_undefined)
+ {
+ preconditions = constraintList_togglePost (preconditions);
+ preconditions = constraintList_preserveCallInfo(preconditions, fcn);
+ preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
+ }
+ else
+ {
+ if (preconditions == NULL)
+ preconditions = constraintList_makeNew();
+ }
+ DPRINTF (( message("Done checkCall\n") ));
+ DPRINTF (( message("Returning list %q ", constraintList_printDetailed(preconditions) ) ));
+ 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 != constraintList_undefined)
+ {
+ postconditions = constraintList_doFixResult (postconditions, fcnCall);
+ postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
+ }
+ else
+ {
+ postconditions = constraintList_makeNew();
+ }
+
+ return postconditions;
+}
+
+void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
+{
+ constraintList temp, temp2;
+
+ DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )) );