X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/bf92e32cf4958be7a9035826b51d0ea8bba57ded..a9aef8c80109c7fc8de874420738037596a2656c:/src/constraintList.c diff --git a/src/constraintList.c b/src/constraintList.c index 21bd987..99dc7e7 100644 --- a/src/constraintList.c +++ b/src/constraintList.c @@ -1,5 +1,5 @@ /* -** LCLint - annotation-assisted static program checker +** Splint - annotation-assisted static program checker ** Copyright (C) 1994-2000 University of Virginia, ** Massachusetts Institute of Technology ** @@ -17,10 +17,11 @@ ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, ** MA 02111-1307, USA. ** -** For information on lclint: lclint-request@cs.virginia.edu -** To report a bug: lclint-bug@cs.virginia.edu -** For more information: http://lclint.cs.virginia.edu +** For information on splint: info@splint.org +** To report a bug: splint-bug@splint.org +** For more information: http://www.splint.org */ + /* ** constraintList.c ** @@ -29,10 +30,29 @@ ** where T has T_equal (or change this) and T_unparse */ -# include "lclintMacros.nf" +# include "splintMacros.nf" # include "llbasic.h" -constraintList constraintList_new () + +/*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/ +# define constraintList_elements_private_only(x, m_el) \ + { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \ + for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ + { constraint m_el = *(m_elements++); + +# define end_constraintList_elements_private_only }}} + + +/*@iter constraintList_elements_private (sef constraintList x, yield constraint el); @*/ +# define constraintList_elements_private(x, m_el) \ + { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \ + for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \ + { constraint m_el = *(m_elements++); + +# define end_constraintList_elements_private }}} + + +/*@only@*/ constraintList constraintList_makeNew () { constraintList s = (constraintList) dmalloc (sizeof (*s)); @@ -50,6 +70,8 @@ constraintList_grow (constraintList s) int i; constraint *newelements; + llassert (constraintList_isDefined (s)); + s->nspace += constraintListBASESIZE; newelements = (constraint *) dmalloc (sizeof (*newelements) * (s->nelements + s->nspace)); @@ -63,12 +85,20 @@ constraintList_grow (constraintList s) s->elements = newelements; } -void constraintList_exprNodemerge() -{ -} + constraintList -constraintList_add (constraintList s, constraint el) +constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el) { + llassert (constraintList_isDefined (s)); + + /*drl7x */ + + if (constraintList_resolve (el, s) ) + { + constraint_free (el); + return s; + } + if (s->nspace <= 0) constraintList_grow (s); @@ -78,32 +108,136 @@ constraintList_add (constraintList s, constraint el) return s; } -constraintList constraintList_addList (constraintList s, constraintList new) +/* frees everything but actual constraints */ +/* This function should only be used if you have + other references to unshared constraints +*/ +static void constraintList_freeShallow (/*@only@*/ constraintList c) +{ + if (constraintList_isDefined(c) ) + { + free (c->elements); + c->elements = NULL; + c->nelements = -1; + c->nspace = -1; + } + free (c); + c = NULL; +} + +/*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ /*@temp@*/ constraintList newList) { - constraintList_elements(new, elem) + llassert(constraintList_isDefined(s) ); + llassert(constraintList_isDefined(newList) ); + + if (newList == constraintList_undefined) + return s; + + constraintList_elements (newList, elem) + { + s = constraintList_add (s, constraint_copy(elem) ); + } + end_constraintList_elements; + + return s; +} + +constraintList constraintList_addListFree (/*@returned@*/ constraintList s, /*@only@*/ constraintList newList) +{ + llassert(constraintList_isDefined(s) ); + llassert(constraintList_isDefined(newList) ); + + if (constraintList_isUndefined(newList) ) + return s; + + constraintList_elements_private_only(newList, elem) + { s = constraintList_add (s, elem); - end_constraintList_elements + } + end_constraintList_elements_private_only + + constraintList_freeShallow(newList); return s; } -cstring -constraintList_print (constraintList s) + +constraintList constraintList_removeSurpressed (/*@only@*/ constraintList s) +{ + constraintList ret; + fileloc loc; + llassert(constraintList_isDefined(s) ); + + ret = constraintList_makeNew(); + + constraintList_elements_private_only(s, elem) + { + loc = constraint_getFileloc(elem); + + if (fileloc_isUndefined(loc)) + { + ret = constraintList_add (ret, elem); + } + + else if (context_suppressFlagMsg(FLG_BOUNDSWRITE, loc) ) + { + DPRINTF ((message ("constraintList_removeSurpressed getting rid of surpressed constraint %q", + constraint_print(elem)))); + constraint_free(elem); + } + + else if (!constraint_hasMaxSet(elem) && context_suppressFlagMsg(FLG_BOUNDSREAD, loc)) + { + DPRINTF ((message("constraintList_removeSurpressed getting rid of surpressed constraint %q", + constraint_print(elem)))); + constraint_free(elem); + } + else + { + ret = constraintList_add (ret, elem); + } + fileloc_free(loc); + } + end_constraintList_elements_private_only; + + constraintList_freeShallow(s); + + return ret; +} + + +extern /*@only@*/ cstring constraintList_unparse ( /*@observer@*/ constraintList s) /*@*/ +{ + return (constraintList_print(s)); +} + +# if 0 +static /*@only@*/ cstring +constraintList_printLocation (/*@temp@*/ constraintList s) /*@*/ { int i; cstring st = cstring_undefined; bool first = TRUE; + + if (!constraintList_isDefined (s)) + { + return cstring_makeLiteral (""); + } if (s->nelements == 0) - st = cstring_makeLiteral(""); - + { + st = cstring_makeLiteral(""); + return st; + } + for (i = 0; i < s->nelements; i++) { cstring type = cstring_undefined; constraint current = s->elements[i]; - if (current != NULL) + if (constraint_isDefined(current) ) { - cstring temp1 = constraint_print(current); + cstring temp1; + temp1 = constraint_printLocation(current); type = message ("%q %q\n", type, temp1 ); } @@ -116,10 +250,90 @@ constraintList_print (constraintList s) { st = message ("%q, %q", st, type); } + } + + return st; +} +# endif + +/*@only@*/ cstring +constraintList_print (/*@temp@*/ constraintList s) /*@*/ +{ + int i; + cstring st = cstring_undefined; + bool first = TRUE; + + if (!constraintList_isDefined (s)) + { + return cstring_makeLiteral (""); } + + if (s->nelements == 0) + { + st = cstring_makeLiteral(""); + return st; + } + + for (i = 0; i < s->nelements; i++) + { + cstring type = cstring_undefined; + constraint current = s->elements[i]; + + if (constraint_isDefined(current) ) + { + cstring temp1; + if ( context_getFlag (FLG_ORCONSTRAINT) ) + temp1 = constraint_printOr(current); + else + temp1 = constraint_print(current); + type = message ("%q %q\n", type, temp1 ); + } + + if (first) + { + st = type; + first = FALSE; + } + else + { + st = message ("%q, %q", st, type); + } + } + return st; } +void constraintList_printErrorPostConditions (constraintList s, fileloc loc) +{ + + constraintList_elements (s, elem) + { + if (constraint_isDefined(elem)) + { + constraint_printErrorPostCondition (elem, loc); + } + } + end_constraintList_elements; + return; +} + +void constraintList_printError (constraintList s, fileloc loc) +{ + + constraintList_elements (s, elem) + { + if (constraint_isDefined(elem) ) + { + if (constraint_isPost(elem) ) + constraint_printErrorPostCondition (elem, loc); + else + constraint_printError (elem, loc); + } + } + end_constraintList_elements; + return; +} + cstring constraintList_printDetailed (constraintList s) @@ -128,50 +342,120 @@ constraintList_printDetailed (constraintList s) cstring st = cstring_undefined; bool first = TRUE; + if (!constraintList_isDefined (s)) + { + return cstring_makeLiteral (""); + } + if (s->nelements == 0) - st = cstring_makeLiteral(""); - + { + st = cstring_makeLiteral(""); + return st; + } + for (i = 0; i < s->nelements; i++) { cstring type = cstring_undefined; constraint current = s->elements[i]; - if (current != NULL) + if (constraint_isDefined(current ) ) { cstring temp1 = constraint_printDetailed (current); type = message ("%s %s\n", type, temp1 ); + cstring_free(temp1); } if (first) { st = type; first = FALSE; + type = NULL; } else { - st = message ("%s %s", st, type); + st = message ("%q %q", st, type); } } return st; } +/*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1) +} */ + +constraintList +constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2) +{ + constraint temp; + constraintList ret; + DPRINTF ((message ("Logical or on %s and %s", + constraintList_print(l1), + constraintList_print(l2)) ) ); + + ret = constraintList_makeNew(); + constraintList_elements (l1, el) + { + temp = constraint_substitute (el, l2); + + if (constraintList_resolve (el, l2) || constraintList_resolve(temp,l2) ) + { /*avoid redundant constraints*/ + if (!constraintList_resolve (el, ret) ) + { + constraint temp2; + temp2 = constraint_copy(el); + ret = constraintList_add (ret, temp2); + } + } + constraint_free(temp); + } + end_constraintList_elements; + + constraintList_elements (l2, el) + { + temp = constraint_substitute (el, l1); + + if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) ) + { + /*avoid redundant constraints*/ + if (!constraintList_resolve (el, ret) ) + { + constraint temp2; + temp2 = constraint_copy(el); + ret = constraintList_add (ret, temp2); + } + } + constraint_free(temp); + } + end_constraintList_elements; + + + return ret; +} + void -constraintList_free (constraintList s) +constraintList_free (/*@only@*/ constraintList s) { int i; + + llassert(constraintList_isDefined(s) ); + + for (i = 0; i < s->nelements; i++) { - // constraint_free (s->elements[i]); + constraint_free (s->elements[i]); } sfree (s->elements); + s->elements = NULL; + s->nelements = -1; + s->nspace = -1; sfree (s); + s = NULL; } constraintList -constraintList_copy (constraintList s) +constraintList_copy (/*@observer@*/ /*@temp@*/ constraintList s) { - constraintList ret = constraintList_new (); + constraintList ret = constraintList_makeNew (); constraintList_elements (s, el) { @@ -183,10 +467,182 @@ constraintList_copy (constraintList s) constraintList constraintList_preserveOrig (constraintList c) { - constraintList_elements (c, el); + DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) )); + + constraintList_elements_private (c, el) { el = constraint_preserveOrig (el); } + end_constraintList_elements_private; + return c; +} + +constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/ exprNode fcn) +{ + DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_print (c) ) )); + + constraintList_elements_private (c, el) + { + el = constraint_setFcnPre(el); + el = constraint_origAddGeneratingExpr (el, fcn); + } + end_constraintList_elements_private; + return c; +} + +constraintList constraintList_single (constraint c) +{ + constraintList res; + res = constraintList_makeNew(); + res = constraintList_add (res, c); + return res; +} + +constraintList constraintList_addGeneratingExpr (constraintList c,/*@dependent@*/ exprNode e) +{ + DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) )); + + constraintList_elements_private (c, el) + { + DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(el), exprNode_unparse(e) ) )); + el = constraint_addGeneratingExpr (el, e); + } + end_constraintList_elements_private; + return c; +} + +/*@only@*/ constraintList constraintList_doFixResult (/*@only@*/constraintList postconditions, exprNode fcnCall) +{ + constraintList ret; + ret = constraintList_makeNew(); + constraintList_elements_private (postconditions, el) + { + ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) ); + } + end_constraintList_elements_private; + + constraintList_free(postconditions); + return ret; +} +/* +Commenting out because function is not yet stable + +/ *@only@* / constraintList constraintList_doSRefFixStructConstraint(constraintList invars, sRef s, ctype ct ) +{ + constraintList ret; + ret = constraintList_makeNew(); + + constraintList_elements (invars, el) + { + ret = constraintList_add(ret, constraint_doSRefFixInvarConstraint (el, s, ct) ); + } + end_constraintList_elements; + + / * constraintList_free (invars);* / + + return ret; +} +*/ + +/*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist) +{ + constraintList ret; + ret = constraintList_makeNew(); + + constraintList_elements (preconditions, el) + { + ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) ); + } + end_constraintList_elements; + + constraintList_free (preconditions); + + return ret; +} +constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/ + exprNodeList arglist) +{ + constraintList ret; + constraint temp; + ret = constraintList_makeNew(); + + constraintList_elements (preconditions, el) + { + temp = constraint_copy(el); + ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) ); + } end_constraintList_elements; + + return ret; +} + +constraintList constraintList_togglePost (/*@returned@*/ constraintList c) +{ + constraintList_elements_private (c, el) + { + el = constraint_togglePost(el); + if (constraint_hasOrig(el) ) + { + el = constraint_togglePostOrig (el); + } + } + end_constraintList_elements_private; return c; } + +/*@only@*/ constraintList constraintList_undump (FILE *f) +{ + constraintList ret; + char *s; + char *os; + + ret = constraintList_makeNew(); + + os = mstring_create (MAX_DUMP_LINE_LENGTH); + s = fgets (os, MAX_DUMP_LINE_LENGTH, f); + + while (s != NULL && *s != ';') + { + constraint temp; + char * c; + + c = reader_getWord(&s); + + if (strcmp (c, "C") != 0) + { + llfatalbug(message("Error reading library. File may be corrupted")); + } + + temp = constraint_undump (f); + ret = constraintList_add (ret, temp); + s = fgets (os, MAX_DUMP_LINE_LENGTH, f); + free(c); + } + free(s); + + return ret; +} + + +void constraintList_dump (/*@observer@*/ constraintList c, FILE *f) +{ + constraintList_elements (c, el) + { + fprintf(f, "C\n"); + constraint_dump (el, f); + } + end_constraintList_elements; ; +} + + +constraintList constraintList_sort (/*@returned@*/ constraintList ret) +{ + qsort (ret->elements, (size_t) ret->nelements, + (sizeof (*ret->elements)), + (int (*)(const void *, const void *)) constraint_compare); + + DPRINTF((message("onstraint_sort returning") )); + return ret; +} + +