can do g[0] = '2'; g++; g[0] = 'g'; I think...
struct _constraintTerm {
+ constraintType constrType;
fileloc loc;
constraintTermValue value;
constraintTermType kind;
abst_typedef struct _constraintTerm * constraintTerm;
struct constraintExpr_ {
- constraintType c1;
- constraintTerm t1;
+
+ constraintTerm term;
constraintExprOp op;
- struct constraintExpr_ * e1;
+ struct constraintExpr_ * expr;
};
# define constraintExpr_undefined ((constraintExpr)NULL)
struct _constraint {
- constraintType c1;
- constraintTerm t1;
+ constraintExpr lexpr;
arithType ar;
- constraintExpr e1;
+ constraintExpr expr;
bool post;
} ;
constraintTerm intLit_makeConstraintTerm (int p_i);
/*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
- /*@post:isnull result->e1@*/
+ /*@post:isnull result->expr@*/
/*@post:notnull result->t1@*/
- /*@defines result->e1, result->t1, result->c1@, result->op*/;
+ /*@defines result->expr, result->t1, result->c1@, result->op*/;
constraintExpr makeConstraintExprIntlit (int p_i);
constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint);
constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc p_sequencePoint);
-void constraintType_print (constraintType c1);
+cstring constraintType_print (constraintType c1);
+constraint constraint_copy (constraint c);
constraintExpr makePostOpInc (exprNode t1);
-void constraintTerm_print (constraintTerm term);
+cstring constraintTerm_print (constraintTerm term);
-void arithType_print (arithType ar);
+cstring arithType_print (arithType ar);
-void constraintExpr_print (constraintExpr ex);
+cstring constraintExpr_print (constraintExpr ex);
-void constraint_print (constraint c);
+cstring constraint_print (constraint c);
/*@=czechfcns*/
-//#warning take this out
+#warning take this out
#include "constraintList.h"
+#include "constraintTerm.h"
extern /*@only@*/ constraintList constraintList_new(void);
extern constraintList constraintList_add (/*@returned@*/ constraintList p_s, /*@only@*/ constraint p_el) ;
+extern constraintList constraintList_addList (/*@returned@*/ constraintList s, /*@only@*/constraintList new);
+
+
extern constraintList constraintList_copy (constraintList p_s);
//extern /*@only@*/ cstring constraintList_unparse (constraintList p_s) ;
extern void constraintList_free (/*@only@*/ constraintList p_s) ;
+
+extern constraintList constraintList_copy (constraintList s);
+
+extern cstring constraintList_print (constraintList s);
/*@constant int constraintListBASESIZE;@*/
# define constraintListBASESIZE SMALLBASESIZE
--- /dev/null
+
+constraintTerm constraintTerm_copy (constraintTerm term);
+
+constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e);
+
+constraintTerm constraintTerm_makeMaxSetexpr (exprNode e);
+
+constraintTerm constraintTerm_makeMinSetexpr (exprNode e);
+
+constraintTerm constraintTerm_makeMaxReadexpr (exprNode e);
+
+constraintTerm constraintTerm_makeMinReadexpr (exprNode e);
+
+constraintTerm constraintTerm_makeValueexpr (exprNode e);
+
+constraintTerm intLit_makeConstraintTerm (int i);
+
+constraintTerm constraintTerm_makeIntLitValue (int i);
+
+cstring constraintType_print (constraintType constrType);
+
+cstring constraintTerm_print (constraintTerm term);
+
+
/*@relnull@*/ exprData edata;
cstring etext;
environmentTable environment;
- constraintList constraints;
+ constraintList requiresConstraints;
+ constraintList ensuresConstraints;
} ;
/*@constant null exprNode exprNode_undefined; @*/
/*@constant observer char *LCL_PARSE_VERSION;@*/
# define LCL_PARSE_VERSION "LCLint 2.5q"
/*@constant observer char *LCL_COMPILE;@*/
-# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g on FreeBSD shankly.cs.virginia.edu 3.2-RELEASE FreeBSD 3.2-RELEASE #0: Tue May 18 04:05:08 GMT 1999 jkh@cathair:/usr/src/sys/compile/GENERIC i386 by drl7x"
+# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on SunOS cobra.cs.Virginia.EDU 5.6 Generic_105181-13 sun4u sparc SUNW,Ultra-60 by drl7x"
/*@constant observer char *LCL_PARSE_VERSION;@*/
# define LCL_PARSE_VERSION "LCLint 2.5q"
/*@constant observer char *LCL_COMPILE;@*/
-# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g on FreeBSD shankly.cs.virginia.edu 3.2-RELEASE FreeBSD 3.2-RELEASE #0: Tue May 18 04:05:08 GMT 1999 jkh@cathair:/usr/src/sys/compile/GENERIC i386 by drl7x"
+# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on SunOS cobra.cs.Virginia.EDU 5.6 Generic_105181-13 sun4u sparc SUNW,Ultra-60 by drl7x"
/*DRL add 9/4/00 */
-extern
extern void usymtab_testInRange (sRef p_s, int p_index) /*@modifies internalState;@*/;
extern void usymtab_postopVar (sRef p_sr) /*@modifies internalState;@*/ ;
GENERALSRC = cstring.c fileloc.c message.c source.c \
fileTable.c hashTable.c llerror.c messageLog.c \
constraint.c \
+ constraintTerm.c \
+ constraintResolve.c \
environmentTable.c \
constraintList.c \
constraintGeneration.c \
-1, -1, 185
};
/* -*-C-*- Note some compilers choke on comments on `#line' lines. */
-#line 3 "/usr/share/misc/bison.simple"
+#line 3 "/gnu/share/bison.simple"
/* Skeleton output parser for bison,
Copyright (C) 1984, 1989, 1990 Free Software Foundation, Inc.
#endif
#endif
\f
-#line 196 "/usr/share/misc/bison.simple"
+#line 196 "/gnu/share/bison.simple"
/* The user can define YYPARSE_PARAM as the name of an argument to be passed
into yyparse. The argument should have type void *.
break;}
}
/* the action file gets copied in in place of this dollarsign */
-#line 498 "/usr/share/misc/bison.simple"
+#line 498 "/gnu/share/bison.simple"
\f
yyvsp -= yylen;
yyssp -= yylen;
/*@-fcnuse*/
/*@-assignexpose*/
+/*@notnull@*/
+/*@special@*/ constraint constraint_makeNew (void)
+ /*@post:isnull result->term, result->expr, result->constrType@*/
+ /*@defines result->ar, result->post@*/;
+
constraint constraint_copy (constraint c)
{
constraint ret;
ret = constraint_makeNew();
- ret->c1 = c->c1;
- ret->t1 = c->t1;
+ ret->lexpr = c->lexpr;
ret->ar = c->ar;
- ret->e1 = c->e1;
+ ret->expr = c->expr;
ret->post = c->post;
return ret;
}
/*@notnull@*/
/*@special@*/ constraint constraint_makeNew (void)
- /*@post:isnull result->t1, result->e1, result->c1@*/
+ /*@post:isnull result->term, result->expr, result->constrType@*/
/*@defines result->ar, result->post@*/
{
constraint ret;
ret = dmalloc(sizeof (*ret) );
- ret->t1 = NULL;
- ret->e1 = NULL;
- ret->c1 = NULL;
+ ret->lexpr = NULL;
+ ret->expr = NULL;
ret->ar = LT;
ret->post = FALSE;
/*@i23*/return ret;
}
/*@-czechfcns@*/
+constraintExpr constraintExpr_alloc ()
+{
+ constraintExpr ret;
+ ret = dmalloc (sizeof (*ret) );
+ ret->term = NULL;
+ ret->expr = NULL;
+ ret->op = PLUS;
+ return ret;
+}
-/*@out@*/ constraintTerm new_constraintTermExpr (void)
+constraintExpr constraintExpr_copy (constraintExpr expr)
{
- constraintTerm ret;
- ret = dmalloc (sizeof (* ret ) );
+ constraintExpr ret;
+ ret = constraintExpr_alloc();
+ ret->term = constraintTerm_copy(expr->term);
+ ret->op = expr->op;
+ if (expr->expr != NULL)
+ {
+ ret->expr = constraintExpr_copy (expr->expr);
+ }
+ else
+ {
+ ret->expr = NULL;
+ }
+}
+
+constraintExpr constraintExpr_makeMaxSetExpr (exprNode expr)
+{
+ constraintExpr ret;
+ ret = constraintExpr_alloc();
+ ret->term = constraintTerm_makeMaxSetexpr(expr);
return ret;
}
-constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e)
+constraintExpr constraintExpr_makeMaxReadExpr (exprNode expr)
{
- constraintTerm ret = new_constraintTermExpr();
- ret->loc = exprNode_getfileloc(e);
- ret->value.expr = e;
- ret->kind = EXPRNODE;
+ constraintExpr ret;
+ ret = constraintExpr_alloc();
+ ret->term = constraintTerm_makeMaxReadexpr(expr);
return ret;
}
+constraintExpr constraintExpr_makeMinSetExpr (exprNode expr)
+{
+ constraintExpr ret;
+ ret = constraintExpr_alloc();
+ ret->term = constraintTerm_makeMinSetexpr(expr);
+ return ret;
+}
-constraintTerm intLit_makeConstraintTerm (int i)
+constraintExpr constraintExpr_makeMinReadExpr (exprNode expr)
{
- constraintTerm ret = new_constraintTermExpr();
- ret->value.intlit = i;
- ret->kind = INTLITERAL;
- ret->loc = fileloc_undefined;
+ constraintExpr ret;
+ ret = constraintExpr_alloc();
+ ret->term = constraintTerm_makeMinReadexpr(expr);
return ret;
}
-
-/*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
- /*@post:isnull result->e1@*/
- /*@post:notnull result->t1@*/
- /*@defines result->e1, result->t1, result->c1@, result->op*/
+constraintExpr constraintExpr_makeValueExpr (exprNode expr)
{
constraintExpr ret;
- ret = dmalloc (sizeof (*ret) );
- ret->t1 = term;
- ret->e1 = NULL;
- ret->c1 = UNDEFINED;
- ret->op = PLUS;
+ ret = constraintExpr_alloc();
+ ret->term = constraintTerm_makeValueexpr(expr);
return ret;
}
- constraintExpr makeConstraintExprIntlit (int i)
+constraintExpr makeConstraintExprIntlit (int i)
{
constraintExpr ret;
ret = dmalloc (sizeof (*ret) );
- ret->t1 = intLit_makeConstraintTerm (i);
- ret->e1 = NULL;
- ret->c1 = VALUE;
+ ret->term = constraintTerm_makeIntLitValue(i);
+ ret->expr = NULL;
ret->op = PLUS;
/*@i1*/ return ret;
}
-
-/*@i33*/
-/*@null@*/ constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
-{
- constraint ret = constraint_makeNew();
- constraintTerm term;
- po = exprNode_fakeCopy(po);
- ind = exprNode_fakeCopy(ind);
- printf ("Requires maxr(%s) >= %s\n", cstring_toCharsSafe (exprNode_unparse (po ) ),
- cstring_toCharsSafe ( exprNode_unparse (ind) ) );
- ret->t1 = exprNode_makeConstraintTerm(po);
- ret->c1 = MAXREAD;
- ret->ar = GTE;
- term = exprNode_makeConstraintTerm (ind);
-
- ret->e1 = makeConstraintExpr (term);
- ret->e1->c1 = VALUE;
- /*@i1*/return ret;
+constraintExpr constraintExpr_makeValueInt (int i)
+{
+ return makeConstraintExprIntlit(i);
}
constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
{
constraint ret = constraint_makeNew();
constraintTerm term;
- printf ("Requires maxw(%s) >= %s\n", cstring_toCharsSafe (exprNode_unparse (po ) ),
- cstring_toCharsSafe( exprNode_unparse (ind) ) );
- ret->t1 = exprNode_makeConstraintTerm(po);
- ret->c1 = MAXSET;
+
+ ret->lexpr =constraintExpr_makeMaxSetExpr(po);
ret->ar = GTE;
-
- term = exprNode_makeConstraintTerm(ind);
-
- ret->e1 = makeConstraintExpr (term);
- ret->e1->c1 = VALUE;
+ ret->expr = constraintExpr_makeValueExpr (ind);
/*@i1*/return ret;
}
+
+constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
+{
+ constraint ret = constraint_makeNew();
+ // constraintTerm term;
+ po = exprNode_fakeCopy(po);
+ ind = exprNode_fakeCopy(ind);
+ ret->lexpr = constraintExpr_makeMaxReadExpr(po);
+ ret->ar = GTE;
+ ret->expr = constraintExpr_makeValueExpr (ind);
+ return ret;
+}
-
-constraint constraint_makeReadSafeInt (exprNode t1, int index)
+constraint constraint_makeWriteSafeInt (exprNode po, int ind)
{
constraint ret = constraint_makeNew();
constraintTerm term;
- printf ("Ensures maxr((valueof(%s)) >= %d\n", cstring_toCharsSafe (exprNode_unparse (t1 ) ),
- index );
- t1 = exprNode_fakeCopy(t1);
- ret->t1 = exprNode_makeConstraintTerm(t1);
- ret->c1 = MAXREAD;
+
+ ret->lexpr =constraintExpr_makeMaxSetExpr(po);
ret->ar = GTE;
- ret->post = TRUE;
- term = intLit_makeConstraintTerm(index);
-
- ret->e1 = makeConstraintExpr (term);
- ret->e1->c1 = VALUE;
- /*make this refer to element after preconditions */
- fileloc_incColumn (ret->t1->loc);
- /*@i1*/ return ret;
+ ret->expr = constraintExpr_makeValueInt (ind);
+ /*@i1*/return ret;
}
+
+constraint constraint_makeReadSafeInt ( exprNode po, int ind)
+{
+ constraint ret = constraint_makeNew();
+ po = exprNode_fakeCopy(po);
+
+ ret->lexpr = constraintExpr_makeMaxReadExpr(po);
+ ret->ar = GTE;
+ ret->expr = constraintExpr_makeValueInt (ind);
+ return ret;
+}
-constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
+constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
{
constraint ret = constraint_makeNew();
constraintTerm term;
- t1 = exprNode_fakeCopy (t1);
+ e1 = exprNode_fakeCopy (e1);
t2 = exprNode_fakeCopy (t2);
- ret->t1 = exprNode_makeConstraintTerm(t1);
-
- if (ret->t1->loc != NULL)
- fileloc_free(ret->t1->loc);
+ ret = constraint_makeReadSafeExprNode(e1, t2);
+ if (ret->lexpr->term->loc != NULL)
+ fileloc_free(ret->lexpr->term->loc);
- ret->t1->loc = fileloc_copy (sequencePoint);
- ret->c1 = MAXREAD;
- ret->ar = GTE;
+ ret->lexpr->term->loc = fileloc_copy (sequencePoint);
ret->post = TRUE;
- term = exprNode_makeConstraintTerm (t2);
-
- ret->e1 = makeConstraintExpr (term);
- ret->e1->c1 = VALUE;
- /*make this refer to element after preconditions */
- fileloc_incColumn (ret->t1->loc);
- /*@i1*/ return ret;
+
+ fileloc_incColumn (ret->lexpr->term->loc);
+ return ret;
}
+
constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint)
{
constraint ret = constraint_makeNew();
constraintTerm term;
+ po = exprNode_fakeCopy(po);
+ ind = exprNode_fakeCopy(ind);
- po = exprNode_fakeCopy (po);
- ind = exprNode_fakeCopy (ind);
-
- ret->t1 = exprNode_makeConstraintTerm(po);
- ret->c1 = MINREAD;
+ ret->lexpr = constraintExpr_makeMinReadExpr(po);
ret->ar = LTE;
+ ret->expr = constraintExpr_makeValueExpr (ind);
ret->post = TRUE;
- term = exprNode_makeConstraintTerm (ind);
+
+ if (ret->lexpr->term->loc != NULL)
+ fileloc_free(ret->lexpr->term->loc);
- ret->e1 = makeConstraintExpr (term);
- ret->e1->c1 = VALUE;
+ ret->lexpr->term->loc = fileloc_copy (sequencePoint);
/*make this refer to element after preconditions */
- fileloc_incColumn (ret->t1->loc);
+ fileloc_incColumn (ret->lexpr->term->loc);
/*@i1*/ return ret;
}
-constraintExpr makePostOpInc (exprNode t1)
+constraintExpr makeMaxSetPostOpInc (exprNode e)
{
constraintExpr ret;
- constraintTerm term;
-
- t1 = exprNode_fakeCopy (t1);
- term = exprNode_makeConstraintTerm(t1);
- ret = makeConstraintExpr (term);
- ret->op = PLUS;
- ret->c1 = VALUE;
- ret->e1 = makeConstraintExprIntlit (1);
+ ret = constraintExpr_makeValueExpr (e);
+ ret->term = constraintTerm_makeMaxSetexpr (e);
+ ret->op = MINUS;
+ ret->expr = makeConstraintExprIntlit (1);
return ret;
}
-constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc sequencePoint)
+constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
{
constraint ret = constraint_makeNew();
//constraintTerm term;
exprNode t2;
- t1 = exprNode_fakeCopy(t1);
- t2 = exprNode_fakeCopy(t1);
-
- ret->t1 = exprNode_makeConstraintTerm(t1);
- ret->c1 = VALUE;
+ e = exprNode_fakeCopy(e);
+ ret->lexpr = constraintExpr_makeMaxSetExpr(e);
ret->ar = EQ;
ret->post = TRUE;
- ret->e1 = makePostOpInc(t2);
+ ret->expr = makeMaxSetPostOpInc(e);
- fileloc_incColumn ( ret->t1->loc);
- fileloc_incColumn ( ret->t1->loc);
-
- /*@i6*/return ret;
+ fileloc_incColumn ( ret->lexpr->term->loc);
+ fileloc_incColumn ( ret->lexpr->term->loc);
+ return ret;
}
-void constraintType_print (constraintType c1)
+constraintExpr makeMaxReadPostOpInc (exprNode e)
{
- switch (c1)
- {
- case VALUE:
- printf("VALUE");
- break;
- case CALLSAFE:
- printf("CALLSAFE");
- break;
- case MAXSET:
- printf ("MAXSET");
- break;
- case MINSET:
- printf ("MINSET");
- break;
- case MAXREAD:
- printf ("MAXREAD");
- break;
- case MINREAD:
- printf ("MINREAD");
- break;
- case NULLTERMINATED:
- printf ("NULLTERMINATED");
- break;
- case UNDEFINED:
- TPRINTF(("Unhandled value for constraintType"));
- llassert(FALSE);
- break;
- default:
- TPRINTF(("Unhandled value for constraintType"));
- llassert(FALSE);
- }
+ constraintExpr ret;
+ ret = constraintExpr_makeValueExpr (e);
+ ret->term = constraintTerm_makeMaxReadexpr (e);
+ ret->op = MINUS;
+ ret->expr = makeConstraintExprIntlit (1);
+ return ret;
}
-void constraintTerm_print (constraintTerm term)
+
+constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
{
- cstring s;
+ constraint ret = constraint_makeNew();
+ //constraintTerm term;
+ exprNode t2;
+ e = exprNode_fakeCopy(e);
+ ret->lexpr = constraintExpr_makeMaxReadExpr(e);
+ ret->ar = EQ;
+ ret->post = TRUE;
+ ret->expr = makeMaxReadPostOpInc(e);
- llassert (term != NULL);
- switch (term->kind)
- {
- case EXPRNODE:
- s = exprNode_unparse (term->value.expr);
- printf(" %s", cstring_toCharsSafe(s) );
- s = fileloc_unparse (term->loc);
- printf("@ %s", cstring_toCharsSafe(s) );
- cstring_free(s);
- break;
- case INTLITERAL:
- {
- char * buf = malloc (15);
- /*@i1*/snprintf (buf, 14, "intliteral(%d)", term->value.intlit);
- /*@i1*/ printf(" %s ", buf);
- free (buf);
- break;
- }
- case SREF:
- TPRINTF( ("Not Implemented\n"));
- llassert(FALSE);
- break;
- }
- /*@-unreachable*/
- return;
- /*@=unreachable*/
+ fileloc_incColumn ( ret->lexpr->term->loc);
+ fileloc_incColumn ( ret->lexpr->term->loc);
+ return ret;
}
-void arithType_print (arithType ar)
+
+cstring arithType_print (arithType ar)
{
+ cstring st = cstring_undefined;
switch (ar)
{
case LT:
- printf(" < ");
- return;
+ st = cstring_makeLiteral (" < ");
+ break;
case LTE:
- printf(" <= ");
- return;
+ st = cstring_makeLiteral (" <= ");
+ break;
case GT:
- printf(" > ");
- return;
+ st = cstring_makeLiteral (" > ");
+ break;
case GTE:
- printf(" <= ");
- return;
+ st = cstring_makeLiteral (" >= ");
+ break;
case EQ:
- printf(" == ");
- return;
+ st = cstring_makeLiteral (" == ");
+ break;
case NONNEGATIVE:
- printf(" NONNEGATIVE ");
- return;
+ st = cstring_makeLiteral (" NONNEGATIVE ");
+ break;
case POSITIVE:
- printf(" POSITIVE ");
- return;
+ st = cstring_makeLiteral (" POSITIVE ");
+ break;
default:
llassert(FALSE);
+ break;
}
+ return st;
}
-void constraintExpr_print (constraintExpr ex)
+cstring constraintExpr_print (constraintExpr ex)
{
+ cstring st;
+ cstring opStr;
llassert (ex != NULL);
- constraintType_print (ex->c1 );
- constraintTerm_print (ex->t1);
- if (ex->e1 != NULL)
+
+ st = message ("%s",
+ constraintTerm_print (ex->term));
+
+ if (ex->expr != NULL)
{
if (ex->op == PLUS)
{
- printf(" + ");
+ opStr = cstring_makeLiteral (" + ");
}
else
{
- printf (" - ");
+ opStr = cstring_makeLiteral (" - ");
}
-
- constraintExpr_print (ex->e1);
+ st = message ("%s %s %s", st, opStr, constraintExpr_print (ex->expr) );
}
-
+ return st;
}
-void constraint_print (constraint c)
+cstring constraint_print (constraint c)
{
+ cstring st = cstring_undefined;
+ cstring type = cstring_undefined;
+ llassert (c);
if (c->post)
{
- printf("Ensures: ");
+ type = cstring_makeLiteral ("Ensures: ");
}
else
{
- printf("requires: ");
+ type = cstring_makeLiteral ("Requires: ");
}
-
- constraintType_print (c->c1);
- constraintTerm_print (c->t1);
- arithType_print(c->ar);
- constraintExpr_print(c->e1);
- printf("\n");
+ st = message ("%s: %s %s %s",
+ type,
+ constraintExpr_print (c->lexpr),
+ arithType_print(c->ar),
+ constraintExpr_print(c->expr)
+ );
+ return st;
}
/*@=fcnuse*/
/*@=assignexpose*/
/*@=czechfcns@*/
-
void /*@alt bool@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e);
static bool exprNode_handleError( exprNode p_e);
-static cstring exprNode_findConstraints ( exprNode p_e);
+//static cstring exprNode_findConstraints ( exprNode p_e);
static bool exprNode_isMultiStatement(exprNode p_e);
static bool exprNode_multiStatement (exprNode p_e);
bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint);
-static void exprNode_constraintPropagateUp (exprNode p_e);
+//static void exprNode_constraintPropagateUp (exprNode p_e);
+constraintList exprNode_traversRequiresConstraints (exprNode e);
+constraintList exprNode_traversEnsuresConstraints (exprNode e);
+void mergeResolve (exprNode parent, exprNode child1, exprNode child2);
+
bool exprNode_isUnhandled (exprNode e)
{
llassert( exprNode_isDefined(e) );
bool exprNode_stmt (exprNode e)
{
exprNode snode;
+ fileloc loc;
+ bool notError;
if (exprNode_isError(e) )
{
return FALSE;
}
+ e->requiresConstraints = constraintList_new();
+ e->ensuresConstraints = constraintList_new();
- TPRINTF(( "STMT:") );
- TPRINTF ( ( cstring_toCharsSafe ( exprNode_unparse(e)) )
+
+ DPRINTF(( "STMT:") );
+ DPRINTF ( ( cstring_toCharsSafe ( exprNode_unparse(e)) )
);
if (e->kind != XPR_STMT)
{
- TPRINTF (("Not Stmt") );
+ DPRINTF (("Not Stmt") );
+ DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
if (exprNode_isMultiStatement (e) )
{
return exprNode_multiStatement (e );
}
llassert(FALSE);
}
-
+
+ DPRINTF (("Stmt") );
+ DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
+
snode = exprData_getUopNode (e->edata);
/* could be stmt involving multiple statements:
llassert(FALSE);
return exprNode_multiStatement (snode);
}
- else
- {
- fileloc loc;
- bool notError;
- loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
- notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc);
- llassert(notError);
- fileloc_free (loc);
- return notError;
- }
+
+ loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
+ notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc);
+ e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
+ printf ("%s\n", constraintList_print(e->requiresConstraints) );
+ e->ensuresConstraints = exprNode_traversEnsuresConstraints(snode);
+ printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
+ llassert(notError);
+ return notError;
+
}
bool exprNode_stmtList (exprNode e)
{
+ exprNode stmt1, stmt2;
if (exprNode_isError (e) )
{
return FALSE;
}
+
+ e->requiresConstraints = constraintList_new();
+ e->ensuresConstraints = constraintList_new();
+
/*Handle case of stmtList with only one statement:
The parse tree stores this as stmt instead of stmtList*/
if (e->kind != XPR_STMTLIST)
return exprNode_stmt(e);
}
llassert (e->kind == XPR_STMTLIST);
- TPRINTF(( "STMTLIST:") );
- TPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
- (void) exprNode_stmt (exprData_getPairA (e->edata));
- TPRINTF(("\nstmt after stmtList call " ));
- // e->constraints = constraintList_exprNodemerge (exprData_getPairA (e->edata), exprData_getPairB (e->edata) );
- return exprNode_stmt (exprData_getPairB (e->edata));
+ DPRINTF(( "STMTLIST:") );
+ DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
+ stmt1 = exprData_getPairA (e->edata);
+ stmt2 = exprData_getPairB (e->edata);
+
+
+ exprNode_stmt (stmt1);
+ DPRINTF(("\nstmt after stmtList call " ));
+
+ exprNode_stmt (stmt2);
+
+ mergeResolve (e, stmt1, stmt2 );
+ TPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
+ constraintList_print(e->requiresConstraints),
+ constraintList_print(e->ensuresConstraints) ) ) );
+ return TRUE;
}
+
bool exprNode_multiStatement (exprNode e)
{
exprNode_generateConstraints (exprData_getTripleInc (data));
break;
case XPR_IF:
- TPRINTF(( "IF:") );
- TPRINTF ((exprNode_unparse(e) ) );
+ DPRINTF(( "IF:") );
+ DPRINTF ((exprNode_unparse(e) ) );
// ret = message ("if (%s) %s",
exprNode_generateConstraints (exprData_getPairA (data));
exprNode_generateConstraints (exprData_getPairB (data));
case XPR_BLOCK:
// ret = message ("{ %s }",
exprNode_generateConstraints (exprData_getSingle (data));
- e->constraints = (exprData_getSingle (data))->constraints;
+ e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
+ e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
+ // e->constraints = (exprData_getSingle (data))->constraints;
break;
case XPR_STMT:
}
-/* void upwrap (exprNode e) */
-/* { */
-/* printf ("in upwrap with e = %X\n" , e); */
-/* printf ("%s\n", exprNode_unparse (e) ); */
-/* } */
-
-
-
bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv, fileloc sequencePoint)
{
exprNode t1, t2;
bool handledExprNode;
- char * mes;
exprData data;
- constraintExpr tmp;
constraint cons;
DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
+
+ e->requiresConstraints = constraintList_new();
+ e->ensuresConstraints = constraintList_new();
if (exprNode_handleError (e))
{
case XPR_FETCH:
- /*
- Make sure these are right!
-
- if (rvalue)
- valueOf (index) <= maxRead (array)
- valueOf (index) >= minRead (array)
- else lvalue
- valueOf (index) <= maxSet (array)
- valueOf (index) >= minSet (array)
- */
if (definatelv )
{
t1 = (exprData_getPairA (data) );
t2 = (exprData_getPairB (data) );
- cons = constraint_makeWriteSafeExprNode (t1, t2);
+ cons = constraint_makeWriteSafeExprNode (t1, t2);
}
else
{
t1 = (exprData_getPairA (data) );
t2 = (exprData_getPairB (data) );
- cons = constraint_makeReadSafeExprNode (t1, t2 );
+ cons = constraint_makeReadSafeExprNode (t1, t2 );
}
- e->constraints = constraintList_add(e->constraints, cons);
- constraint_print (cons);
+
+ e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
- constraint_print (cons);
+ e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
- constraint_print (cons);
-
+ e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
+
exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
/*@i325 Should check which is array/index. */
-
-
break;
case XPR_PREOP:
t1 = exprData_getUopNode(data);
{
if (definatelv)
{
- printf ("Requires maxs(%s) > %d \n", exprNode_unparse (exprData_getUopNode (data) ), 0 );
+ cons = constraint_makeWriteSafeInt (t1, 0);
}
else
{
cons = constraint_makeReadSafeInt (t1, 0);
- constraint_print(cons);
}
+ e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
+ }
+ if (lltok_isInc_Op (exprData_getUopTok (data) ) )
+ {
+ // cons = constraint_makeSideEffectPostIncrement (t1, sequencePoint);
+ // e->ensuresConstraints = constraintList_add(e->requiresConstraints, cons);
}
-
break;
case XPR_PARENS:
exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
- e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
+ // e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
break;
case XPR_ASSIGN:
exprNode_exprTraverse (exprData_getOpA (data), TRUE, definaterv, sequencePoint );
lltok_unparse (exprData_getOpTok (data));
exprNode_exprTraverse (exprData_getOpB (data), definatelv, TRUE, sequencePoint );
- e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data) );
+ // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data) );
break;
case XPR_OP:
exprNode_exprTraverse (exprData_getOpA (data), definatelv, definaterv, sequencePoint );
lltok_unparse (exprData_getOpTok (data));
exprNode_exprTraverse (exprData_getOpB (data), definatelv, definaterv, sequencePoint );
- e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
+ // e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
break;
case XPR_SIZEOFT:
ctype_unparse (qtype_getType (exprData_getType (data) ) );
case XPR_SIZEOF:
exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
- e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
+ // e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
break;
case XPR_CALL:
exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
lltok_unparse (exprData_getUopTok (data));
- e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
if (lltok_isInc_Op (exprData_getUopTok (data) ) )
{
+ TPRINTF(("doing ++"));
t1 = exprData_getUopNode (data);
- cons = constraint_makeSideEffectPostIncrement (t1, sequencePoint );
- constraint_print (cons);
- // printf("Side Effect: %s = (%s)0 +1 ", exprNode_unparse (exprData_getUopNode (data) ), exprNode_unparse (exprData_getUopNode(data) ) );
+ cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
+ e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
+ cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint );
+ e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
}
break;
default:
return handledExprNode;
}
-/* void exprNode_constraintPropagateUp (exprNode e) */
-/* { */
-
-/* cstring ret; */
-/* exprData data; */
-
-/* if (exprNode_handleError (e) ) */
-/* { */
-/* return; */
-/* } */
-
-/* data = e->edata; */
-
-/* switch (e->kind) */
-/* { */
-/* case XPR_PARENS: */
-/* e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined); */
-/* break; */
-/* case XPR_ASSIGN: */
-/* e->constraints = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data) ); */
-/* break; */
-/* case XPR_CALL: */
-/* // e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT, CALLSAFE ) ); */
-/* break; */
-/* case XPR_INITBLOCK: */
-/* //("{ %q }" */
-/* exprNodeList_unparse (exprData_getArgs (data) ); */
-/* // e->constraints = constraintList_exprNodemerge (exprData_getArgs (data), exprData_getOpB (data) ); */
-/* break; */
-
-/* case XPR_OP: */
-/* // 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_ALIGNOF: */
-/* e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined); */
-/* break; */
-
-/* case XPR_VAARG: */
-/* e->constraints = constraintList_exprNodemerge (exprData_getCastNode (data), exprNode_undefined); */
-/* break; */
-
-/* case XPR_ITERCALL: */
-/* // ret = message ("%q(%q)", */
-/* // uentry_getName (exprData_getIterCallIter (data)), */
-/* // exprNodeList_unparse (exprData_getIterCallArgs (data))); */
-/* //// e->constraints = constraintList_exprNodemerge (exprData_getIterCallArgs (data), exprNode_undefined); */
-/* break; */
-/* case XPR_ITER: */
-/* DPRINTF(("XPR_ITER NOT IMPLEMENTED" )); */
-/* // 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: */
-/* e->constraints = constraintList_exprNodemerge (exprData_getCastNode (data), exprNode_undefined); */
-/* break; */
-
-/* default: */
-/* DPRINTF(("NOT Currently IMplemented")); */
-/* } */
-/* } */
-
-/* //Not used below */
-
-/* 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))); */
-/* e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),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))); */
-/* e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), 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; %s", */
-/* exprNode_generateConstraints (exprData_getPairA (data)), */
-/* 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; */
-/* } */
-
-/* return ret; */
-/* } */
+/* walk down the tree and get all requires Constraints in each subexpression*/
+constraintList exprNode_traversRequiresConstraints (exprNode e)
+{
+ // exprNode t1, t2;
+
+ bool handledExprNode;
+ // char * mes;
+ exprData data;
+ constraintList ret;
+ ret = constraintList_copy (e->requiresConstraints );
+ if (exprNode_handleError (e))
+ {
+ return ret;
+ }
+
+ handledExprNode = TRUE;
+
+ data = e->edata;
+
+ switch (e->kind)
+ {
+
+ case XPR_FETCH:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getPairA (data) ) );
+
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getPairB (data) ) );
+ break;
+ case XPR_PREOP:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getUopNode (data) ) );
+ break;
+
+ case XPR_PARENS:
+ ret = constraintList_addList (ret, exprNode_traversRequiresConstraints
+ (exprData_getUopNode (data) ) );
+ break;
+ case XPR_ASSIGN:
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getOpA (data) ) );
+
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getOpB (data) ) );
+ break;
+ case XPR_OP:
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getOpA (data) ) );
+
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getOpB (data) ) );
+ break;
+ case XPR_SIZEOFT:
+
+ // ctype_unparse (qtype_getType (exprData_getType (data) ) );
+
+ break;
+
+ case XPR_SIZEOF:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getSingle (data) ) );
+ break;
+
+ case XPR_CALL:
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getFcn (data) ) );
+ /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
+ break;
+
+ case XPR_RETURN:
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getSingle (data) ) );
+ break;
+
+ case XPR_NULLRETURN:
+ // cstring_makeLiteral ("return");;
+ break;
+
+ case XPR_FACCESS:
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getFieldNode (data) ) );
+ //exprData_getFieldName (data) ;
+ break;
+
+ case XPR_ARROW:
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getFieldNode (data) ) );
+ // exprData_getFieldName (data);
+ break;
+
+ case XPR_STRINGLITERAL:
+ // cstring_copy (exprData_getLiteral (data));
+ break;
+
+ case XPR_NUMLIT:
+ // cstring_copy (exprData_getLiteral (data));
+ break;
+ case XPR_POSTOP:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversRequiresConstraints
+ (exprData_getUopNode (data) ) );
+ break;
+ default:
+ break;
+ }
+
+ return ret;
+}
+
+
+/* walk down the tree and get all Ensures Constraints in each subexpression*/
+constraintList exprNode_traversEnsuresConstraints (exprNode e)
+{
+ // exprNode t1, t2;
+
+ bool handledExprNode;
+ // char * mes;
+ exprData data;
+ // constraintExpr tmp;
+ // constraint cons;
+ constraintList ret;
+ ret = constraintList_copy (e->ensuresConstraints );
+ if (exprNode_handleError (e))
+ {
+ return ret;
+ }
+
+ handledExprNode = TRUE;
+
+ data = e->edata;
+
+ DPRINTF( (message (
+ "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
+ exprNode_unparse (e),
+ constraintList_print(e->ensuresConstraints)
+ )
+ ));
+
+
+ switch (e->kind)
+ {
+
+ case XPR_FETCH:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getPairA (data) ) );
+
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getPairB (data) ) );
+ break;
+ case XPR_PREOP:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getUopNode (data) ) );
+ break;
+
+ case XPR_PARENS:
+ ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints
+ (exprData_getUopNode (data) ) );
+ break;
+ case XPR_ASSIGN:
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getOpA (data) ) );
+
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getOpB (data) ) );
+ break;
+ case XPR_OP:
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getOpA (data) ) );
+
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getOpB (data) ) );
+ break;
+ case XPR_SIZEOFT:
+
+ // ctype_unparse (qtype_getType (exprData_getType (data) ) );
+
+ break;
+
+ case XPR_SIZEOF:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getSingle (data) ) );
+ break;
+
+ case XPR_CALL:
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getFcn (data) ) );
+ /*@i11*/ // exprNodeList_unparse (exprData_getArgs (data) );
+ break;
+
+ case XPR_RETURN:
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getSingle (data) ) );
+ break;
+
+ case XPR_NULLRETURN:
+ // cstring_makeLiteral ("return");;
+ break;
+
+ case XPR_FACCESS:
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getFieldNode (data) ) );
+ //exprData_getFieldName (data) ;
+ break;
+
+ case XPR_ARROW:
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getFieldNode (data) ) );
+ // exprData_getFieldName (data);
+ break;
+
+ case XPR_STRINGLITERAL:
+ // cstring_copy (exprData_getLiteral (data));
+ break;
+
+ case XPR_NUMLIT:
+ // cstring_copy (exprData_getLiteral (data));
+ break;
+ case XPR_POSTOP:
+
+ ret = constraintList_addList (ret,
+ exprNode_traversEnsuresConstraints
+ (exprData_getUopNode (data) ) );
+ break;
+ default:
+ break;
+ }
+DPRINTF( (message (
+ "exprnode_traversEnsuresConstraints call for %s with constraintList of is returning %s",
+ exprNode_unparse (e),
+ // constraintList_print(e->ensuresConstraints),
+ constraintList_print(ret)
+ )
+ ));
+
+
+ return ret;
+}
+
s->elements = newelements;
}
-constraintList_exprNodemerge()
+void constraintList_exprNodemerge()
{
}
constraintList
return s;
}
-/* cstring */
-/* constraintList_unparse (constraintList s) */
-/* { */
-/* int i; */
-/* cstring st = cstring_undefined; */
-/* bool first = TRUE; */
-
-/* for (i = 0; i < s->nelements; i++) */
-/* { */
-/* cstring type = cstring_undefined; */
-/* constraint current = s->elements[i]; */
-
-/* if (current->isObj) */
-/* { */
-/* type = cstring_makeLiteral ("obj "); */
-/* } */
-
-/* if (current->type != NULL) */
-/* { */
-/* type = message (": %q%q", type, lclTypeSpecNode_unparse (current->type)); */
-/* } */
-
-/* if (first) */
-/* { */
-/* st = type; */
-/* first = FALSE; */
-/* } */
-/* else */
-/* { */
-/* st = message ("%q, %q", st, type); */
-/* } */
-/* } */
-
-/* return st; */
-/* } */
+constraintList constraintList_addList (constraintList s, constraintList new)
+{
+ constraintList_elements(new, elem)
+ s = constraintList_add (s, elem);
+ end_constraintList_elements
+ return s;
+}
+
+cstring
+constraintList_print (constraintList s)
+{
+ int i;
+ cstring st = cstring_undefined;
+ bool first = TRUE;
+
+ if (s->nelements == 0)
+ st = cstring_makeLiteral("<List Empty>");
+
+ for (i = 0; i < s->nelements; i++)
+ {
+ cstring type = cstring_undefined;
+ constraint current = s->elements[i];
+
+ if (current != NULL)
+ {
+ cstring 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_free (constraintList s)
return ret;
}
+
+
--- /dev/null
+/*
+** LCLint - 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 lclint: lclint-request@cs.virginia.edu
+** To report a bug: lclint-bug@cs.virginia.edu
+** For more information: http://lclint.cs.virginia.edu
+*/
+/*
+** termNodeList.c
+**
+** based on list_template.c
+**
+** where T has T_equal (or change this) and T_unparse
+*/
+
+# include "lclintMacros.nf"
+# include "llbasic.h"
+
+constraintList constraintList_new ()
+{
+ constraintList s = (constraintList) dmalloc (sizeof (*s));
+
+ s->nelements = 0;
+ s->nspacelow = constraintListGROWLOW;
+ s->nspacehigh = constraintListGROWHI;
+ s->elementsroot = (constraint *) dmalloc (sizeof (*s->elements) * (s->nspacelow + s->nspacehigh));
+ s->elements = s->elementsroot + constraintListGROWLOW;
+ s->current = 0;
+
+ return (s);
+}
+
+static void
+constraintList_grow (constraintList s)
+{
+ int i;
+ constraint *newelements = (constraint *) dmalloc (sizeof (*newelements)
+ * (s->nelements + constraintListBASESIZE));
+
+ for (i = 0; i < s->nelements; i++)
+ {
+ newelements[i + constraintListGROWLOW] = s->elements[i];
+ }
+
+ sfree (s->elementsroot);
+
+ s->nspacelow = constraintListGROWLOW;
+ s->nspacehigh = constraintListGROWHI;
+
+ s->elementsroot = newelements;
+ s->elements = s->elementsroot + s->nspacelow;
+}
+
+void
+constraintList_addh (constraintList s, constraint el)
+{
+ llassert (constraintListGROWHI > 0);
+
+ if (s->nspacehigh <= 0)
+ constraintList_grow (s);
+
+ s->nspacehigh--;
+ s->elements[s->nelements] = el;
+ s->nelements++;
+}
+
+constraintList
+constraintList_push (constraintList s, constraint el)
+{
+ constraintList_addh (s, el);
+ return s;
+}
+
+void constraintList_insertList (constraintList
+
+void
+constraintList_addl (constraintList s, constraint el)
+{
+ llassert (constraintListGROWLOW > 0);
+
+ if (s->nspacelow <= 0)
+ constraintList_grow (s);
+
+ s->nspacelow--;
+ s->elements--;
+ s->elements[0] = el;
+ s->current++;
+ s->nelements++;
+}
+
+void
+constraintList_reset (constraintList s)
+{
+ s->current = 0;
+}
+
+void
+constraintList_finish (constraintList s)
+{
+ s->current = s->nelements - 1;
+}
+
+void
+constraintList_advance (constraintList s)
+{
+ s->current++;
+ llassert (s->current < s->nelements);
+}
+
+/*@exposed@*/ constraint
+constraintList_head (constraintList s)
+{
+ llassert (s->nelements > 0);
+ return (s->elements[0]);
+}
+
+/*@only@*/ constraintList
+constraintList_copy (constraintList s)
+{
+ constraintList r = constraintList_new ();
+
+ constraintList_elements (s, x)
+ {
+ constraintList_addh (r, constraint_copySafe (x));
+ } end_constraintList_elements;
+
+ return r;
+}
+
+/*@exposed@*/ constraint
+constraintList_current (constraintList s)
+{
+ llassert (!(s->current >= s->nelements));
+ return (s->elements[s->current]);
+}
+
+constraint
+constraintList_getN (constraintList s, int n)
+{
+ llassert (n >= 0 && n < s->nelements);
+
+ return (s->elements[n]);
+}
+
+/*@only@*/ cstring
+constraintList_unparse (constraintList s)
+{
+ bool first = TRUE;
+ cstring st = cstring_undefined;
+
+ constraintList_elements (s, current)
+ {
+ if (first)
+ {
+ st = constraint_unparse (current);
+ first = FALSE;
+ }
+ else
+ st = message ("%q, %q", st, constraint_unparse (current));
+ } end_constraintList_elements;
+
+ return st;
+}
+
+///* /*@only@*/ cstring */
+/* constraintList_unparseTail (constraintList s) */
+/* { */
+/* bool head = TRUE; */
+/* bool first = TRUE; */
+/* cstring st = cstring_undefined; */
+
+/* constraintList_elements (s, current) */
+/* { */
+/* if (head) */
+/* { */
+/* head = FALSE; */
+/* } */
+/* else */
+/* { */
+/* if (first) */
+/* { */
+/* st = constraint_unparse (current); */
+/* first = FALSE; */
+/* } */
+/* else */
+/* st = message ("%q, %q", st, constraint_unparse (current)); */
+/* } */
+/* } end_constraintList_elements; */
+
+/* return st; */
+/* } */
+
+// /*@only@*/ cstring
+/* constraintList_unparseToCurrent (constraintList s) */
+/* { */
+/* int i; */
+/* cstring st = cstring_undefined; */
+
+/* for (i = 0; i < s->current; i++) */
+/* { */
+/* constraint current = s->elements[i]; */
+
+/* if (i == 0) */
+/* st = constraint_unparse (current); */
+/* else */
+/* st = message ("%q, %q", st, constraint_unparse (current)); */
+/* } */
+
+/* return st; */
+/* } */
+
+///*@only@*/ cstring
+/* constraintList_unparseSecondToCurrent (constraintList s) */
+/* { */
+/* int i; */
+/* cstring st = cstring_undefined; */
+
+/* for (i = 1; i < s->current; i++) */
+/* { */
+/* constraint current = s->elements[i]; */
+
+/* if (i == 1) */
+/* { */
+/* st = constraint_unparse (current); */
+/* } */
+/* else */
+/* { */
+/* st = message ("%q, %q", st, constraint_unparse (current)); */
+/* } */
+/* } */
+
+/* return st; */
+/* } */
+
+void
+constraintList_free (constraintList s)
+{
+ int i;
+ for (i = 0; i < s->nelements; i++)
+ {
+ constraint_free (s->elements[i]);
+ }
+
+ sfree (s->elementsroot);
+ sfree (s);
+}
--- /dev/null
+/*
+** constraintList.c
+*/
+
+# include <ctype.h> /* for isdigit */
+# include "lclintMacros.nf"
+# include "basic.h"
+# include "cgrammar.h"
+# include "cgrammar_tokens.h"
+
+# include "exprChecks.h"
+# include "aliasChecks.h"
+# include "exprNodeSList.h"
+# include "exprData.i"
+
+/*@i33*/
+/*@-fcnuse*/
+
+/*@notnull@*/ constraintList constraintList_new () {
+constraintList ret;
+
+ret = dmalloc ( sizeof (*ret) );
+llassert ( ret != NULL);
+
+ret->numconstraints = 0;
+/*@i22@*/ret->constraints = dmalloc (INITIALCONSTRAINTLISTSIZE * sizeof (constraint) );
+ret->size = INITIALCONSTRAINTLISTSIZE;
+return ret;
+}
+
+void exprNode_printfileloc (exprNode e)
+{
+ DPRINTF ((" %q ", fileloc_unparse (exprNode_getfileloc (e) ) ) );
+}
+
+void constraintList_debugPrint ( char * s )
+{
+ DPRINTF((s) );
+}
+
+void constraintList_print (constraintList cl)
+{
+
+ int i;
+ if (constraintList_isUndefined (cl) )
+ {
+ constraintList_debugPrint("Constraint List undefined\n");
+ return;
+ }
+ for (i = 0; i < cl->numconstraints; i++)
+ {
+ constraint_print (cl->constraints[i]);
+ }
+
+}
+
+void constraintList_resolve (constraintList cl)
+{
+ int i;
+ if (constraintList_isUndefined (cl) )
+ {
+ constraintList_debugPrint("Constraint List empty \n");
+ return;
+ }
+ for (i = 0; i < cl->numconstraints; i++)
+ {
+ constraintList_debugPrint("Trying to resolve:\n");
+ constraint_print (cl->constraints[i]);
+ if ( constraint_resolve (cl->constraints[i] ) )
+ constraintList_debugPrint ("resolve sucessfully\n");
+ else
+ constraintList_debugPrint ("not resolved sucessfully\n");
+
+ }
+}
+constraintList constraintList_get (exprNode e1 )
+{
+ return e1->constraints;
+}
+
+constraintList constraintList_exprNodemerge (exprNode e1, exprNode e2)
+{
+ constraintList ret;
+ if ( (e1 != NULL) && (e2 != NULL) )
+ {
+ ret = constraintList_merge (e1->constraints, e2->constraints);
+ }
+ 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;
+}
+
+
+constraintList constraintList_merge (constraintList cl1, constraintList cl2)
+{
+ constraintList ret;
+ int i;
+ ret = constraintList_undefined;
+ if (constraintList_isDefined (cl1) )
+ {
+ for (i = 0; i < cl1->numconstraints; i++)
+ {
+ ret = constraintList_add (ret, cl1->constraints[i]);
+ }
+ }
+ if (constraintList_isDefined (cl2) )
+ {
+ for (i = 0; i < cl2->numconstraints; i++)
+ {
+ ret = constraintList_add (ret, cl2->constraints[i]);
+ }
+ }
+ return ret;
+
+
+}
+
+constraintList constraintList_add (constraintList constraints, constraint newconstr)
+{
+ constraintList ret;
+
+ if ( constraintList_isUndefined(constraints) )
+ {
+ ret = constraintList_new ();
+ }
+ else
+ {
+ ret = constraints;
+ }
+
+ llassert (constraintList_isDefined (ret) );
+
+
+ ret->constraints[ret->numconstraints] = newconstr;
+
+ ret->numconstraints++;
+ if (ret->numconstraints == ret->size)
+ {
+ ret->constraints = realloc (ret->constraints, sizeof (constraint) * (ret->size*2) );
+ ret->size *= 2;
+ }
+ return ret;
+
+}
+/*@=fcnuse*/
--- /dev/null
+/*
+/*
+** constraintResolve.c
+*/
+
+# include <ctype.h> /* for isdigit */
+# include "lclintMacros.nf"
+# include "basic.h"
+# include "cgrammar.h"
+# include "cgrammar_tokens.h"
+
+# include "exprChecks.h"
+# include "aliasChecks.h"
+# include "exprNodeSList.h"
+# include "exprData.i"
+
+
+int constraintExpr_getValue (constraintExpr expr)
+{
+ if (expr->expr != NULL)
+ {
+ TPRINTF( ( "Not Implemented" ));
+ llassert(FALSE);
+ }
+ return (constraintTerm_getValue (expr->term) );
+}
+
+// returns 1 0 -1 like strcopy
+int constraintExpr_compare (constraintExpr expr1, constraintExpr expr2)
+{
+ int value1, value2;
+
+ value1 = constraintExpr_getValue(expr1);
+ value2 = constraintExpr_getValue(expr2);
+
+ if (value1 > value2)
+ return 1;
+
+ if (value1 == value2)
+ return 0;
+
+ else
+ return -1;
+}
+
+bool constraintExpr_canCompare (constraintExpr expr1, constraintExpr expr2)
+{
+ if (expr1->expr != NULL)
+ {
+ return FALSE;
+ }
+
+ if (expr2->expr != NULL)
+ {
+ return FALSE;
+ }
+
+ return TRUE;
+}
+
+bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2)
+
+{
+ switch (ar1)
+ {
+ case GTE:
+ case GT:
+ /*irst constraint is > only > => or == cosntraint can satify it */
+ if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
+ {
+ if (! constraintExpr_canCompare (expr1, expr2) )
+ return FALSE;
+
+ if (constraintExpr_compare (expr2, expr1) >= 0)
+ return TRUE;
+
+ }
+ return FALSE;
+ default:
+ TPRINTF(("case not handled"));
+ }
+ return FALSE;
+}
+
+/*returns true if cosntraint post satifies cosntriant pre */
+bool satifies (constraint pre, constraint post)
+{
+ if (!constraintTerm_same(pre->lexpr->term, post->lexpr->term) )
+ {
+ return FALSE;
+ }
+ if (post->expr->expr == NULL)
+ return FALSE;
+ return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
+
+ return TRUE;
+}
+
+constraintExpr constraintExpr_simplify (constraintExpr expr)
+{
+
+ expr->term = constraintTerm_simplify (expr->term);
+ if (expr->expr == NULL)
+ return expr;
+
+ expr->expr = constraintExpr_simplify (expr->expr);
+ if ( (expr->term->constrType == INTLITERAL) && (expr->expr->term->constrType == INTLITERAL) )
+ {
+ TPRINTF( ("EVENTUAL IMPLEMENTATION OF LITERAL MERGE " ));
+
+ TPRINTF ( (message ("Expression is %s ", constraintExpr_print (expr) ) ) );
+
+ if (expr->op == PLUS )
+ {
+ TPRINTF( (message ("Adding %d and %d ", expr->term->value.intlit,
+ expr->expr->term->value.intlit) ) );
+ expr->term->value.intlit += expr->expr->term->value.intlit;
+ }
+ else if (expr->op == MINUS )
+ {
+ expr->term->value.intlit -= expr->expr->term->value.intlit;
+ }
+ expr->op = expr->expr->op;
+
+ expr->expr = expr->expr->expr;
+ }
+ return expr;
+
+}
+
+constraintExpr constraintExpr_add (constraintExpr e, constraintTerm term, constraintExprOp op)
+{
+ constraintExpr p;
+
+ p = e;
+ while (p->expr != NULL)
+ {
+ p = p->expr;
+ }
+
+ p->op = op;
+ p->expr = constraintExpr_alloc();
+ p->expr->term = term;
+
+ return e;
+}
+
+constraintExpr termMove (constraintExpr dst, constraintExpr src)
+{
+ constraintTerm term;
+ llassert (src->expr != NULL);
+ term = src->expr->term;
+ if (src->op == PLUS)
+ dst = constraintExpr_add (dst, term, MINUS);
+ else
+ if (src->op == MINUS)
+ dst = constraintExpr_add (dst, term, PLUS);
+
+ return dst;
+}
+
+constraint solveforterm (constraint c)
+{
+ constraintExpr p;
+ p = c->lexpr;
+ while (p->expr != NULL)
+ {
+ TPRINTF( (message("Moving %s", constraintExpr_print (c->expr) ) ) );
+ c->expr = termMove(c->expr, p);
+ p->op = p->expr->op;
+ #warning memleak
+
+ p->expr = p->expr->expr;
+ }
+ return c;
+}
+
+constraint constraint_simplify (constraint c)
+{
+ c = solveforterm (c);
+ c->lexpr = constraintExpr_simplify (c->lexpr);
+ c->expr = constraintExpr_simplify (c->expr);
+ return c;
+}
+
+bool resolve (constraint c, constraintList p)
+{
+ constraintList_elements (p, el)
+ {
+ if ( satifies (c, el) )
+ {
+ TPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
+ return TRUE;
+ }
+ }
+ end_constraintList_elements;
+ TPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
+ return FALSE;
+}
+
+constraint substitute (constraint c, constraintList p)
+{
+ constraintList_elements (p, el)
+ {
+ if (constraintTerm_same(c->lexpr->term, el->lexpr->term) )
+ {
+ if ( el->ar == EQ)
+ {
+ c->lexpr = constraintExpr_copy (el->expr);
+ c = constraint_simplify(c);
+ return c;
+ }
+ }
+ }
+ end_constraintList_elements;
+
+ c = constraint_simplify(c);
+ return c;
+}
+
+
+constraintList reflectChanges (constraintList pre2, constraintList post1)
+{
+
+ constraintList ret;
+ constraint temp;
+ ret = constraintList_new();
+ constraintList_elements (pre2, el)
+ {
+ if (!resolve (el, post1) )
+ {
+ temp = substitute (el, post1);
+ ret = constraintList_add (ret, temp);
+ }
+ } end_constraintList_elements;
+
+ return ret;
+}
+
+
+/*check if rvalue side has term*/
+bool constraintExpr_hasTerm (constraint c, constraintTerm term)
+{
+ constraintExpr p;
+ p = c->expr;
+ while (p != NULL)
+ {
+ if (constraintTerm_same (p->term, term) )
+ return TRUE;
+
+ p = p->expr->expr;
+ }
+ TPRINTF((
+ message ("constraintExpr_hasTerm returned fallse for %s %S",
+ constraint_print(c), constraintTerm_print(term)
+ )
+ ));
+ return FALSE;
+}
+
+constraintExpr solveEq (constraint c, constraintTerm t)
+{
+ constraintExpr p;
+ c = constraint_copy (c);
+ TPRINTF(("\ndoing solveEq\n"));
+ if (! constraintTerm_same (c->expr->term, t) )
+ {
+ TPRINTF ( (message ("\n\nconstraintTerms: %s %s not same ", constraintTerm_print(c->expr->term),
+ constraintTerm_print(t) )
+ ) );
+ return NULL;
+ }
+
+ p = c->expr;
+ while (p->expr != NULL)
+ {
+ TPRINTF( (message("\n\nMoving %s", constraintExpr_print (c->expr) ) ) );
+ c->lexpr = termMove(c->lexpr, p);
+ p->expr = p->expr->expr;
+ }
+
+ return c->lexpr;
+
+}
+
+constraint updateConstraint (constraint c, constraintList p)
+{
+ TPRINTF(("start updateConstraints"));
+ constraintList_elements (p, el)
+ {
+
+ if (constraintTerm_same(c->lexpr->term, el->lexpr->term) )
+ {
+ TPRINTF((""));
+ if ( el->ar == EQ)
+ {
+ TPRINTF((""));
+
+ if (constraintExpr_hasTerm (el, c->lexpr->term) )
+ {
+ constraintExpr solve;
+ TPRINTF((""));
+ solve = solveEq (el, c->lexpr->term);
+ if (solve)
+ {
+ c->lexpr = constraintExpr_copy (solve);
+ c = constraint_simplify(c);
+ return c;
+ }
+ }
+ }
+ }
+ }
+ end_constraintList_elements;
+ c = constraint_simplify(c);
+
+ TPRINTF(("end updateConstraints"));
+ return c;
+}
+
+
+constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
+{
+ constraintList ret;
+ constraint temp;
+ ret = constraintList_new();
+ constraintList_elements (pre2, el)
+ {
+ if (!resolve (el, post1) )
+ {
+ temp = updateConstraint (el, post1);
+ if (temp != NULL)
+ ret = constraintList_add (ret, temp);
+ }
+ } end_constraintList_elements;
+
+ return ret;
+}
+
+void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
+{
+ constraintList temp;
+ TPRINTF( (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) );
+
+ TPRINTF( (message ("Child constraints are %s and %s ",
+ constraintList_print (child1->requiresConstraints),
+ constraintList_print (child2->requiresConstraints)
+ ) ) );
+
+ parent->requiresConstraints = constraintList_new();
+ parent->ensuresConstraints = constraintList_new();
+
+ parent->requiresConstraints = constraintList_copy (child1->requiresConstraints);
+
+ temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
+ parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp);
+
+
+ temp = reflectChangesEnsures (child1->ensuresConstraints, child2->ensuresConstraints);
+ // temp = constraintList_copy (child1->ensuresConstraints);
+
+
+ parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
+ parent->ensuresConstraints = constraintList_addList (parent->ensuresConstraints, temp);
+
+ TPRINTF( (message ("Parent constraints are %s and %s ",
+ constraintList_print (parent->requiresConstraints),
+ constraintList_print (parent->ensuresConstraints)
+ ) ) );
+
+}
+
--- /dev/null
+/*
+** constraintTerm.c
+*/
+
+# include <ctype.h> /* for isdigit */
+# include "lclintMacros.nf"
+# include "basic.h"
+# include "cgrammar.h"
+# include "cgrammar_tokens.h"
+
+# include "exprChecks.h"
+# include "aliasChecks.h"
+# include "exprNodeSList.h"
+# include "exprData.i"
+
+int constraintTerm_getValue (constraintTerm term)
+{
+ if (term->kind == EXPRNODE)
+ {
+ return (multiVal_forceInt (term->value.expr->val) );
+ }
+ if (term->kind == INTLITERAL )
+ {
+ return (term->value.intlit);
+ }
+ llassert(FALSE);
+ return 0;
+}
+
+/*@out@*/ static constraintTerm new_constraintTermExpr (void)
+{
+ constraintTerm ret;
+ ret = dmalloc (sizeof (* ret ) );
+ return ret;
+}
+
+constraintTerm constraintTerm_simplify (constraintTerm term)
+{
+ if (term->constrType == VALUE)
+ {
+ if (term->kind == EXPRNODE)
+ {
+ if ( exprNode_knownIntValue (term->value.expr ) )
+ {
+ int temp;
+ temp = exprNode_getLongValue (term->value.expr);
+ term->value.intlit = temp;
+ term->kind = INTLITERAL;
+ }
+
+ }
+
+ }
+ return term;
+}
+
+constraintTerm constraintTerm_copy (constraintTerm term)
+{
+ constraintTerm ret;
+ ret = new_constraintTermExpr();
+ ret->constrType = term->constrType;
+ ret->loc = fileloc_copy (term->loc);
+ ret->value= term->value;
+ ret->kind = term->kind;
+ return ret;
+}
+
+constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e)
+{
+ constraintTerm ret = new_constraintTermExpr();
+ ret->loc = exprNode_getfileloc(e);
+ ret->value.expr = e;
+ ret->kind = EXPRNODE;
+ return ret;
+}
+
+
+constraintTerm constraintTerm_makeMaxSetexpr (exprNode e)
+{
+ constraintTerm ret;
+ ret = exprNode_makeConstraintTerm (e);
+ ret->constrType = MAXSET;
+ return ret;
+}
+
+constraintTerm constraintTerm_makeMinSetexpr (exprNode e)
+{
+ constraintTerm ret;
+ ret = exprNode_makeConstraintTerm (e);
+ ret->constrType = MINSET;
+ return ret;
+}
+
+constraintTerm constraintTerm_makeMaxReadexpr (exprNode e)
+{
+ constraintTerm ret;
+ ret = exprNode_makeConstraintTerm (e);
+ ret->constrType = MAXREAD;
+ return ret;
+}
+
+constraintTerm constraintTerm_makeMinReadexpr (exprNode e)
+{
+ constraintTerm ret;
+ ret = exprNode_makeConstraintTerm (e);
+ ret->constrType = MINREAD;
+ return ret;
+}
+
+constraintTerm constraintTerm_makeValueexpr (exprNode e)
+{
+ constraintTerm ret;
+ ret = exprNode_makeConstraintTerm (e);
+ ret->constrType = VALUE;
+ ret = constraintTerm_simplify (ret);
+ return ret;
+}
+
+
+constraintTerm intLit_makeConstraintTerm (int i)
+{
+ constraintTerm ret = new_constraintTermExpr();
+ ret->value.intlit = i;
+ ret->kind = INTLITERAL;
+ ret->loc = fileloc_undefined;
+ return ret;
+}
+
+
+constraintTerm constraintTerm_makeIntLitValue (int i)
+{
+ constraintTerm ret;
+ ret = intLit_makeConstraintTerm (i);
+ ret->constrType = VALUE;
+ return ret;
+
+}
+
+/* constraintTerm constraintTerm_makeMinSetexpr (int i) */
+/* { */
+/* constraintTerm ret; */
+/* ret = intLit_makeConstraintTerm (i); */
+/* ret->constrType = MINSET; */
+/* } */
+
+/* constraintTerm constraintTerm_makeMaxReadexpr (int i) */
+/* { */
+/* constraintTerm ret; */
+/* ret = intLit_makeConstraintTerm (i); */
+/* ret->constrType = MAXREAD; */
+/* } */
+/* constraintTerm constraintTerm_makeMinReadexpr (int i) */
+/* { */
+/* constraintTerm ret; */
+/* ret = exprNode_makeConstraintTerm (i); */
+/* ret->constrType = MINREAD; */
+/* } */
+
+
+
+
+cstring constraintType_print (constraintType constrType)
+{
+ cstring st = cstring_undefined;
+
+ switch (constrType)
+ {
+ case VALUE:
+ st = cstring_makeLiteral("VALUE");
+ break;
+ case CALLSAFE:
+ st = cstring_makeLiteral("CALLSAFE");
+ break;
+ case MAXSET:
+ st = cstring_makeLiteral ("MAXSET");
+ break;
+ case MINSET:
+ st = cstring_makeLiteral ("MINSET");
+ break;
+ case MAXREAD:
+ st = cstring_makeLiteral ("MAXREAD");
+ break;
+ case MINREAD:
+ st = cstring_makeLiteral ("MINREAD");
+ break;
+ case NULLTERMINATED:
+ st = cstring_makeLiteral ("NULLTERMINATED");
+ break;
+ case UNDEFINED:
+ st = cstring_makeLiteral (("Unhandled value for constraintType"));
+ llassert(FALSE);
+ break;
+ default:
+ st = cstring_makeLiteral (("Unhandled value for constraintType"));
+ llassert(FALSE);
+ }
+ return st;
+}
+cstring constraintTerm_print (constraintTerm term)
+{
+ cstring s;
+ s = cstring_undefined;
+
+ llassert (term != NULL);
+
+ switch (term->kind)
+ {
+ case EXPRNODE:
+ /*@i334*/ //wtf
+ s = message ("%s @ %s ", exprNode_unparse (term->value.expr),
+ fileloc_unparse (term->loc) );
+ break;
+ case INTLITERAL:
+ {
+ s = message (" %d ", term->value.intlit);
+ break;
+ }
+ case SREF:
+ s = cstring_makeLiteral("Not Implemented\n");
+ llassert(FALSE);
+ break;
+ }
+ s = message (" %s %s ", constraintType_print (term->constrType), s);
+ return s;
+
+}
+
+
+
+bool constraintTerm_same (constraintTerm term1, constraintTerm term2)
+{
+ llassert (term1 !=NULL && term2 !=NULL);
+
+ if (term1->constrType != term2->constrType)
+ {
+ return FALSE;
+ }
+ if ( (term1->kind != term2->kind) || (term1->kind != EXPRNODE) )
+ {
+ return FALSE;
+ }
+
+ DPRINTF ( (message
+ ("Comparing srefs for %s and %s ", constraintTerm_print(term1), constraintTerm_print(term2)
+ )
+ )
+ );
+
+ if (sRef_same (term1->value.expr->sref, term2->value.expr->sref) )
+ {
+ TPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
+ return TRUE;
+ }
+ else
+ {
+ TPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2) ) ));
+ return FALSE;
+ }
+
+}
+
e->mustBreak = FALSE;
e->isJumpPoint = FALSE;
e->environment = environmentTable_undefined;
- e->constraints = constraintList_undefined;
+ e->requiresConstraints = constraintList_new();
+ e->ensuresConstraints = constraintList_new();
+
return (e);
}
if (exprNode_isDefined (e) && e->kind == XPR_STMT) {
lltok t = exprData_getUopTok (e->edata);
- printf ("!!!!!!!!!!!!!!!!!!Tok is \n\n%s\n", lltok_unparse(t) );
return lltok_getLoc (t);
} else {
llcontbug (message ("Cannot get next sequence point: %s", exprNode_unparse (e)));
andersk / splint.git / commitdiff
