/*
-** 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 "llbasic.h"
-
+# include "splintMacros.nf"
+# include "basic.h"
/*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/
# define constraintList_elements_private_only(x, m_el) \
s->nspace = constraintListBASESIZE;
s->elements = (constraint *)
dmalloc (sizeof (*s->elements) * constraintListBASESIZE);
-
+
return (s);
}
int i;
constraint *newelements;
- llassert (constraintList_isDefined (s));
+ llassertfatal (constraintList_isDefined (s));
s->nspace += constraintListBASESIZE;
newelements = (constraint *) dmalloc (sizeof (*newelements)
constraintList
constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
{
- llassert (constraintList_isDefined (s));
+ llassertfatal (constraintList_isDefined (s));
/*drl7x */
- // el = constraint_simplify (el);
- if (constraintList_resolve (el, s) )
+
+ if (constraintList_resolve (el, s))
{
+ DPRINTF (("Resolved constraint: %s", constraint_unparse (el)));
constraint_free (el);
return s;
}
+
+ DPRINTF (("Adding constraint: %s", constraint_unparse (el)));
if (s->nspace <= 0)
constraintList_grow (s);
c = NULL;
}
-/*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ constraintList newList)
+/*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ /*@temp@*/ constraintList newList)
{
- llassert(constraintList_isDefined(s) );
- llassert(constraintList_isDefined(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) );
+ s = constraintList_add (s, constraint_copy(elem));
}
end_constraintList_elements;
constraintList constraintList_addListFree (/*@returned@*/ constraintList s, /*@only@*/ constraintList newList)
{
- llassert(constraintList_isDefined(s) );
- llassert(constraintList_isDefined(newList) );
-
- if (constraintList_isUndefined(newList) )
+ if (constraintList_isUndefined (newList))
return s;
+
+ llassert (constraintList_isDefined (s));
+ llassert (constraintList_isDefined (newList));
constraintList_elements_private_only(newList, elem)
{
- s = constraintList_add (s, elem);
- }
- end_constraintList_elements_private_only
-
- constraintList_freeShallow(newList);
- return s;
+ s = constraintList_add (s, elem);
+ } end_constraintList_elements_private_only;
+
+ constraintList_freeShallow (newList);
+ return s;
}
-
constraintList constraintList_removeSurpressed (/*@only@*/ constraintList s)
{
constraintList ret;
fileloc loc;
- llassert(constraintList_isDefined(s) );
+ llassert (constraintList_isDefined (s));
ret = constraintList_makeNew();
- constraintList_elements_private_only(s, elem)
+ constraintList_elements_private_only (s, elem)
{
loc = constraint_getFileloc(elem);
- if(fileloc_isUndefined(loc) )
+ if (fileloc_isUndefined(loc))
{
ret = constraintList_add (ret, elem);
}
-
- else if (context_suppressFlagMsg(FLG_ARRAYBOUNDS, loc) )
+ else if (context_suppressFlagMsg(FLG_BOUNDSWRITE, loc) )
{
- DPRINTF(( message("constraintList_removeSurpressed getting rid of surpressed constraint %q", constraint_print(elem) ) ));
+ DPRINTF ((message ("constraintList_removeSurpressed getting rid of surpressed constraint %q",
+ constraint_unparse(elem))));
constraint_free(elem);
}
-
- else if ( (! constraint_hasMaxSet(elem) ) && context_suppressFlagMsg(FLG_ARRAYBOUNDSREAD, loc) )
+ else if (!constraint_hasMaxSet(elem) && context_suppressFlagMsg(FLG_BOUNDSREAD, loc))
{
- DPRINTF(( message("constraintList_removeSurpressed getting rid of surpressed constraint %q", constraint_print(elem) ) ));
+ 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;
+ } 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) /*@*/
+constraintList_unparseLocation (/*@temp@*/ constraintList s) /*@*/
{
int i;
cstring st = cstring_undefined;
if (constraint_isDefined(current) )
{
cstring temp1;
- temp1 = constraint_printLocation(current);
+ temp1 = constraint_unparseLocation(current);
type = message ("%q %q\n", type, temp1 );
}
{
st = message ("%q, %q", st, type);
}
- } //end for
+ }
return st;
}
-
+# endif
/*@only@*/ cstring
-constraintList_print (/*@temp@*/ constraintList s) /*@*/
+constraintList_unparse (/*@temp@*/ constraintList s) /*@*/
{
int i;
cstring st = cstring_undefined;
if (constraint_isDefined(current) )
{
cstring temp1;
- if ( context_getFlag (FLG_ORCONSTRAINT) )
- temp1 = constraint_printOr(current);
- else
- temp1 = constraint_print(current);
+
+ if (context_getFlag (FLG_ORCONSTRAINT))
+ {
+ temp1 = constraint_unparseOr (current);
+ }
+ else
+ {
+ temp1 = constraint_unparse (current);
+ }
type = message ("%q %q\n", type, temp1 );
}
{
st = message ("%q, %q", st, type);
}
- } //end for
+ }
return st;
}
cstring
-constraintList_printDetailed (constraintList s)
+constraintList_unparseDetailed (constraintList s)
{
int i;
cstring st = cstring_undefined;
if (constraint_isDefined(current ) )
{
- cstring temp1 = constraint_printDetailed (current);
+ cstring temp1 = constraint_unparseDetailed (current);
type = message ("%s %s\n", type, temp1 );
cstring_free(temp1);
}
{
constraint temp;
constraintList ret;
- DPRINTF ( (message ("Logical or 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_makeNew();
constraintList_elements (l1, el)
void
constraintList_free (/*@only@*/ constraintList s)
{
- int i;
-
- llassert(constraintList_isDefined(s) );
-
-
- 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);
- s->elements = NULL;
- s->nelements = -1;
- s->nspace = -1;
- sfree (s);
- s = NULL;
}
constraintList
constraintList constraintList_preserveOrig (constraintList c)
{
- DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
+ DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_unparse (c) ) ));
constraintList_elements_private (c, el)
{
constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/ exprNode fcn)
{
- DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_print (c) ) ));
+ DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_unparse (c) ) ));
constraintList_elements_private (c, el)
{
- // el = constraint_preserveOrig (el);
el = constraint_setFcnPre(el);
el = constraint_origAddGeneratingExpr (el, fcn);
}
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_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)
{
/*@only@*/ constraintList constraintList_undump (FILE *f)
{
constraintList ret;
- char *s = mstring_create (MAX_DUMP_LINE_LENGTH);
+ char *s;
char *os;
ret = constraintList_makeNew();
- os = s;
+ os = mstring_create (MAX_DUMP_LINE_LENGTH);
s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
while (s != NULL && *s != ';')
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"));
end_constraintList_elements; ;
}
-
constraintList constraintList_sort (/*@returned@*/ constraintList ret)
{
-
- DPRINTF(( message("Before constraint_sort %q", constraintList_printLocation(ret) ) ));
-
- qsort (ret->elements, (size_t) ret->nelements,
- (sizeof (*ret->elements) ), constraint_compare);
-
- DPRINTF((message("After constraint_sort %q", constraintList_printLocation(ret) ) ));
+ if (constraintList_isUndefined(ret) )
+ {
+ llassert(FALSE);
+ return ret;
+ }
- DPRINTF((message("onstraint_sort returning") ));
+ 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