/*
-** LCLint - annotation-assisted static program checker
+** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2000 University of Virginia,
** Massachusetts Institute of Technology
**
** 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
**
** 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));
s->nspace = constraintListBASESIZE;
s->elements = (constraint *)
dmalloc (sizeof (*s->elements) * constraintListBASESIZE);
-
+
return (s);
}
int i;
constraint *newelements;
+ llassert (constraintList_isDefined (s));
+
s->nspace += constraintListBASESIZE;
newelements = (constraint *) dmalloc (sizeof (*newelements)
* (s->nelements + s->nspace));
s->elements = newelements;
}
-/* void constraintList_exprNodemerge(void) */
-/* { */
-/* } */
+
constraintList
-constraintList_add (constraintList s, constraint el)
+constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
{
- if (resolve (el, s) )
- return s;
+ llassert (constraintList_isDefined (s));
+
+ /*drl7x */
+
+ if (constraintList_resolve (el, s) )
+ {
+ constraint_free (el);
+ return s;
+ }
if (s->nspace <= 0)
constraintList_grow (s);
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)
+{
+ 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(s);
- llassert(new);
+ llassert(constraintList_isDefined(s) );
+ llassert(constraintList_isDefined(newList) );
- if (new == constraintList_undefined)
+ if (constraintList_isUndefined(newList) )
return s;
- constraintList_elements(new, elem)
+ 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_unparse(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_unparse(elem))));
+ constraint_free(elem);
+ }
+ else
+ {
+ ret = constraintList_add (ret, elem);
+ }
+ fileloc_free(loc);
+ }
+ end_constraintList_elements_private_only;
+
+ constraintList_freeShallow(s);
+
+ return ret;
+}
+
+# if 0
+static /*@only@*/ cstring
+constraintList_unparseLocation (/*@temp@*/ constraintList s) /*@*/
{
int i;
cstring st = cstring_undefined;
bool first = TRUE;
+
+ if (!constraintList_isDefined (s))
+ {
+ return cstring_makeLiteral ("<undefined>");
+ }
if (s->nelements == 0)
- st = cstring_makeLiteral("<List Empty>");
-
+ {
+ st = cstring_makeLiteral("<List Empty>");
+ 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_unparseLocation(current);
type = message ("%q %q\n", type, temp1 );
}
{
st = message ("%q, %q", st, type);
}
+ }
+
+ return st;
+}
+# endif
+
+/*@only@*/ cstring
+constraintList_unparse (/*@temp@*/ constraintList s) /*@*/
+{
+ int i;
+ cstring st = cstring_undefined;
+ bool first = TRUE;
+
+ if (!constraintList_isDefined (s))
+ {
+ return cstring_makeLiteral ("<undefined>");
+ }
+
+ if (s->nelements == 0)
+ {
+ st = cstring_makeLiteral("<List Empty>");
+ 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_unparseOr(current);
+ }
+ else
+ {
+ temp1 = constraint_unparse (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_printError (constraintList s, fileloc loc)
+void constraintList_unparseErrorPostConditions (constraintList s, fileloc loc)
+{
+
+ constraintList_elements (s, elem)
+ {
+ if (constraint_isDefined(elem))
+ {
+ constraint_printErrorPostCondition (elem, loc);
+ }
+ }
+ end_constraintList_elements;
+ return;
+}
+
+void constraintList_unparseError (constraintList s, fileloc loc)
{
constraintList_elements (s, elem)
{
- if (elem != NULL)
+ if (constraint_isDefined(elem) )
{
- constraint_printError (elem, loc);
+ if (constraint_isPost(elem) )
+ constraint_printErrorPostCondition (elem, loc);
+ else
+ constraint_printError (elem, loc);
}
}
end_constraintList_elements;
return;
}
+
cstring
-constraintList_printDetailed (constraintList s)
+constraintList_unparseDetailed (constraintList s)
{
int i;
cstring st = cstring_undefined;
bool first = TRUE;
+ if (!constraintList_isDefined (s))
+ {
+ return cstring_makeLiteral ("<undefined>");
+ }
+
if (s->nelements == 0)
- st = cstring_makeLiteral("<List Empty>");
-
+ {
+ st = cstring_makeLiteral("<List Empty>");
+ 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);
+ cstring temp1 = constraint_unparseDetailed (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;
} */
constraintList
-constraintList_logicalOr (constraintList l1, constraintList l2)
+constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
{
constraint temp;
constraintList ret;
- DPRINTF ( (message ("Logical of on %s and %s",
- constraintList_print(l1),
- constraintList_print(l2)) ) );
+ DPRINTF ((message ("Logical or on %s and %s",
+ constraintList_unparse(l1),
+ constraintList_unparse(l2)) ) );
- ret = constraintList_new();
+ ret = constraintList_makeNew();
constraintList_elements (l1, el)
{
- temp = substitute (el, l2);
+ temp = constraint_substitute (el, l2);
- if (resolve (el, l2) || resolve(temp,l2) )
+ if (constraintList_resolve (el, l2) || constraintList_resolve(temp,l2) )
{ /*avoid redundant constraints*/
- if (!resolve (el, ret) )
- ret = constraintList_add (ret, el);
+ 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 = substitute (el, l1);
+ temp = constraint_substitute (el, l1);
- if (resolve (el, l1) || resolve(temp,l1) )
+ if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) )
{
/*avoid redundant constraints*/
- if (!resolve (el, ret) )
- ret = constraintList_add (ret, el);
+ if (!constraintList_resolve (el, ret) )
+ {
+ constraint temp2;
+ temp2 = constraint_copy(el);
+ ret = constraintList_add (ret, temp2);
+ }
}
+ constraint_free(temp);
}
end_constraintList_elements;
}
void
-constraintList_free (constraintList s)
+constraintList_free (/*@only@*/ constraintList s)
{
- int i;
- for (i = 0; i < s->nelements; i++)
+ if (constraintList_isDefined (s))
{
- // constraint_free (s->elements[i]);
+ int i;
+
+ for (i = 0; i < s->nelements; i++)
+ {
+ constraint_free (s->elements[i]);
+ }
+
+ sfree (s->elements);
+ s->elements = NULL;
+ s->nelements = -1;
+ s->nspace = -1;
+ sfree (s);
+ s = NULL;
}
-
- sfree (s->elements);
- sfree (s);
}
constraintList
-constraintList_copy (constraintList s) /*@*/
+constraintList_copy (/*@observer@*/ /*@temp@*/ constraintList s)
{
- constraintList ret = constraintList_new ();
+ constraintList ret = constraintList_makeNew ();
constraintList_elements (s, el)
{
constraintList constraintList_preserveOrig (constraintList c)
{
- constraintList_elements (c, el)
+ DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_unparse (c) ) ));
+
+ constraintList_elements_private (c, el)
{
el = constraint_preserveOrig (el);
}
- end_constraintList_elements;
+ end_constraintList_elements_private;
+ return c;
+}
+
+constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/ exprNode fcn)
+{
+ DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_unparse (c) ) ));
+
+ constraintList_elements_private (c, el)
+ {
+ el = constraint_setFcnPre(el);
+ el = constraint_origAddGeneratingExpr (el, fcn);
+ }
+ end_constraintList_elements_private;
return c;
}
-constraintList constraintList_addGeneratingExpr (constraintList c, exprNode e)
+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 (c, el)
+ constraintList_elements_private (c, el)
{
- DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(el), exprNode_unparse(e) ) ));
+ DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_unparse(el), exprNode_unparse(e) ) ));
el = constraint_addGeneratingExpr (el, e);
}
- end_constraintList_elements;
+ end_constraintList_elements_private;
return c;
}
-constraintList constraintList_doFixResult (constraintList postconditions, exprNode fcnCall)
+/*@only@*/ constraintList constraintList_doFixResult (/*@only@*/constraintList postconditions, exprNode fcnCall)
{
constraintList ret;
- ret = constraintList_new();
- constraintList_elements (postconditions, el)
+ 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;
}
+*/
-constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, exprNodeList arglist)
+/*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist)
{
constraintList ret;
- ret = constraintList_new();
+ ret = constraintList_makeNew();
constraintList_elements (preconditions, el)
{
}
end_constraintList_elements;
+ constraintList_free (preconditions);
+
return ret;
}
-constraintList constraintList_doSRefFixBaseParam (constraintList preconditions,
+constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/
exprNodeList arglist)
{
constraintList ret;
- ret = constraintList_new();
+ constraint temp;
+ ret = constraintList_makeNew();
constraintList_elements (preconditions, el)
{
- ret = constraintList_add(ret, constraint_doSRefFixBaseParam (el, arglist) );
+ temp = constraint_copy(el);
+ ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
}
end_constraintList_elements;
constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
{
- constraintList_elements (c, el)
+ constraintList_elements_private (c, el)
{
- el->post = !el->post;
+ el = constraint_togglePost(el);
+ if (constraint_hasOrig(el) )
+ {
+ el = constraint_togglePostOrig (el);
+ }
}
- end_constraintList_elements;
+ 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 (! mstring_isDefined(c) )
+ {
+ llfatalbug(message("Library file is corrupted") );
+ }
+
+
+ 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)
+{
+ if (constraintList_isUndefined(ret) )
+ {
+ llassert(FALSE);
+ return 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;
+}
+
andersk / splint.git / blobdiff