+/*
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2000 University of Virginia,
+** Massachusetts Institute of Technology
+**
+** This program is free software; you can redistribute it and/or modify it
+** under the terms of the GNU General Public License as published by the
+** Free Software Foundation; either version 2 of the License, or (at your
+** option) any later version.
+**
+** This program is distributed in the hope that it will be useful, but
+** WITHOUT ANY WARRANTY; without even the implied warranty of
+** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+** General Public License for more details.
+**
+** The GNU General Public License is available from http://www.gnu.org/ or
+** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+** MA 02111-1307, USA.
+**
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
+*/
+
/*
** constraintList.c
+**
+** based on list_template.c
+**
+** where T has T_equal (or change this) and T_unparse
*/
-# include <ctype.h> /* for isdigit */
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
# include "basic.h"
-# include "cgrammar.h"
-# include "cgrammar_tokens.h"
-# include "exprChecks.h"
-# include "aliasChecks.h"
-# include "exprNodeSList.h"
-# include "exprData.i"
+/*@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 }}}
-/*@notnull@*/ constraintList constraintList_new () {
-constraintList ret;
+/*@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));
-ret = dmalloc ( sizeof (constraintList_) );
-llassert ( ret != NULL);
-ret->numconstraints = 0;
-return ret;
+ s->nelements = 0;
+ s->nspace = constraintListBASESIZE;
+ s->elements = (constraint *)
+ dmalloc (sizeof (*s->elements) * constraintListBASESIZE);
+
+ return (s);
}
-cstring parse_restriction (arithType at)
+static void
+constraintList_grow (constraintList s)
{
- switch (at)
+ int i;
+ constraint *newelements;
+
+ llassert (constraintList_isDefined (s));
+
+ s->nspace += constraintListBASESIZE;
+ newelements = (constraint *) dmalloc (sizeof (*newelements)
+ * (s->nelements + s->nspace));
+
+ for (i = 0; i < s->nelements; i++)
{
- case LT: return "<";
- case LTE: return "<=";
- case GT: return ">";
- case GTE: return ">=";
- case EQ: return "=";
- case NONNEGATIVE: return " >= 0";
- case POSITIVE: return " > 0";
- }
+ newelements[i] = s->elements[i];
+ }
+
+ sfree (s->elements);
+ s->elements = newelements;
}
-cstring constraint_parseKind (constraintType kind)
+
+
+constraintList
+constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
{
- switch (kind)
+ llassert (constraintList_isDefined (s));
+
+ /*drl7x */
+
+ if (constraintList_resolve (el, s))
{
- case BUFFSIZE: return "BufferSize";
- case STRINGLEN: return "StringLength";
- case VALUE: return "value";
+ 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);
+
+ s->nspace--;
+ s->elements[s->nelements] = el;
+ s->nelements++;
+ return s;
}
-void constraint_print (constraint c)
+/* 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 0
- printf ("Constraint: %s of %s %s %s\n", constraint_parseKind (c.kind),
- exprNode_unparse(c.expr1), parse_restriction(c.restriction), exprNode_unparse(c.expr2) );
- #endif
+ if (constraintList_isDefined(c) )
+ {
+ free (c->elements);
+ c->elements = NULL;
+ c->nelements = -1;
+ c->nspace = -1;
+ }
+ free (c);
+ c = NULL;
}
-void constraintList_print (constraintList cl)
+
+/*@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)
+{
+ 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;
+}
+
+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) /*@*/
{
-#if o
int i;
- if (constraintList_isUndefined (cl) )
+ cstring st = cstring_undefined;
+ bool first = TRUE;
+
+ if (!constraintList_isDefined (s))
{
- printf("Constraint List undefined\n");
- return;
+ return cstring_makeLiteral ("<undefined>");
}
- for (i = 0; i < cl->numconstraints; i++)
+
+ if (s->nelements == 0)
{
- constraint_print (cl->constraints[i]);
+ st = cstring_makeLiteral("<List Empty>");
+ return st;
}
-#endif
+
+ for (i = 0; i < s->nelements; i++)
+ {
+ cstring type = cstring_undefined;
+ constraint current = s->elements[i];
+
+ if (constraint_isDefined(current) )
+ {
+ cstring temp1;
+ temp1 = constraint_unparseLocation(current);
+ type = message ("%q %q\n", type, temp1 );
+ }
+
+ if (first)
+ {
+ st = type;
+ first = FALSE;
+ }
+ else
+ {
+ 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;
+}
-constraint constraint_create (exprNode e1, exprNode e2, arithType restriction, constraintType kind)
+void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
{
- constraint ret;
- ret.expr1 = e1;
- ret.expr2 = e2;
- ret.restriction = restriction;
- ret.kind = kind;
- return ret;
+
+ constraintList_elements (s, elem)
+ {
+ if (constraint_isDefined(elem))
+ {
+ constraint_printErrorPostCondition (elem, loc);
+ }
+ }
+ end_constraintList_elements;
+ return;
}
-constraintList constraintList_get (exprNode e1 )
+void constraintList_printError (constraintList s, fileloc loc)
{
- return e1->constraints;
+
+ 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;
}
-constraintList constraintList_exprNodemerge (exprNode e1, exprNode e2)
+
+cstring
+constraintList_unparseDetailed (constraintList s)
{
- constraintList ret;
- if ( (e1 != NULL) && (e2 != NULL) )
+ int i;
+ cstring st = cstring_undefined;
+ bool first = TRUE;
+
+ if (!constraintList_isDefined (s))
{
- ret = constraintList_merge (e1->constraints, e2->constraints);
+ return cstring_makeLiteral ("<undefined>");
}
- else if ( (e1 == NULL) && (e2 == NULL) )
- ret = constraintList_merge ( (constraintList)NULL, (constraintList)NULL );
- else if (e1 == NULL)
- ret = constraintList_merge ( (constraintList)NULL, e2->constraints);
- else
- ret = constraintList_merge (e1->constraints, (constraintList)NULL );
- return ret;
+
+ 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 = constraint_unparseDetailed (current);
+ type = message ("%s %s\n", type, temp1 );
+ cstring_free(temp1);
+ }
+
+ if (first)
+ {
+ st = type;
+ first = FALSE;
+ type = NULL;
+ }
+ else
+ {
+ st = message ("%q %q", st, type);
+ }
+ }
+ return st;
}
+/*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
+} */
-constraintList constraintList_merge (constraintList cl1, constraintList cl2)
+constraintList
+constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
{
+ constraint temp;
constraintList ret;
- int i;
- ret = constraintList_undefined;
- if (constraintList_isDefined (cl1) )
+ DPRINTF ((message ("Logical or on %s and %s",
+ constraintList_unparse(l1),
+ constraintList_unparse(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)
{
- for (i = 0; i < cl1->numconstraints; i++)
+ temp = constraint_substitute (el, l1);
+
+ if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) )
{
- ret = constraintList_add (ret, cl1->constraints[i]);
+ /*avoid redundant constraints*/
+ if (!constraintList_resolve (el, ret) )
+ {
+ constraint temp2;
+ temp2 = constraint_copy(el);
+ ret = constraintList_add (ret, temp2);
+ }
}
+ constraint_free(temp);
}
- if (constraintList_isDefined (cl2) )
+ end_constraintList_elements;
+
+
+ return ret;
+}
+
+void
+constraintList_free (/*@only@*/ constraintList s)
+{
+ if (constraintList_isDefined (s))
{
- for (i = 0; i < cl2->numconstraints; i++)
+ int i;
+
+ for (i = 0; i < s->nelements; i++)
{
- ret = constraintList_add (ret, cl2->constraints[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 (/*@observer@*/ /*@temp@*/ constraintList s)
+{
+ constraintList ret = constraintList_makeNew ();
+
+ constraintList_elements (s, el)
+ {
+ ret = constraintList_add (ret, constraint_copy (el));
+ } end_constraintList_elements;
+
return ret;
+}
+constraintList constraintList_preserveOrig (constraintList c)
+{
+ 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_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_add (constraintList constraints, constraint newconstr)
+constraintList constraintList_single (constraint c)
{
- constraintList ret;
+ 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) ) ));
- if ( constraintList_isUndefined(constraints) )
+ constraintList_elements_private (c, el)
+ {
+ DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_unparse(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_new ();
+ ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) );
}
- else
+ 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 = constraints;
+ ret = constraintList_add(ret, constraint_doSRefFixInvarConstraint (el, s, ct) );
}
- llassert (constraintList_isDefined (ret) );
- llassert (ret->numconstraints < max_constraints);
- ret->constraints[ret->numconstraints] = newconstr;
- ret->numconstraints++;
+ end_constraintList_elements;
+
+ / * constraintList_free (invars);* /
+
return ret;
}
+*/
-cstring exprNode_generateConstraints (exprNode e)
+/*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist)
{
- static int temp = 0;
- cstring ret;
- exprData data;
+ constraintList ret;
+ ret = constraintList_makeNew();
- if (exprNode_isError (e))
+ constraintList_elements (preconditions, el)
{
- static /*@only@*/ cstring error = cstring_undefined;
+ 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;
- if (!cstring_isDefined (error))
+ return ret;
+}
+
+constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
+{
+ constraintList_elements_private (c, el)
+ {
+ el = constraint_togglePost(el);
+ if (constraint_hasOrig(el) )
{
- error = cstring_makeLiteral ("<error>");
+ el = constraint_togglePostOrig (el);
}
-
- return error;
- }
+ }
+ end_constraintList_elements_private;
+ return c;
+}
- data = e->edata;
+/*@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);
- switch (e->kind)
+ while (s != NULL && *s != ';')
{
- case XPR_PARENS:
- ret = message ("(%s)", exprNode_generateConstraints (exprData_getUopNode (e->edata)));
- break;
- case XPR_ASSIGN:
- ret = message ("%s %s %s",
- exprNode_generateConstraints (exprData_getOpA (data)),
- lltok_unparse (exprData_getOpTok (data)),
- exprNode_generateConstraints (exprData_getOpB (data)));
- e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data) );
- break;
- case XPR_CALL:
- ret = message ("%s(%q)",
- exprNode_generateConstraints (exprData_getFcn (data)),
- exprNodeList_unparse (exprData_getArgs (data)));
- break;
- case XPR_INITBLOCK:
- ret = message ("{ %q }", exprNodeList_unparse (exprData_getArgs (data)));
- break;
- case XPR_EMPTY:
- ret = cstring_undefined;
- break;
- case XPR_LABEL:
- ret = message ("%s:", exprData_getId (data));
- break;
- case XPR_CONST:
- case XPR_VAR:
- ret = cstring_copy (exprData_getId (data));
- break;
- case XPR_FETCH:
- ret = message ("%s[%s]", exprNode_generateConstraints (exprData_getPairA (data)),
- exprNode_generateConstraints (exprData_getPairB (data)));
- // printf("Making constraint that size %s > %s\n",exprNode_generateConstraints (exprData_getPairA (data)),
- // exprNode_generateConstraints (exprData_getPairB (data)));
- e->constraints = constraintList_add (e->constraints, constraint_create (exprData_getPairA (data),exprData_getPairB (data) , GT, BUFFSIZE ) );
- e->constraints = constraintList_add (e->constraints, constraint_create (exprData_getPairB (data), exprNode_undefined, NONNEGATIVE, VALUE) );
- /* crude test to see if this is an lvalue */
- if ( sRefSet_isEmpty(e->sets) )
- {
- /* if its not an lvalue we assume it's an rvalue*/
- /* of course if its am lvalue we assume its not an rvalue
- should put in a more accurate test sometime...*/
-
- // printf("Making constraint that length %s > %s\n",exprNode_generateConstraints (exprData_getPairA (data)),
- // exprNode_generateConstraints (exprData_getPairB (data)));
- e->constraints = constraintList_add (e->constraints, constraint_create (exprData_getPairA (data),exprData_getPairB (data) , GT, STRINGLEN ) );
- }
- break;
- case XPR_BODY:
- ret = message ("<body>");
- break;
- case XPR_OP:
- ret = message ("%s %s %s",
- exprNode_generateConstraints (exprData_getOpA (data)),
- lltok_unparse (exprData_getOpTok (data)),
- exprNode_generateConstraints (exprData_getOpB (data)));
- break;
+ constraint temp;
+ char * c;
+
+ c = reader_getWord(&s);
- case XPR_PREOP:
- ret = message ("%s%s",
- lltok_unparse (exprData_getUopTok (data)),
- exprNode_generateConstraints (exprData_getUopNode (data)));
- /*handle * pointer access */
- if (lltok_isMult( exprData_getUopTok (data) ) )
+ 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; ;
+}
+
+//! don't use this!
+void constraintList_castConstraints (constraintList c, ctype tfrom, ctype tto)
+{
+ if (TRUE) /* flag to allow casting */
+ {
+ int fsize = ctype_getSize (tfrom);
+ int tsize = ctype_getSize (tto);
+
+ DPRINTF (("Sizes: [%s] [%s] %d / %d", ctype_unparse (tfrom),
+ ctype_unparse (tto), fsize, tsize));
+
+ if (fsize == tsize)
+ {
+ return; /* Sizes match, no change to constraints */
+ }
+ else
{
- e->constraints = constraintList_add (e->constraints, constraint_create (exprData_getUopNode (data), exprNode_undefined, POSITIVE, BUFFSIZE ) );
- /* crude test to see if this is an lvalue */
- if ( sRefSet_isEmpty(e->sets) )
+ float scale = fsize / tsize;
+
+ DPRINTF (("Scaling constraints by: %f", scale));
+
+ constraintList_elements (c, el)
{
- /* if its not an lvalue we assume it's an rvalue*/
- /* of course if its am lvalue we assume its not an rvalue
- should put in a more accurate test sometime...*/
- e->constraints = constraintList_add (e->constraints, constraint_create (exprData_getUopNode (data), exprNode_undefined, POSITIVE, STRINGLEN ) );
- }
+ DPRINTF (("Scale: %s", constraint_unparse (el)));
+ // constraint_scaleSize (el, scale);
+ DPRINTF ((" ==> %s", constraint_unparse (el)));
+ }
+ end_constraintList_elements;
}
- break;
+ }
+}
- case XPR_POSTOP:
- ret = message ("%s%s",
- exprNode_generateConstraints (exprData_getUopNode (data)),
- lltok_unparse (exprData_getUopTok (data)));
- break;
-
- case XPR_OFFSETOF:
- ret = message ("offsetof(%s,%q)",
- ctype_unparse (qtype_getType (exprData_getOffsetType (data))),
- cstringList_unparseSep (exprData_getOffsetName (data), cstring_makeLiteralTemp (".")));
- break;
-
- case XPR_SIZEOFT:
- ret = message ("sizeof(%s)", ctype_unparse (qtype_getType (exprData_getType (data))));
- break;
-
- case XPR_SIZEOF:
- ret = message ("sizeof(%s)", exprNode_generateConstraints (exprData_getSingle (data)));
- break;
- case XPR_ALIGNOFT:
- ret = message ("alignof(%s)", ctype_unparse (qtype_getType (exprData_getType (data))));
- break;
-
- case XPR_ALIGNOF:
- ret = message ("alignof(%s)", exprNode_generateConstraints (exprData_getSingle (data)));
- break;
-
- case XPR_VAARG:
- ret = message ("va_arg(%s, %q)",
- exprNode_generateConstraints (exprData_getCastNode (data)),
- qtype_unparse (exprData_getCastType (data)));
- break;
-
- case XPR_ITERCALL:
- ret = message ("%q(%q)",
- uentry_getName (exprData_getIterCallIter (data)),
- exprNodeList_unparse (exprData_getIterCallArgs (data)));
- break;
- case XPR_ITER:
- ret = message ("%q(%q) %s %q",
- uentry_getName (exprData_getIterSname (data)),
- exprNodeList_unparse (exprData_getIterAlist (data)),
- exprNode_generateConstraints (exprData_getIterBody (data)),
- uentry_getName (exprData_getIterEname (data)));
- break;
- case XPR_CAST:
- ret = message ("(%q)%s",
- qtype_unparse (exprData_getCastType (data)),
- exprNode_generateConstraints (exprData_getCastNode (data)));
- break;
-
- case XPR_FOR:
- ret = message ("%s %s",
- exprNode_generateConstraints (exprData_getPairA (data)),
- exprNode_generateConstraints (exprData_getPairB (data)));
- break;
-
- case XPR_FORPRED:
- ret = message ("for (%s; %s; %s)",
- exprNode_generateConstraints (exprData_getTripleInit (data)),
- exprNode_generateConstraints (exprData_getTripleTest (data)),
- exprNode_generateConstraints (exprData_getTripleInc (data)));
- break;
-
- case XPR_GOTO:
- ret = message ("goto %s", exprData_getLiteral (data));
- break;
-
- case XPR_CONTINUE:
- ret = cstring_makeLiteral ("continue");
- break;
-
- case XPR_BREAK:
- ret = cstring_makeLiteral ("break");
- break;
-
- case XPR_RETURN:
- ret = message ("return %s", exprNode_generateConstraints (exprData_getSingle (data)));
- break;
-
- case XPR_NULLRETURN:
- ret = cstring_makeLiteral ("return");
- break;
-
- case XPR_COMMA:
- ret = message ("%s, %s",
- exprNode_generateConstraints (exprData_getPairA (data)),
- exprNode_generateConstraints (exprData_getPairB (data)));
- break;
-
- case XPR_COND:
- ret = message ("%s ? %s : %s",
- exprNode_generateConstraints (exprData_getTriplePred (data)),
- exprNode_generateConstraints (exprData_getTripleTrue (data)),
- exprNode_generateConstraints (exprData_getTripleFalse (data)));
- break;
- case XPR_IF:
- ret = message ("if (%s) %s",
- exprNode_generateConstraints (exprData_getPairA (data)),
- exprNode_generateConstraints (exprData_getPairB (data)));
- break;
-
- case XPR_IFELSE:
- ret = message ("if (%s) %s else %s",
- exprNode_generateConstraints (exprData_getTriplePred (data)),
- exprNode_generateConstraints (exprData_getTripleTrue (data)),
- exprNode_generateConstraints (exprData_getTripleFalse (data)));
- break;
- case XPR_WHILE:
- ret = message ("while (%s) %s",
- exprNode_generateConstraints (exprData_getPairA (data)),
- exprNode_generateConstraints (exprData_getPairB (data)));
- break;
-
- case XPR_WHILEPRED:
- ret = cstring_copy (exprNode_generateConstraints (exprData_getSingle (data)));
- break;
-
- case XPR_TOK:
- ret = cstring_copy (lltok_unparse (exprData_getTok (data)));
- break;
-
- case XPR_DOWHILE:
- ret = message ("do { %s } while (%s)",
- exprNode_generateConstraints (exprData_getPairB (data)),
- exprNode_generateConstraints (exprData_getPairA (data)));
- break;
-
- case XPR_BLOCK:
- ret = message ("{ %s }", exprNode_generateConstraints (exprData_getSingle (data)));
- e->constraints = (exprData_getSingle (data))->constraints;
- break;
-
- case XPR_STMT:
- ret = cstring_copy (exprNode_generateConstraints (exprData_getSingle (data)));
- e->constraints = (exprData_getSingle (data))->constraints;
- break;
-
- case XPR_STMTLIST:
- ret = message ("%s;%d %s",
- exprNode_generateConstraints (exprData_getPairA (data)), temp++,
- exprNode_generateConstraints (exprData_getPairB (data)));
- e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) );
- break;
-
- case XPR_FTDEFAULT:
- case XPR_DEFAULT:
- ret = cstring_makeLiteral ("default:");
- break;
-
- case XPR_SWITCH:
- ret = message ("switch (%s) %s",
- exprNode_generateConstraints (exprData_getPairA (data)),
- exprNode_generateConstraints (exprData_getPairB (data)));
- break;
-
- case XPR_FTCASE:
- case XPR_CASE:
- ret = message ("case %s:",
- exprNode_generateConstraints (exprData_getSingle (data)));
- break;
-
- case XPR_INIT:
- ret = message ("%s = %s",
- idDecl_getName (exprData_getInitId (data)),
- exprNode_generateConstraints (exprData_getInitNode (data)));
- break;
-
- case XPR_FACCESS:
- ret = message ("%s.%s",
- exprNode_generateConstraints (exprData_getFieldNode (data)),
- exprData_getFieldName (data));
- break;
-
- case XPR_ARROW:
- ret = message ("%s->%s",
- exprNode_generateConstraints (exprData_getFieldNode (data)),
- exprData_getFieldName (data));
- break;
-
- case XPR_STRINGLITERAL:
- ret = cstring_copy (exprData_getLiteral (data));
- break;
-
- case XPR_NUMLIT:
- ret = cstring_copy (exprData_getLiteral (data));
- break;
-
- case XPR_NODE:
- ret = cstring_makeLiteral ("<node>");
- break;
+constraintList constraintList_sort (/*@returned@*/ constraintList ret)
+{
+ if (constraintList_isUndefined(ret) )
+ {
+ llassert(FALSE);
+ return ret;
}
- 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