From: drl7x Date: Tue, 3 Oct 2000 18:06:14 +0000 (+0000) Subject: It mostly works but it has a convolted API that needs fixxing. X-Git-Tag: oct3uglyapi X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/commitdiff_plain/6364363cda6f8558b839d1b07ec85effee287580 It mostly works but it has a convolted API that needs fixxing. --- diff --git a/src/constraint.c b/src/constraint.c index 4b7b5c2..7693e2f 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -350,7 +350,7 @@ cstring constraint_printDetailed (constraint c) } else { - st = message ("Function Post condition:\nBased on the constraint %s this function appears to have the post condition %s", constraint_print (c), constraint_print(c->orig) ); + st = message ("Function Post condition:\nThis function appears to have the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) ); } return st; } diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index ed0bbd7..70e1ae8 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -211,12 +211,14 @@ bool exprNode_stmtList (exprNode e) stmt1 = exprData_getPairA (e->edata); stmt2 = exprData_getPairB (e->edata); - + + DPRINTF(("XW stmtlist ") ); + DPRINTF ((message("XW%s | %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) ); + exprNode_stmt (stmt1); DPRINTF(("\nstmt after stmtList call " )); exprNode_stmt (stmt2); - mergeResolve (e, stmt1, stmt2 ); DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n", constraintList_print(e->requiresConstraints), diff --git a/src/constraintResolve.c b/src/constraintResolve.c index 24d43cf..6367d5c 100644 --- a/src/constraintResolve.c +++ b/src/constraintResolve.c @@ -187,6 +187,22 @@ constraint solveforterm (constraint c) return c; } +constraint solveforOther (constraint c) +{ + constraintExpr p; + p = c->expr; + while (p->expr != NULL) + { + TPRINTF( (message("Moving %s", constraintExpr_print (c->expr) ) ) ); + c->lexpr = termMove(c->lexpr, p); + p->op = p->expr->op; + #warning memleak + + p->expr = p->expr->expr; + } + return c; +} + constraint constraint_simplify (constraint c) { c = solveforterm (c); @@ -230,11 +246,76 @@ constraintExpr constraintExpr_substituteTerm (constraintExpr expr, constraintTer return expr; } -constraint constraint_substituteTerm (constraint c, constraintTerm oldterm, constraintExpr replacement) + +/* returns true if fileloc for term2 is closer to file for term1 than is term3*/ + +bool fileloc_closer (constraintTerm term1, constraintTerm term2, constraintTerm term3) { - c->lexpr = constraintExpr_substituteTerm (c->lexpr, oldterm, replacement); - c->expr = constraintExpr_substituteTerm (c->expr, oldterm, replacement); - return c; + if ( fileloc_lessthan (term1->loc, term2->loc) ) + { + if (fileloc_lessthan (term2->loc, term3->loc) ) + { + llassert (fileloc_lessthan (term1->loc, term3->loc) ); + return TRUE; + } + else + { + return FALSE; + } + } + + if ( ! (fileloc_lessthan (term1->loc, term2->loc) ) ) + { + if (!fileloc_lessthan (term2->loc, term3->loc) ) + { + llassert (fileloc_lessthan (term3->loc, term1->loc) ); + return TRUE; + } + else + { + return FALSE; + + } + } + + llassert(FALSE); + return FALSE; +} + +constraint constraint_substituteTerm (constraint c, constraint subs) +{ + constraintTerm oldterm; + constraintExpr replacement; + + llassert(subs->lexpr->expr == NULL); + + + oldterm = subs->lexpr->term; + replacement = subs->expr; + + // Chessy hack assumes that subs always has the form g:1 = g:2 + expr + + /*@i2*/ + + /*find out which value to substitute*/ + TPRINTF((message ("doing substitute for %s and %s", constraint_print (c), constraint_print(subs) ) ) ); + if ( constraintExpr_containsTerm (subs->expr, subs->lexpr->term) ) + { + TPRINTF(("doing new stuff")); + if (fileloc_closer (c->lexpr->term, subs->expr->term, subs->lexpr->term) ) + { + // use the other term + constraint new; + new = constraint_copy (subs); + new = solveforOther(new); + oldterm = new->expr->term; + replacement = new->lexpr; + } + } + + c->lexpr = constraintExpr_substituteTerm (c->lexpr, oldterm, replacement); + c->expr = constraintExpr_substituteTerm (c->expr, oldterm, replacement); + return c; } constraint substitute (constraint c, constraintList p) @@ -243,19 +324,18 @@ constraint substitute (constraint c, constraintList p) { if ( el->ar == EQ) if (constraint_hasTerm (c, el->lexpr->term) ) - // constraintTerm_same(c->lexpr->term, el->lexpr->term) ) { - { + llassert(el->lexpr->expr == NULL); DPRINTF((message ("doing substitute for %s", constraint_print (c) ) ) ); - c = constraint_substituteTerm (c, el->lexpr->term, el->expr); + + c = constraint_substituteTerm (c, el); DPRINTF((message ("substituted constraint is now %s", constraint_print (c) ) ) ); // c->lexpr = constraintExpr_copy (el->expr); c = constraint_simplify(c); c = constraint_simplify(c); c = constraint_simplify(c); return c; - } - } + } } end_constraintList_elements; @@ -282,6 +362,25 @@ constraintList reflectChanges (constraintList pre2, constraintList post1) return ret; } +bool constraintExpr_containsTerm (constraintExpr p, constraintTerm term) +{ + TPRINTF(("constraintExpr_containsTerm")); + + while (p != NULL) + { + if (constraintTerm_similar (p->term, term) ) + return TRUE; + + p = p->expr->expr; + } + DPRINTF(( + message ("constraintExpr_hasTerm returned fallse for %s %S", + constraint_print(c), constraintTerm_print(term) + ) + )); + return FALSE; +} + /*check if rvalue side has term*/ bool constraintExpr_hasTerm (constraint c, constraintTerm term) @@ -330,16 +429,16 @@ constraintExpr solveEq (constraint c, constraintTerm t) constraint updateConstraint (constraint c, constraintList p) { - DPRINTF(("start updateConstraints")); + TPRINTF(("start updateConstraints")); constraintList_elements (p, el) { if (constraintTerm_same(c->lexpr->term, el->lexpr->term) ) { - DPRINTF(("")); + TPRINTF(("")); if ( el->ar == EQ) { - TPRINTF(("")); + TPRINTF(("j")); if (constraintExpr_hasTerm (el, c->lexpr->term) ) { @@ -373,7 +472,7 @@ constraintList reflectChangesEnsures (constraintList pre2, constraintList post1) { if (!resolve (el, post1) ) { - temp = updateConstraint (el, post1); + temp = substitute (el, post1); if (temp != NULL) ret = constraintList_add (ret, temp); } @@ -387,21 +486,30 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2) constraintList temp; DPRINTF( (message ("magically merging constraint into parent:%s for children: %s and %s", exprNode_unparse (parent), exprNode_unparse (child1), exprNode_unparse(child2) ) ) ); - llassert (!exprNode_isError (child1) || !exprNode_isError(child2) ); - if (exprNode_isError (child1) ) - { - parent->requiresConstraints = constraintList_copy (child2->requiresConstraints); - parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints); - DPRINTF((message ("Copied child constraints: pre: %s and post: %s", - constraintList_print( child2->requiresConstraints), - constraintList_print (child2->ensuresConstraints) - ) - )); - return; - } - - llassert(!exprNode_isError(child2) ); - + if (exprNode_isError (child1) || exprNode_isError(child2) ) + { + if (exprNode_isError (child1) && !exprNode_isError(child2) ) + { + parent->requiresConstraints = constraintList_copy (child2->requiresConstraints); + parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints); + DPRINTF((message ("Copied child constraints: pre: %s and post: %s", + constraintList_print( child2->requiresConstraints), + constraintList_print (child2->ensuresConstraints) + ) + )); + return; + } + else + { + llassert(exprNode_isError(child2) ); + parent->requiresConstraints = constraintList_new(); + parent->ensuresConstraints = constraintList_new(); + return; + } + } + + llassert(!exprNode_isError (child1) && ! exprNode_isError(child2) ); + DPRINTF( (message ("Child constraints are %s %s and %s %s", constraintList_print (child1->requiresConstraints), constraintList_print (child1->ensuresConstraints), diff --git a/src/constraintTerm.c b/src/constraintTerm.c index 471dae7..e7f0551 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -320,7 +320,7 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) return FALSE; } - DPRINTF ( (message + TPRINTF ( (message ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2) ) ) @@ -333,7 +333,7 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) } else { - DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); + TPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) )); return FALSE; }