** constraintExpr.c
*/
-//#define DEBUGPRINT 1
+/* #define DEBUGPRINT 1 */
# include "lclintMacros.nf"
# include "basic.h"
# include "exprChecks.h"
# include "exprNodeSList.h"
-//# include "constraintExpr.h"
-
-
/*@-czechfcns@*/
static /*@only@*/ constraintExpr
doFixResultTerm (/*@only@*/ constraintExpr p_e, /*@exposed@*/ exprNode p_fcnCall)
/*@modifies p_e@*/;
-
-
- /*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void) ; /// @allocates result->data @ @sets result->kind @;
-
-//constraintExpr constraintExpr_makeMaxSetConstraintExpr (constraintExpr c);
+
+
+/*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
+ /* @allocates result->data @ @sets result->kind @ */ ;
void constraintExpr_free (/*@only@*/ constraintExpr expr)
{
tempOp = constraintExprData_binaryExprGetOp (expr2->data);
- if (op == PLUS)
+ if (op == BINARYOP_PLUS)
op = tempOp;
- else if (op == MINUS)
+ else if (op == BINARYOP_MINUS)
{
- if (tempOp == PLUS)
- op = MINUS;
- else if (tempOp == MINUS)
- op = PLUS;
+ if (tempOp == BINARYOP_PLUS)
+ op = BINARYOP_MINUS;
+ else if (tempOp == BINARYOP_MINUS)
+ op = BINARYOP_PLUS;
else
BADEXIT;
}
else
BADEXIT;
- /*@i834@*/ constraintExpr_free(expr2);
-
expr->data = constraintExprData_binaryExprSetExpr2(expr->data, temp);
expr->data = constraintExprData_binaryExprSetOp(expr->data, op);
*propagate = FALSE;
*literal = 0;
+
llassert (expr != NULL);
- // we simplify unaryExpr else where
+ /* we simplify unaryExpr elsewhere */
if (expr->kind != binaryexpr)
return expr;
expr1 = constraintExpr_propagateConstants (expr1, &propagate1, &literal1);
expr2 = constraintExpr_propagateConstants (expr2, &propagate2, &literal2);
+ expr1 = removeZero(expr1);
+ expr2 = removeZero(expr2);
+
+
*propagate = propagate1 || propagate2;
- if (op == PLUS)
+ if (op == BINARYOP_PLUS)
*literal = literal1 + literal2;
- else if (op == MINUS)
+ else if (op == BINARYOP_MINUS)
*literal = literal1 - literal2;
else
BADEXIT;
constraintExpr_free (expr1);
constraintExpr_free (expr2);
- if (op == PLUS )
+ if (op == BINARYOP_PLUS )
return (constraintExpr_makeIntLiteral ( (t1+t2) ));
- else if (op == MINUS)
+ else if (op == BINARYOP_MINUS)
return (constraintExpr_makeIntLiteral ( (t1-t2) ));
else
BADEXIT;
*literal += constraintExpr_getValue (expr1);
- if (op == PLUS)
+ if (op == BINARYOP_PLUS)
{
constraintExpr_free(expr1);
constraintExpr_free(expr);
return expr2;
}
- else if (op == MINUS)
+ else if (op == BINARYOP_MINUS)
{
+
constraintExpr temp;
/* this is an ugly kludge to deal with not
having a unary minus operation...*/
-
+
temp = constraintExpr_makeIntLiteral (0);
temp = constraintExpr_makeSubtractExpr (temp, expr2);
{
*propagate = TRUE;
- if ( op == PLUS )
+ if ( op == BINARYOP_PLUS )
*literal += constraintExpr_getValue (expr2);
- else if (op == MINUS)
+ else if (op == BINARYOP_MINUS)
*literal -= constraintExpr_getValue (expr2);
else
BADEXIT;
ce2 = constraintExpr_makeExprNode (t2);
ret = constraintExpr_parseMakeBinaryOp (ce1, tok, ce2);
}
- else
+ /*
+ drl 8-11-001
+
+ We handle expressions containing sizeof with the rule
+ (sizeof type ) * Expr = Expr
+
+ This is the total wronge way to do this but...
+ it may be better than nothing
+ */
+ else if (lltok_isMult(tok) )
{
- ret = oldconstraintExpr_makeTermExprNode (e);
+ if ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
+ {
+ ret = constraintExpr_makeExprNode(t2);
+ }
+ else if ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
+ {
+ ret = constraintExpr_makeExprNode(t1);
+ }
+ else
+ {
+ ret = oldconstraintExpr_makeTermExprNode (e);
+ }
}
+ else
+ ret = oldconstraintExpr_makeTermExprNode (e);
+
break;
case XPR_PARENS:
t = exprData_getUopNode (data);
return ret;
}
-/*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode e)
+/*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode e)
{
- return oldconstraintExpr_makeTermExprNode(e); //constraintExpr_makeExprNode (e);
+ return oldconstraintExpr_makeTermExprNode(e);
}
static constraintExpr constraintExpr_makeTerm (/*@only@*/ constraintTerm t)
ret = constraintExpr_alloc();
ret->kind = term;
ret->data = dmalloc (sizeof *(ret->data) );
+ ret->data->term = NULL;
ret->data = constraintExprData_termSetTerm (ret->data, t);
return ret;
ret = constraintExpr_alloc();
ret->kind = unaryExpr;
ret->data = dmalloc ( sizeof *(ret->data) );
+ ret->data->unaryOp.expr = constraintExpr_undefined;
return ret;
}
/*@-uniondef@*/
/*@-compdef@*/
- ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
- ret->data = constraintExprData_unaryExprSetOp (ret->data, UNARYOP_UNDEFINED);
-
+ ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
+ ret->data = constraintExprData_unaryExprSetOp (ret->data, UNARYOP_UNDEFINED);
+
return ret;
-
+
/*@=compdef@*/
/*@=uniondef@*/
}
return ret;
}
+# if 0
/*@only@*/
/*@unused@*/ static constraintExpr constraintExpr_makeMinSetExpr (/*@exposed@*/ exprNode expr)
{
ret->data = constraintExprData_unaryExprSetOp (ret->data, MINREAD);
return ret;
}
-
+# endif
/*@only@*/
constraintExpr constraintExpr_makeValueExpr (/*@exposed@*/ exprNode expr)
ret = constraintExpr_alloc();
ret->kind = binaryexpr;
ret->data = dmalloc ( sizeof *(ret->data) );
- // ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_UNDEFINED);
+
+ ret->data->binaryOp.expr1 = constraintExpr_undefined;
+ ret->data->binaryOp.expr2 = constraintExpr_undefined;
+
return ret;
}
constraintExpr ret;
ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
if (op.tok == TPLUS)
- ret->data = constraintExprData_binaryExprSetOp(ret->data, PLUS);
+ ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
else if (op.tok == TMINUS)
- ret->data = constraintExprData_binaryExprSetOp(ret->data, MINUS);
+ ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
else
{
llassert(FALSE);
return ret;
}
+# if 0
/*@only@*/
/*@unused@*/ static constraintExpr constraintExpr_makeBinaryOpExprNode (/*@exposed@*/ exprNode expr1, /*@exposed@*/ exprNode expr2)
{
ret = constraintExpr_makeBinaryOpConstraintExpr(sub1, sub2);
return ret;
}
+# endif
static /*@only@*/
constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/ constraintExpr expr, int literal)
constExpr = constraintExpr_makeIntLiteral (literal);
ret = constraintExpr_makeBinaryOpConstraintExpr (expr, constExpr);
- ret->data = constraintExprData_binaryExprSetOp(ret->data, PLUS);
+ ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
return ret;
}
inc = constraintExpr_makeIntLiteral (1);
ret = constraintExpr_makeBinaryOpConstraintExpr (expr, inc);
- ret->data = constraintExprData_binaryExprSetOp(ret->data, MINUS);
+ ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
return ret;
}
DPRINTF ( (message ("Making subtract expression") ) );
ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
- ret->data = constraintExprData_binaryExprSetOp (ret->data, MINUS);
+ ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_MINUS);
return ret;
}
DPRINTF ( (message ("Doing addTerm simplification") ) );
ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
- ret->data = constraintExprData_binaryExprSetOp (ret->data, PLUS);
+ ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_PLUS);
return ret;
}
inc = constraintExpr_makeIntLiteral (1);
ret = constraintExpr_makeBinaryOpConstraintExpr (expr, inc);
- ret->data = constraintExprData_binaryExprSetOp(ret->data, PLUS);
+ ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
return ret;
}
switch (op)
{
- case PLUS:
+ case BINARYOP_PLUS:
return message("+");
- case MINUS:
+ case BINARYOP_MINUS:
return message("-");
default:
else
{
op = constraintExprData_binaryExprGetOp (c->data);
- if (op == MINUS)
+ if (op == BINARYOP_MINUS)
if (constraintExpr_similar(e1, e2) )
{
constraintExpr_free(c);
expr1 = constraintExpr_copy(expr1);
expr2 = constraintExpr_copy(expr2);
-//drl possible problem : warning make sure this works
-
- lexpr->kind = expr1->kind;
- free (lexpr->data);
-
- lexpr->data = copyExprData (expr1->data, expr1->kind);
- constraintExpr_free(expr1);
-
- if (op == PLUS)
- expr = constraintExpr_makeSubtractExpr (expr, expr2);
- else if (op == MINUS)
- expr = constraintExpr_makeAddExpr (expr, expr2);
- else
- BADEXIT;
-
-
- return expr;
+ /* drl possible problem : warning make sure this works */
+
+ lexpr->kind = expr1->kind;
+ sfree (lexpr->data);
+
+ lexpr->data = copyExprData (expr1->data, expr1->kind);
+ constraintExpr_free(expr1);
+
+ if (op == BINARYOP_PLUS)
+ expr = constraintExpr_makeSubtractExpr (expr, expr2);
+ else if (op == BINARYOP_MINUS)
+ expr = constraintExpr_makeAddExpr (expr, expr2);
+ else
+ BADEXIT;
+
+
+ return expr;
/*
#warning this needs to be checked
{
return c;
}
- // pattern mxr ( var + const) = mxr(var) - const
exp = constraintExprData_unaryExprGetExpr (c->data);
-
+ exp = constraintExpr_copy(exp);
+
if (exp->kind == term)
{
constraintTerm cterm;
temp = constraintExpr_makeIntLiteral ((int)strlen (cstring_toCharsSafe(val) ) );
cstring_free(val);
constraintExpr_free(c);
+ constraintExpr_free(exp);
+
return temp;
+
}
if (constraintExprData_unaryExprGetOp (c->data) == MAXREAD)
{
temp = constraintExpr_makeIntLiteral ((int)strlen (cstring_toCharsSafe(val) ) );
cstring_free(val);
constraintExpr_free(c);
+ constraintExpr_free(exp);
+
return temp;
}
BADEXIT;
}
- // slight Kludge to hanlde var [] = { , , };
- // type syntax I don't think this is sounds but it should be good
- // enough. The C stanrad is very confusing about initialization
- // -- DRL 7/25/01
+ /* slight Kludge to hanlde var [] = { , , };
+ ** type syntax I don't think this is sounds but it should be good
+ ** enough. The C stanrad is very confusing about initialization
+ ** -- DRL 7/25/01
+ */
if (constraintTerm_isInitBlock(cterm) )
{
constraintExpr_free(c);
DPRINTF(( message("Changed too %q", constraintExpr_print(temp)
) ));
+ constraintExpr_free(exp);
return temp;
}
+ constraintExpr_free(exp);
return c;
}
if (exp->kind != binaryexpr)
- return c;
-
- if (constraintExprData_binaryExprGetOp (exp->data) == PLUS )
+ {
+ constraintExpr_free(exp);
+ return c;
+ }
+
+ if (constraintExprData_binaryExprGetOp (exp->data) == BINARYOP_PLUS )
{
- // if (constraintExpr_canGetValue (constraintExprData_binaryExprGetExpr2 (exp->data) ) )
+ /* if (constraintExpr_canGetValue (constraintExprData_binaryExprGetExpr2 (exp->data) ) ) */
{
constraintExpr temp, temp2;
}
}
- DPRINTF ( (message ("Done simplification:%s", constraintExpr_unparse (c) ) ) );
+ DPRINTF ( (message ("constraintExpr_simplifyUnaryExpr: Done simplification:%s", constraintExpr_unparse (c) ) ) );
+
+ constraintExpr_free(exp);
return c;
}
switch (kind)
{
case term:
- st = message ("(%q) ", constraintTerm_print (constraintExprData_termGetTerm (ex->data)));
+
+ if (context_getFlag (FLG_PARENCONSTRAINT) )
+ {
+ st = message ("(%q) ", constraintTerm_print (constraintExprData_termGetTerm (ex->data)));
+ }
+ else
+ {
+ st = message ("%q", constraintTerm_print (constraintExprData_termGetTerm (ex->data)));
+ }
break;
case unaryExpr:
- st = message ("%q (%q)",
- constraintExprUnaryOpKind_print (constraintExprData_unaryExprGetOp (ex->data)
- ),
+ st = message ("%q(%q)",
+ constraintExprUnaryOpKind_print (constraintExprData_unaryExprGetOp (ex->data) ),
constraintExpr_unparse (constraintExprData_unaryExprGetExpr (ex->data) )
);
break;
case binaryexpr:
- st = message ("(%q) %q (%q)",
+ if (context_getFlag (FLG_PARENCONSTRAINT) )
+ {
+ st = message ("(%q) %q (%q)",
constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)
),
constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
);
+ }
+ else
+ {
+ st = message ("%q %q %q",
+ constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data) ),
+ constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)
+ ),
+ constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data) )
+ );
+ }
+
break;
default:
llassert(FALSE);
constraintTerm t;
sRef s;
/*maybe this should move to cosntraintExpr.c -drl7x 5/18/01*/
- /*@i22*/ constraintExprData data = e->data;
-
- /*@i22*/constraintExprKind kind = e->kind;
+ /*@i22*/
+
+ constraintExprData data = e->data;
+ constraintExprKind kind = e->kind;
constraintExpr ret;
return FALSE;
}
+/*drl added 8/08/001 */
+bool constraintExpr_isTerm (/*@observer@*/ constraintExpr c) /*@*/
+{
+ if (c->kind == term)
+ return TRUE;
+
+ else
+ return FALSE;
+}
+
+/*@observer@*/ /*@temp@*/ constraintTerm constraintExpr_getTerm ( /*@temp@*/ /*@observer@*/ constraintExpr c) /*@*/
+{
+ constraintTerm term;
+
+ llassert(constraintExpr_isTerm(c) );
+
+ term = constraintExprData_termGetTerm(c->data);
+
+ return term;
+}
+
static void binaryExpr_dump (/*@observer@*/ constraintExprData data, FILE *f)
{
constraintExpr expr1;
return ret;
}
+
+int constraintExpr_getDepth (constraintExpr ex)
+{
+ int ret;
+
+ constraintExprKind kind;
+
+ llassert (ex != NULL);
+
+ kind = ex->kind;
+
+ switch (kind)
+ {
+ case term:
+ ret = 1;
+ break;
+ case unaryExpr:
+ ret = constraintExpr_getDepth (constraintExprData_unaryExprGetExpr (ex->data) );
+ ret++;
+
+ break;
+ case binaryexpr:
+ ret = 0;
+ ret = constraintExpr_getDepth (constraintExprData_binaryExprGetExpr1 (ex->data) );
+
+ ret++;
+
+ ret += constraintExpr_getDepth (constraintExprData_binaryExprGetExpr2 (ex->data) );
+
+ break;
+ default:
+ BADEXIT;
+ }
+
+ return ret;
+}
+
+
+
andersk / splint.git / blobdiff