+/*
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2003 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
+*/
+
/*
** constraintExpr.c
*/
-//#define DEBUGPRINT 1
+/* #define DEBUGPRINT 1 */
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
# include "basic.h"
# include "cgrammar.h"
# include "cgrammar_tokens.h"
# include "exprChecks.h"
# include "exprNodeSList.h"
-//# include "constraintExpr.h"
-
-
-/*@-czechfcns@*/
-
-
-
-/*@access exprNode constraintExpr@*/
+static ctype constraintExpr_getOrigType (constraintExpr p_e);
+static bool constraintExpr_hasTypeChange(constraintExpr p_e) /*@*/;
static /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/constraintExpr p_expr, int p_literal);
+/*@only@*/ static constraintExpr
+doSRefFixInvarConstraintTerm (/*@only@*/ constraintExpr p_e,
+ sRef p_s, ctype p_ct);
+
/*@only@*/ static constraintExpr
doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr p_e, /*@temp@*/ /*@observer@*/ exprNodeList p_arglist) /*@modifies p_e@*/;
doFixResultTerm (/*@only@*/ constraintExpr p_e, /*@exposed@*/ exprNode p_fcnCall)
/*@modifies p_e@*/;
+static bool constraintExpr_canGetCType (constraintExpr p_e) /*@*/;
+
+static ctype constraintExpr_getCType (constraintExpr p_e);
- /*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void) ; /// @allocates result->data @ @sets result->kind @;
+static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr p_e, ctype p_ct);
-//constraintExpr constraintExpr_makeMaxSetConstraintExpr (constraintExpr c);
+/*@special@*/ /*@notnull@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
+ /* @allocates result->data @ @sets result->kind @ */ ;
void constraintExpr_free (/*@only@*/ constraintExpr expr)
{
{
constraintExpr e2;
+ llassert (expr != NULL); /* evans 2001-07-18 */
+
if (!constraintExpr_isBinaryExpr (expr) )
{
return FALSE;
e2 = constraintExprData_binaryExprGetExpr2(expr->data);
+ llassert (e2 != NULL); /* evans 2001-07-18 */
+
if (constraintExpr_isBinaryExpr (e2) )
{
constraintExpr e1;
/* change expr + (o - expr) to (expr -expr) */
-/*@only@*/ static constraintExpr removeZero (/*@only@*/ /*@returned@*/ constraintExpr expr)
+/*@only@*/ /*@notnull@*/ static constraintExpr removeZero (/*@only@*/ /*@returned@*/ constraintExpr expr)
{
constraintExpr expr1, expr2;
constraintExprBinaryOpKind tempOp;
+ llassert (expr != NULL); /* evans 2001-07-18 */
+
if (!isZeroBinaryOp(expr) )
return expr;
expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
op = constraintExprData_binaryExprGetOp(expr->data);
- llassert( constraintExpr_isBinaryExpr(expr2) );
-
+ llassert( constraintExpr_isBinaryExpr(expr2) );
+
temp = constraintExprData_binaryExprGetExpr2 (expr2->data);
temp = constraintExpr_copy (temp);
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;
- constraintExpr_free(expr2);
-
-
-
expr->data = constraintExprData_binaryExprSetExpr2(expr->data, temp);
expr->data = constraintExprData_binaryExprSetOp(expr->data, op);
}
-/*@only@*/ constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
+/*@only@*//*@notnull@*/ constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
/*@out@*/ bool * propagate,
/*@out@*/ int *literal)
{
*propagate = FALSE;
*literal = 0;
+
llassert (expr != NULL);
- // we simplify unaryExpr else where
+ /* we simplify unaryExpr elsewhere */
if (expr->kind != binaryexpr)
return expr;
op = constraintExprData_binaryExprGetOp (expr->data);
- DPRINTF( (message("constraintExpr_propagateConstants: binaryexpr: %s", constraintExpr_unparse(expr) ) ) );
+ DPRINTF((message("constraintExpr_propagateConstants: binaryexpr: %s", constraintExpr_unparse(expr) ) ) );
expr = removeZero(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;
if ( constraintExpr_isLit (expr1) && constraintExpr_isLit (expr2) )
{
- int t1, t2;
+ long t1, t2;
t1 = constraintExpr_getValue (expr1);
t2 = constraintExpr_getValue (expr2);
llassert(*propagate == FALSE);
constraintExpr_free (expr1);
constraintExpr_free (expr2);
- if (op == PLUS )
- return (constraintExpr_makeIntLiteral ( (t1+t2) ));
- else if (op == MINUS)
- return (constraintExpr_makeIntLiteral ( (t1-t2) ));
+ if (op == BINARYOP_PLUS )
+ return (constraintExpr_makeIntLiteral ((t1+t2) ));
+ 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);
constraintExpr_free(expr1);
constraintExpr_free(expr);
-
+
+ llassert (constraintExpr_isDefined(temp) );
return temp;
}
+ else
+ {
+ BADBRANCH; /* evans 2001-07-18 */
+ }
}
if (constraintExpr_isLit (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;
return expr1;
}
- DPRINTF( (message("constraintExpr_propagateConstants returning: %s", constraintExpr_unparse(expr) ) ) );
+ DPRINTF((message("constraintExpr_propagateConstants returning: %s", constraintExpr_unparse(expr) ) ) );
expr->data = constraintExprData_binaryExprSetExpr1 (expr->data, expr1);
expr->data = constraintExprData_binaryExprSetExpr2 (expr->data, expr2);
return expr;
}
-/*@only@*/ static constraintExpr constraintExpr_combineConstants (/*@only@*/ constraintExpr expr ) /*@modifies expr@*/
+/*@notnull@*/ /*@only@*/ static constraintExpr constraintExpr_combineConstants (/*@only@*/ constraintExpr expr ) /*@modifies expr@*/
{
bool propagate;
int literal;
- DPRINTF ( (message ("Before combine %s", constraintExpr_unparse(expr) ) ) );
+ DPRINTF ((message ("Before combine %s", constraintExpr_unparse(expr) ) ) );
expr = constraintExpr_propagateConstants (expr, &propagate, &literal);
expr = ret;
}
}
- DPRINTF ( (message ("After combine %s", constraintExpr_unparse(expr) ) ) );
- return expr;
+ DPRINTF ((message ("After combine %s", constraintExpr_unparse(expr) ) ) );
+
+ llassert(constraintExpr_isDefined(expr) );
+ return expr;
}
/*@special@*/
-static constraintExpr constraintExpr_alloc (void) /*@post:isnull result->data@*/
+static /*@notnull@*/ constraintExpr constraintExpr_alloc (void) /*@post:isnull result->data@*/
{
constraintExpr ret;
ret = dmalloc (sizeof (*ret) );
ret->kind = term;
ret->data = NULL;
+ ret->ct = FALSE;
+ ret->origType = ctype_undefined;
return ret;
}
constraintExpr constraintExpr_copy (constraintExpr expr)
{
constraintExpr ret;
- ret = constraintExpr_alloc();
+ ret = constraintExpr_alloc ();
+
+
+ /*drl 03/02/2003 this shouldn't be used to copy a null
+ expression but handle things cleanly if it is*/
+ llassert (!constraintExpr_isUndefined(expr) );
+
+ if (constraintExpr_isUndefined(expr) )
+ {
+ return constraintExpr_undefined;
+ }
+
ret->kind = expr->kind;
ret->data = copyExprData (expr->data, expr->kind);
+ ret->ct = expr->ct;
+ ret->origType = expr->origType;
return ret;
}
ret->data = dmalloc (sizeof *(ret->data) );
t = constraintTerm_makeExprNode (e);
ret->data = constraintExprData_termSetTerm (ret->data, t);
+ ret->ct = FALSE;
+ ret->origType = ctype_undefined;
+
return ret;
}
+/*@access exprNode@*/
constraintExpr constraintExpr_makeExprNode (exprNode e)
{
sRef s;
exprNode t, t1, t2;
lltok tok;
-
llassert (e != NULL);
data = e->edata;
{
case XPR_SIZEOF:
t = exprData_getSingle (data);
+ while (exprNode_isInParens (t) )
+ {
+ t = exprData_getUopNode (t->edata);
+ }
s = exprNode_getSref (t);
if (sRef_isFixedArray(s) )
{
size = (int) sRef_getArraySize(s);
ret = constraintExpr_makeIntLiteral (size);
}
+ else if (exprNode_isStringLiteral (t))
+ {
+ cstring str = multiVal_forceString (exprNode_getValue(t));
+ ret = constraintExpr_makeIntLiteral (size_toLong (cstring_length (str) + 1));
+ }
else
{
DPRINTF ((message ("could not determine the size of %s", exprNode_unparse (e) ) ) );
ce2 = constraintExpr_makeExprNode (t2);
ret = constraintExpr_parseMakeBinaryOp (ce1, tok, ce2);
}
- else
+
+
+ /*@i333*/
+ /* uncomment this block to activate the cheesy heuristic
+ for handling sizeof expressions
+
+ / *
+ 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);
case XPR_PREOP:
t = exprData_getUopNode (data);
tok = exprData_getUopTok (data);
- if (lltok_isInc_Op (tok) )
+ if (lltok_isIncOp (tok))
{
constraintExpr temp;
temp = constraintExpr_makeExprNode(t);
ret = constraintExpr_makeIncConstraintExpr(temp);
}
- else if (lltok_isDec_Op (tok) )
+ else if (lltok_isDecOp (tok))
{
constraintExpr temp;
temp = constraintExpr_makeExprNode(t);
case XPR_COMMA:
t = exprData_getPairA(data);
ret = constraintExpr_makeExprNode(t);
- /*@i3434*/ /*I'm not sure if this is right. I'm adding a break to quite LCLint*/
+ /*@i3434*/ /* drl: I'm not sure if this is right. I'm adding a break to quiet Splint */
break;
default:
ret = oldconstraintExpr_makeTermExprNode (e);
return ret;
}
+/*@noaccess exprNode@*/
+
+
-/*@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);
+ ret->ct = FALSE;
+ ret->origType = ctype_undefined;
return ret;
}
ret->data = dmalloc (sizeof *(ret->data) );
t = constraintTerm_makesRef (s);
ret->data = constraintExprData_termSetTerm (ret->data, t);
+
+ ret->ct = FALSE;
+ ret->origType = ctype_undefined;
+
return ret;
}
-/*@special@*/ static constraintExpr makeUnaryOpGeneric (void) /*@allocates result->data@*/ /*@defines result->kind@*/
+/*@special@*/ /*@notnull@*/ static constraintExpr makeUnaryOpGeneric (void) /*@allocates result->data@*/ /*@defines result->kind@*/
{
constraintExpr ret;
ret = constraintExpr_alloc();
ret->kind = unaryExpr;
ret->data = dmalloc ( sizeof *(ret->data) );
+ ret->data->unaryOp.expr = constraintExpr_undefined;
return ret;
}
-/*@only@*/ static constraintExpr constraintExpr_makeUnaryOpConstraintExpr (/*@only@*/ constraintExpr cexpr)
+/*@notnull@*/ /*@only@*/ static constraintExpr constraintExpr_makeUnaryOpConstraintExpr (/*@only@*/ constraintExpr cexpr)
{
constraintExpr ret;
ret = makeUnaryOpGeneric();
/*@-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@*/
}
-/*@only@*/ static constraintExpr constraintExpr_makeUnaryOp (/*@only@*/ constraintExpr cexpr, constraintExprUnaryOpKind Op )
+/*@only@*/ /*@notnull@*/static constraintExpr constraintExpr_makeUnaryOp (/*@only@*/ constraintExpr cexpr, constraintExprUnaryOpKind Op )
{
constraintExpr ret;
ret = makeUnaryOpGeneric();
ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
ret->data = constraintExprData_unaryExprSetOp (ret->data, Op);
- return ret;
-}
+ ret->ct = FALSE;
+ ret->origType = ctype_undefined;
-/*@only@*/
-static constraintExpr constraintExpr_makeMaxSetConstraintExpr (/*@only@*/ constraintExpr c)
-{
- constraintExpr ret;
- ret = constraintExpr_makeUnaryOp (c, MAXSET);
return ret;
}
-/*@only@*/
+/*@only@*/ /*@notnull@*/
static constraintExpr constraintExpr_makeUnaryOpExprNode (/*@exposed@*/ exprNode expr)
{
constraintExpr ret;
return ret;
}
+/*@only@*/ /*@notnull@*/
+static constraintExpr constraintExpr_makeMaxSetConstraintExpr (/*@only@*/ constraintExpr c)
+{
+ constraintExpr ret;
+ ret = constraintExpr_makeUnaryOp (c, MAXSET);
+ return ret;
+}
-/*@only@*/
+/*@only@*/ /*@notnull@*/
static constraintExpr constraintExpr_makeSRefUnaryOp (/*@temp@*/ /*@observer@*/ sRef s, constraintExprUnaryOpKind op)
{
constraintExpr ret;
constraintExpr ret;
ret = constraintExpr_makeUnaryOpConstraintExpr ( cexpr);
- switch (op.tok)
+ switch (lltok_getTok (op))
{
case QMAXSET:
ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXSET);
ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXREAD);
break;
default:
- llfatalbug(message("Unhandled Operation in Constraint") );
+ llfatalbug (message ("Unhandled operation in constraint: %s", lltok_unparse (op)));
}
return ret;
}
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)
return ret;
}
-/*@only@*/
-constraintExpr constraintExpr_makeIntLiteral (int i)
+/*@only@*/ /*@notnull@*/
+constraintExpr constraintExpr_makeIntLiteral (long i)
{
constraintExpr ret;
constraintTerm t;
ret->data = dmalloc (sizeof *(ret->data) );
t = constraintTerm_makeIntLiteral (i);
ret->data = constraintExprData_termSetTerm (ret->data, t);
+
+ ret->ct = FALSE;
+ ret->origType = ctype_undefined;
+
return ret;
}
}
*/
-/*@only@*/
+/*@only@*/ /*@notnull@*/
/*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
/*@allocates result->data @*/ /*@sets result->kind @*/
{
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;
}
-static /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExpr (/*@only@*/constraintExpr expr1, /*@only@*/ constraintExpr expr2)
+static /*@notnull@*/ /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExpr (/*@only@*/constraintExpr expr1, /*@only@*/ constraintExpr expr2)
{
constraintExpr ret;
ret->data = constraintExprData_binaryExprSetExpr1 (ret->data, expr1);
ret->data = constraintExprData_binaryExprSetExpr2 (ret->data, expr2);
ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_UNDEFINED);
+
+ ret->ct = FALSE;
+ ret->origType = ctype_undefined;
+
return ret;
}
{
constraintExpr ret;
ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
- if (op.tok == TPLUS)
- ret->data = constraintExprData_binaryExprSetOp(ret->data, PLUS);
- else if (op.tok == TMINUS)
- ret->data = constraintExprData_binaryExprSetOp(ret->data, MINUS);
- else
- {
- llassert(FALSE);
- }
+
+ if (lltok_getTok (op) == TPLUS)
+ {
+ ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
+ }
+ else if (lltok_getTok (op) == TMINUS)
+ {
+ 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@*/
+static /*@notnull@*/ /*@only@*/
constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/ constraintExpr expr, int literal)
{
constraintExpr ret;
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;
}
{
constraintExpr ret;
- DPRINTF ( (message ("Making subtract expression") ) );
+ 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;
}
{
constraintExpr ret;
- DPRINTF ( (message ("Doing addTerm simplification") ) );
+ 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 MAXSET:
- return message("MAXSET");
+ return message("maxSet");
case MINSET:
- return message("MINSET");
+ return message("minSet");
case MAXREAD:
- return message("MAXREAD");
+ return message("maxRead");
case MINREAD:
- return message("MINREAD");
+ return message("minRead");
default:
llassert(FALSE);
return message ("<(Unary OP OTHER>");
switch (op)
{
- case PLUS:
+ case BINARYOP_PLUS:
return message("+");
- case MINUS:
+ case BINARYOP_MINUS:
return message("-");
default:
BADEXIT;
}
-bool constraintExpr_search (/*@observer@*/ constraintExpr c, /*@observer@*/ constraintExpr old)
+bool
+constraintExpr_search (/*@observer@*/ constraintExpr c,
+ /*@observer@*/ constraintExpr old)
{
bool ret = FALSE;
constraintExprKind kind;
constraintExpr temp;
- if ( constraintExpr_similar (c, old) )
+ if (constraintExpr_similar (c, old))
{
- DPRINTF((message ("Found %q",
- constraintExpr_unparse(old)
- )));
+ DPRINTF (("Found %q", constraintExpr_unparse (old)));
return TRUE;
}
+ llassert (constraintExpr_isDefined (c) && constraintExpr_isDefined(old) );
+
+ if ( !(constraintExpr_isDefined (c) && constraintExpr_isDefined(old) ) )
+ return FALSE;
+
kind = c->kind;
switch (kind)
{
constraintExprKind kind;
constraintExpr temp;
+ constraintExpr ret;
+
+ llassert(constraintExpr_isDefined (newExpr) && (constraintExpr_isDefined (old) && constraintExpr_isDefined(c) ) );
if ( constraintExpr_similar (c, old) )
{
+
+ ctype newType, cType;
+
+
+
+ ret = constraintExpr_copy (newExpr);
+ llassert(constraintExpr_isDefined(ret) );
+ /*drl if newExpr != NULL then ret will != NULL*/
+
DPRINTF((message ("Replacing %s with %s",
constraintExpr_unparse(old), constraintExpr_unparse(newExpr)
)));
+
+ if (constraintExpr_canGetCType(c) && constraintExpr_canGetCType(newExpr) )
+ {
+ cType = constraintExpr_getCType(c);
+ newType = constraintExpr_getCType(newExpr);
+
+ if (ctype_match(cType,newType) )
+ {
+ DPRINTF(( message("constraintExpr_searchandreplace: replacing "
+ " %s with type %s with %s with type %s",
+ constraintExpr_print(c), ctype_unparse(cType),
+ constraintExpr_print(newExpr), ctype_unparse(newType)
+ )
+ ));
+
+ ret->ct = TRUE;
+ ret->origType = cType;
+ }
+ }
+
+ if (constraintExpr_hasMaxSet(c) )
+ {
+ if (constraintExpr_hasTypeChange(c))
+ {
+ DPRINTF(( message("constraintExpr_searchandreplace: encountered "
+ "MaxSet with changed type %s ",
+ constraintExpr_print(c) )
+ ));
+
+ /*fix this with a conversation */
+ ret = constraintExpr_adjustMaxSetForCast(ret, constraintExpr_getOrigType(c));
+ }
+ }
constraintExpr_free(c);
- return constraintExpr_copy (newExpr);
+
+ return ret;
}
kind = c->kind;
llassert(FALSE);
}
return c;
-
}
-static constraintExpr constraintExpr_simplifyChildren (/*@returned@*/ constraintExpr c)
+/*@notnull@*/ static constraintExpr constraintExpr_simplifyChildren (/*@returned@*/ /*@notnull@*/ constraintExpr c)
{
constraintExprKind kind;
constraintExpr temp;
return c;
}
-static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/constraintExpr c)
+static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/ /*@notnull@*/ constraintExpr c)
{
constraintExpr e1, e2;
constraintExprBinaryOpKind op;
if (constraintExpr_canGetValue (e1) && constraintExpr_canGetValue(e2) )
{
- int i;
+ long i;
i = constraintExpr_getValue(e1) + constraintExpr_getValue (e2);
constraintExpr_free(c);
else
{
op = constraintExprData_binaryExprGetOp (c->data);
- if (op == MINUS)
+ if (op == BINARYOP_MINUS)
if (constraintExpr_similar(e1, e2) )
{
constraintExpr_free(c);
{
constraintExpr expr1, expr2;
constraintExprBinaryOpKind op;
+
+ llassert(constraintExpr_isDefined (lexpr) && constraintExpr_isDefined (expr) );
if (lexpr->kind != binaryexpr)
return expr;
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;
+
+ llassert(constraintExpr_isDefined (expr1) && constraintExpr_isDefined (expr2) );
+
+ /* 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
static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ constraintExpr c)
{
constraintExpr exp;
-
+
+ llassert(constraintExpr_isDefined (c) );
llassert (c->kind == unaryExpr);
- DPRINTF ( (message ("Doing constraintExpr_simplifyunaryExpr:%s", constraintExpr_unparse (c) ) ) );
+ DPRINTF ((message ("Doing constraintExpr_simplifyunaryExpr:%s", constraintExpr_unparse (c) ) ) );
- if ( (constraintExprData_unaryExprGetOp (c->data) != MAXSET) &&
+ if ((constraintExprData_unaryExprGetOp (c->data) != MAXSET) &&
(constraintExprData_unaryExprGetOp (c->data) != MAXREAD) )
{
return c;
}
- // pattern mxr ( var + const) = mxr(var) - const
exp = constraintExprData_unaryExprGetExpr (c->data);
-
+ exp = constraintExpr_copy(exp);
+
+ llassert(constraintExpr_isDefined (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
+ */
+
+ if (constraintTerm_isInitBlock(cterm) )
+ {
+ constraintExpr temp;
+ int len;
+
+ len = constraintTerm_getInitBlockLength(cterm);
+
+ temp = constraintExpr_makeIntLiteral (len );
+
+ 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 ("Doing fancy simplification") ) );
+ DPRINTF ((message ("Doing fancy simplification") ) );
temp = constraintExprData_binaryExprGetExpr2 (exp->data);
c = constraintExpr_makeSubtractExpr (c, temp);
- DPRINTF ( (message ("Done fancy simplification:%s", constraintExpr_unparse (c) ) ) );
+ DPRINTF ((message ("Done fancy simplification:%s", constraintExpr_unparse (c) ) ) );
}
}
- DPRINTF ( (message ("Done simplification:%s", constraintExpr_unparse (c) ) ) );
+ DPRINTF ((message ("constraintExpr_simplifyUnaryExpr: Done simplification:%s", constraintExpr_unparse (c) ) ) );
+
+ constraintExpr_free(exp);
return c;
}
constraintExpr ret;
constraintTerm t;
- DPRINTF ( (message ("Doing constraintExpr_simplify:%s", constraintExpr_unparse (c) ) ) );
+ DPRINTF ((message ("Doing constraintExpr_simplify:%s", constraintExpr_unparse (c) ) ) );
/*@i22*/
- /*I think this is an LCLint bug */
+ /* drl: I think this is an Splint bug */
+ llassert ( constraintExpr_isDefined (c) );
+ if (constraintExpr_isUndefined (c) )
+ {
+ return constraintExpr_undefined;
+ }
+
ret = constraintExpr_copy(c);
-
+ llassert(constraintExpr_isDefined (ret) );
+
constraintExpr_free(c);
ret = constraintExpr_simplifyChildren (ret);
llassert(FALSE);
}
- DPRINTF ( (message ("constraintExpr_simplify returning :%s", constraintExpr_unparse (ret) ) ) );
+ DPRINTF ((message ("constraintExpr_simplify returning :%s", constraintExpr_unparse (ret) ) ) );
return ret;
}
switch (kind)
{
case term:
- st = message ("(%q) ", constraintTerm_print (constraintExprData_termGetTerm(ex->data) ) );
+
+ if (context_getFlag (FLG_PARENCONSTRAINT) )
+ {
+ st = message ("(%q) ", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
+ }
+ else
+ {
+ st = message ("%q", constraintTerm_unparse (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);
return expr;
}
+/*
+/ *@only@* / constraintExpr constraintExpr_doSRefFixInvarConstraint (/ *@only@* / constraintExpr expr, sRef s, ctype ct)
+{
+ constraintExprKind kind;
+ constraintExpr expr1, expr2;
+ constraintExprData data;
+ llassert (expr != NULL);
+
+ data = expr->data;
+
+ kind = expr->kind;
+
+ switch (kind)
+ {
+ case term:
+ expr = doSRefFixInvarConstraintTerm (expr, s, ct);
+ break;
+ case unaryExpr:
+ expr1 = constraintExprData_unaryExprGetExpr (data);
+ expr1 = constraintExpr_copy(expr1);
+ expr1 = constraintExpr_doSRefFixInvarConstraint (expr1, s, ct);
+ data = constraintExprData_unaryExprSetExpr (data, expr1);
+ break;
+ case binaryexpr:
+ expr1 = constraintExprData_binaryExprGetExpr1 (data);
+ expr2 = constraintExprData_binaryExprGetExpr2 (data);
+
+ expr1 = constraintExpr_copy(expr1);
+ expr2 = constraintExpr_copy(expr2);
+
+ expr1 = constraintExpr_doSRefFixInvarConstraint (expr1, s, ct);
+ data = constraintExprData_binaryExprSetExpr1 (data, expr1);
+ expr2 = constraintExpr_doSRefFixInvarConstraint (expr2, s, ct);
+ data = constraintExprData_binaryExprSetExpr2 (data, expr2);
+
+ break;
+ default:
+ llassert(FALSE);
+ data = NULL;
+ }
+ return expr;
+}
+*/
+
/*@only@*/ constraintExpr constraintExpr_doSRefFixConstraintParam (/*@only@*/ constraintExpr expr, exprNodeList arglist) /*@modifies expr@*/
{
constraintExprKind kind;
cstring constraintExpr_print (constraintExpr expr) /*@*/
{
- return constraintExpr_unparse(expr);
+ return constraintExpr_unparse (expr);
}
bool constraintExpr_hasMaxSet (constraintExpr expr) /*@*/
t = constraintExpr_unparse(expr);
- if (cstring_containsLit(t, "MAXSET") != NULL )
+ if (cstring_containsLit(t, "maxSet") != NULL )
{
cstring_free(t);
return (TRUE);
0 => expr1 == expr2
-1 => expr1 < expr2
*/
+
int constraintExpr_compare (constraintExpr expr1, constraintExpr expr2)
{
- int value1, value2;
+ long value1, value2;
if (constraintExpr_similar (expr1, expr2) )
{
return 0;
}
+
value1 = constraintExpr_getValue(expr1);
value2 = constraintExpr_getValue(expr2);
return -1;
}
-int constraintExpr_getValue (constraintExpr expr)
+long constraintExpr_getValue (constraintExpr expr)
{
+ llassert (constraintExpr_isDefined(expr) );
llassert (expr->kind == term);
- return (constraintTerm_getValue (constraintExprData_termGetTerm (expr->data) ) );
+
+ return (constraintTerm_getValue (constraintExprData_termGetTerm (expr->data)));
}
bool constraintExpr_canGetValue (constraintExpr expr)
{
+ llassert ( constraintExpr_isDefined (expr) );
+ if (constraintExpr_isUndefined (expr) )
+ {
+ return FALSE;
+ }
+
switch (expr->kind)
{
case term:
constraintTerm t;
constraintExprKind kind;
+ llassert ( constraintExpr_isDefined (expr) );
+ if (constraintExpr_isUndefined (expr) )
+ {
+ return fileloc_undefined;
+ }
+
+
kind = expr->kind;
switch (kind)
{
constraintTerm t;
sRef s;
- /*maybe this should move to cosntraintExpr.c -drl7x 5/18/01*/
- /*@i22*/ constraintExprData data = e->data;
+ constraintExprData data;
+ constraintExprKind kind;
+ constraintExpr ret;
- /*@i22*/constraintExprKind kind = e->kind;
+ llassert (constraintExpr_isDefined (e) );
+
+ data = e->data;
+ kind = e->kind;
+
+ llassert (kind == term);
- constraintExpr ret;
-
- llassert(kind == term);
-
t = constraintExprData_termGetTerm (data);
- llassert (constraintTerm_isDefined(t) );
-
+ llassert (constraintTerm_isDefined (t));
+
ret = e;
- switch (constraintTerm_getKind(t) )
+
+ switch (constraintTerm_getKind (t))
{
- case EXPRNODE:
- break;
- case INTLITERAL:
+ case CTT_EXPR:
+ case CTT_INTLITERAL:
break;
- case SREF:
+ case CTT_SREF:
s = constraintTerm_getSRef(t);
if (sRef_isResult (s))
{
}
-/*drl moved from constriantTerm.c 5/20/001*/
-/*@only@*/ static constraintExpr
-doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
+#if 0
+
+/*to be used for structure checking */
+
+/ *@only@* / static constraintExpr
+doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e,
+ sRef s, ctype ct)
{
constraintTerm t;
llassert (constraintTerm_isDefined(t) );
ret = e;
- /*@i1*/ switch (t->kind)
+
+ DPRINTF (("Fixing: %s", constraintExpr_print (e)));
+
+ switch (constraintTerm_getKind(t))
{
- case EXPRNODE:
- DPRINTF((message ("%q @ %q ", constraintTerm_print(t),
+ case CTT_EXPR:
+ DPRINTF((message ("%q @ %q ", constraintTerm_unparse(t),
fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
break;
- case INTLITERAL:
- DPRINTF((message (" %q ", constraintTerm_print (t)) ));
+ case CTT_INTLITERAL:
+ DPRINTF((message (" %q ", constraintTerm_unparse (t)) ));
break;
- case SREF:
- DPRINTF (( message("Doing sRef_fixConstraintParam for %q ",
- constraintTerm_print (t) ) ));
- ret = sRef_fixConstraintParam (constraintTerm_getSRef(t), arglist);
-
- constraintExpr_free(e);
+ case CTT_SREF:
+ / * evans 2001-07-24: constants should use the original term * /
+ if (!constraintTerm_canGetValue (t))
+ {
+ sRef snew;
+ DPRINTF ((message("Doing sRef_fixInvarConstraint for %q ",
+ constraintTerm_unparse (t) ) ));
+
+ snew = fixSref (ct, s, constraintTerm_getSRef(t));
+
+ ret = constraintExpr_makeTermsRef(snew);
+
+ constraintExpr_free (e);
+
+ DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
+ constraintExpr_print (ret) ) ));
+ / *@-branchstate@* /
+ } / *@=branchstate@* /
- DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
- constraintExpr_print (ret) ) ));
break;
default:
BADEXIT;
}
+
return ret;
}
+#endif
+
+/*drl moved from constriantTerm.c 5/20/001*/
+/*@only@*/ static constraintExpr
+doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
+{
+ constraintTerm t;
+
+ constraintExprData data;
+
+ constraintExprKind kind;
+
+ constraintExpr ret;
-/* bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term) */
-/* { */
-/* if (constraintTerm_hasTerm (expr->term, term) ) */
-/* return TRUE; */
+ llassert(constraintExpr_isDefined (e) );
-/* if ( (expr->expr) != NULL) */
-/* { */
-/* return ( constraintExpr_includesTerm (expr->expr, term) ); */
-/* } */
-/* return FALSE; */
+ data = e->data;
+
+ kind = e->kind;
-/* } */
+
+
+ llassert(kind == term);
+
+ t = constraintExprData_termGetTerm (data);
+ llassert (constraintTerm_isDefined(t) );
+
+ ret = e;
+
+ DPRINTF (("Fixing: %s", constraintExpr_print (e)));
+
+ switch (constraintTerm_getKind(t))
+ {
+ case CTT_EXPR:
+ DPRINTF((message ("%q @ %q ", constraintTerm_unparse(t),
+ fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
+ break;
+ case CTT_INTLITERAL:
+ DPRINTF((message (" %q ", constraintTerm_unparse (t)) ));
+ break;
+ case CTT_SREF:
+ /* evans 2001-07-24: constants should use the original term */
+ if (!constraintTerm_canGetValue (t))
+ {
+ DPRINTF ((message("Doing sRef_fixConstraintParam for %q ",
+ constraintTerm_unparse (t) ) ));
+ ret = sRef_fixConstraintParam (constraintTerm_getSRef(t), arglist);
+
+ constraintExpr_free (e);
+
+ DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ",
+ constraintExpr_print (ret) ) ));
+ /*@-branchstate@*/
+ } /*@=branchstate@*/
+
+ break;
+ default:
+ BADEXIT;
+ }
+
+ return ret;
+
+}
+
+
+#if 0
+bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term)
+{
+ if (constraintTerm_hasTerm (expr->term, term) )
+ return TRUE;
+
+ if ((expr->expr) != NULL)
+ {
+ return ( constraintExpr_includesTerm (expr->expr, term) );
+ }
+ return FALSE;
+
+}
+#endif
/*drl added 6/11/01 */
bool constraintExpr_isBinaryExpr (/*@observer@*/ constraintExpr c)
{
+
+ llassert(constraintExpr_isDefined (c) );
+
+ if ( ! (constraintExpr_isDefined (c) ) )
+ return FALSE;
+
if (c->kind == binaryexpr)
return TRUE;
return FALSE;
}
+/*drl added 8/08/001 */
+bool constraintExpr_isTerm (/*@observer@*/ constraintExpr c) /*@*/
+{
+ llassert(constraintExpr_isDefined (c) );
+
+ if (c->kind == term)
+ return TRUE;
+
+ else
+ return FALSE;
+}
+
+/*@observer@*/ /*@temp@*/ constraintTerm constraintExpr_getTerm ( /*@temp@*/ /*@observer@*/ constraintExpr c) /*@*/
+{
+ constraintTerm term;
+
+ llassert(constraintExpr_isDefined (c) );
+
+ llassert(constraintExpr_isTerm(c) );
+
+ term = constraintExprData_termGetTerm(c->data);
+
+ return term;
+}
+
static void binaryExpr_dump (/*@observer@*/ constraintExprData data, FILE *f)
{
constraintExpr expr1;
char * str;
char * os;
- str = mstring_create (MAX_DUMP_LINE_LENGTH);
- os = str;
+ os = mstring_create (MAX_DUMP_LINE_LENGTH);
+
str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+ if (! mstring_isDefined(str) )
+ {
+ llfatalbug(message("Library file is corrupted") );
+ }
binaryOp = (constraintExprBinaryOpKind) reader_getInt(&str);
str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+ if (! mstring_isDefined(str) )
+ {
+ llfatalbug(message("Library file is corrupted") );
+ }
+
reader_checkChar (&str, 'e');
reader_checkChar (&str, '1');
os = str;
str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+ if (! mstring_isDefined(str) )
+ {
+ llfatalbug(message("Library file is corrupted") );
+ }
+
unaryOp = (constraintExprUnaryOpKind) reader_getInt(&str);
expr = constraintExpr_undump (f);
constraintExprKind kind;
constraintTerm t;
+
+ llassert(constraintExpr_isDefined(expr) );
+
+ DPRINTF((message("constraintExpr_dump:: dumping constraintExpr %s",
+ constraintExpr_unparse(expr)
+ ) ));
kind = expr->kind;
s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+ if (! mstring_isDefined(s) )
+ {
+ llfatalbug(message("Library file is corrupted") );
+ }
+
kind = (constraintExprKind) reader_getInt(&s);
free (os);
}
+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;
+}
+
+
+bool constraintExpr_canGetCType (constraintExpr e) /*@*/
+{
+ if (constraintExpr_isUndefined(e) )
+ return FALSE;
+
+ if (e->kind == term)
+ {
+ return TRUE;
+ }
+ else
+ {
+ DPRINTF(( message("constraintExpr_canGetCType: can't get type for %s ",
+ constraintExpr_print(e) ) ));
+ return FALSE;
+ }
+}
+
+ctype constraintExpr_getCType (constraintExpr e) /*@*/
+{
+ constraintTerm t;
+
+ llassert(constraintExpr_isDefined(e) );
+
+ llassert(constraintExpr_canGetCType(e) );
+
+ switch (e->kind)
+ {
+ case term:
+ t = constraintExprData_termGetTerm (e->data);
+ return (constraintTerm_getCType(t) );
+ /* assume that a unary expression will be an int ... */
+ case unaryExpr:
+ return ctype_signedintegral;
+
+ /* drl for just return type of first operand */
+ case binaryexpr:
+ return (
+ constraintExpr_getCType
+ (constraintExprData_binaryExprGetExpr1 (e->data) )
+ );
+ default:
+ BADEXIT;
+ }
+ BADEXIT;
+}
+/* drl add 10-5-001 */
+static bool constraintExpr_hasTypeChange(constraintExpr e)
+{
+ llassert(constraintExpr_isDefined(e) );
+ if (constraintExpr_isDefined((e)) && (e->ct == TRUE) )
+ {
+ return TRUE;
+ }
+
+ if (e->kind == unaryExpr)
+ {
+ if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
+ {
+ constraintExpr ce;
+
+ ce = constraintExprData_unaryExprGetExpr(e->data);
+
+ return (constraintExpr_hasTypeChange(ce) );
+ }
+
+ }
+ return FALSE;
+}
+
+/* drl add 10-5-001 */
+
+static ctype constraintExpr_getOrigType (constraintExpr e)
+{
+
+ llassert(constraintExpr_isDefined(e) );
+ llassert(constraintExpr_hasTypeChange(e) );
+
+
+ if (e->ct == TRUE)
+ {
+ return e->origType;
+ }
+
+ if (e->kind == unaryExpr)
+ {
+ if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
+ {
+ constraintExpr ce;
+
+ ce = constraintExprData_unaryExprGetExpr(e->data);
+
+ return (constraintExpr_getOrigType(ce) );
+ }
+
+ }
+
+ BADEXIT;
+}
+
+/*drl added these around 10/18/001*/
+
+static /*@only@*/ constraintExpr constraintExpr_div (/*@only@*/ constraintExpr e, /*@unused@*/ ctype ct)
+{
+ return e;
+}
+
+
+/*@access exprNode@*/
+static /*@only@*/ constraintExpr constraintTerm_simpleDivTypeExprNode(/*@only@*/ constraintExpr e, ctype ct)
+{
+ exprData data;
+ exprNode t1, t2, expr;
+ lltok tok;
+ constraintTerm t;
+
+ llassert(constraintExpr_isDefined(e) );
+
+ DPRINTF((
+ message("constraintTerm_simpleDivTypeExprNode e=%s, ct=%s",
+ constraintExpr_print(e), ctype_unparse(ct)
+ )
+ ));
+
+ t = constraintExprData_termGetTerm(e->data);
+
+ expr = constraintTerm_getExprNode(t);
+
+ llassert(constraintExpr_isDefined(e) );
+ llassert(exprNode_isDefined(expr) );
+
+ if (expr->kind == XPR_OP)
+ {
+ data = expr->edata;
+
+ t1 = exprData_getOpA (data);
+ t2 = exprData_getOpB (data);
+ tok = exprData_getOpTok (data);
+ if (lltok_isMult(tok) )
+ {
+ llassert(exprNode_isDefined(t1) && exprNode_isDefined(t2) );
+ /*drl 3/2/2003 we know this from the fact that it's a
+ multiplication operation...*/
+
+ if ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
+ {
+ ctype ct2;
+
+ if (t1->kind == XPR_SIZEOFT)
+ {
+ ct2 = qtype_getType (exprData_getType (t1->edata));
+ }
+ else
+ {
+ exprNode tempE;
+
+ tempE = exprData_getSingle (t1->edata);
+
+ ct2 = exprNode_getType (tempE);
+ }
+ if (ctype_match (ctype_makePointer(ct2), ct) )
+ {
+ /* this is a bit sloopy but ... */
+ constraintExpr_free(e);
+ return constraintExpr_makeExprNode(t2);
+ }
+ }
+
+
+ else if ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
+ {
+ ctype ct2;
+
+ if (t2->kind == XPR_SIZEOFT)
+ {
+ ct2 = qtype_getType (exprData_getType (t2->edata));
+ }
+ else
+ {
+ exprNode exprTemp;
+ exprData eDTemp;
+
+ exprTemp = exprData_getSingle (t2->edata);
+
+ llassert(exprNode_isDefined(exprTemp) );
+ eDTemp = exprTemp->edata;
+
+ ct2 = qtype_getType (exprData_getType(eDTemp ) );
+
+ }
+ if (ctype_match (ctype_makePointer(ct2),ct) )
+ {
+ /* sloopy way to do this... */ /*@i22*/
+ constraintExpr_free(e);
+ return constraintExpr_makeExprNode(t1);
+ }
+ }
+ else
+ {
+ /*empty*/
+ }
+
+ }
+ }
+ return (constraintExpr_div (e, ct) );
+}
+/*@noaccess exprNode@*/
+
+static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype ct)
+{
+ /*@i333*/
+ DPRINTF(( (message("simpleDiv got %s ", constraintExpr_unparse(e) ) )
+ ));
+
+ llassert(constraintExpr_isDefined(e) );
+
+ switch (e->kind)
+ {
+ case term:
+
+ {
+ constraintTerm t;
+
+ t = constraintExprData_termGetTerm(e->data);
+
+
+ if (constraintTerm_isExprNode (t) )
+ {
+ return constraintTerm_simpleDivTypeExprNode(e, ct);
+
+ /* search for * size of ct and remove */
+ }
+ return constraintExpr_div (e, ct);
+ }
+
+ case binaryexpr:
+ {
+ constraintExpr temp;
+
+ temp = constraintExprData_binaryExprGetExpr1 (e->data);
+ temp = constraintExpr_copy(temp);
+ temp = simpleDivType (temp, ct);
+
+ e->data = constraintExprData_binaryExprSetExpr1 (e->data, temp);
+
+ temp = constraintExprData_binaryExprGetExpr2 (e->data);
+ temp = constraintExpr_copy(temp);
+ temp = simpleDivType (temp, ct);
+ e->data = constraintExprData_binaryExprSetExpr2 (e->data, temp);
+
+ DPRINTF(( (message("simpleDiv binaryexpr returning %s ", constraintExpr_unparse(e) ) )
+ ));
+
+ return e;
+ }
+ case unaryExpr:
+ return constraintExpr_div (e, ct);
+
+ default:
+ BADEXIT;
+ }
+}
+
+static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr e, ctype ct)
+{
+
+ DPRINTF(( (message("constraintExpr_adjustMaxSetForCast got %s ", constraintExpr_unparse(e) ) )
+ ));
+
+ e = constraintExpr_makeIncConstraintExpr(e);
+
+ e = constraintExpr_simplify(e);
+
+
+ e = simpleDivType (e, ct);
+
+ e = constraintExpr_makeDecConstraintExpr(e);
+
+ e = constraintExpr_simplify(e);
+
+ DPRINTF(( (message("constraintExpr_adjustMaxSetForCast returning %s ", constraintExpr_unparse(e) ) )
+ ));
+
+ return e;
+}
+
+
+bool constraintExpr_isConstantOnly ( constraintExpr e )
+{
+ DPRINTF(( (message("constraintExpr_isConstantOnly %s ",
+ constraintExpr_unparse(e) ) )
+ ));
+
+ llassert(constraintExpr_isDefined(e) );
+
+ switch (e->kind)
+ {
+ case term:
+ {
+ constraintTerm t;
+
+ t = constraintExprData_termGetTerm(e->data);
+
+
+ if (constraintTerm_isConstantOnly (t) )
+ {
+ return TRUE;
+ }
+ else
+ {
+ return FALSE;
+ }
+ }
+
+ case binaryexpr:
+ {
+ constraintExpr temp1, temp2;
+
+ temp1 = constraintExprData_binaryExprGetExpr1 (e->data);
+
+ temp2 = constraintExprData_binaryExprGetExpr2 (e->data);
+
+ if (constraintExpr_isConstantOnly(temp1) &&
+ constraintExpr_isConstantOnly(temp2) )
+ {
+ return TRUE;
+ }
+ else
+ {
+ return FALSE;
+ }
+ }
+
+ case unaryExpr:
+ {
+ constraintExpr temp;
+
+ temp = constraintExprData_unaryExprGetExpr (e->data );
+
+ if (constraintExpr_isConstantOnly(temp) )
+ {
+ return TRUE;
+ }
+ else
+ {
+ return FALSE;
+ }
+ }
+ default:
+ BADEXIT;
+ }
+}
andersk / splint.git / blobdiff