/*
** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
# include "exprChecks.h"
# include "exprNodeSList.h"
-/*@-czechfcns@*/
-
-/*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */
-/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
-/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
-/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
-
static ctype constraintExpr_getOrigType (constraintExpr p_e);
static bool constraintExpr_hasTypeChange(constraintExpr p_e) /*@*/;
doFixResultTerm (/*@only@*/ constraintExpr p_e, /*@exposed@*/ exprNode p_fcnCall)
/*@modifies p_e@*/;
-static bool constraintExpr_canGetCType (constraintExpr p_e) /*@*/;
+static bool constraintExpr_canGetCType (constraintExpr p_e) /*@*/;
static ctype constraintExpr_getCType (constraintExpr p_e);
-static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr p_e, ctype p_ct);
+static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast (/*@only@*/ constraintExpr p_e,
+ ctype p_tfrom, ctype p_tto,
+ fileloc p_loc);
-/*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
+/*@special@*/ /*@notnull@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
/* @allocates result->data @ @sets result->kind @ */ ;
void constraintExpr_free (/*@only@*/ constraintExpr expr)
/* 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;
- llassert (expr != NULL); /* evans 2001-07-18 */
expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
}
-/*@only@*/ constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
+/*@only@*//*@notnull@*/ constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
/*@out@*/ bool * propagate,
/*@out@*/ int *literal)
{
constraintExpr_free(expr1);
constraintExpr_free(expr);
-
+
+ llassert (constraintExpr_isDefined(temp) );
return temp;
}
else
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 ("After combine %s", constraintExpr_unparse(expr) ) ) );
- return expr;
+
+ llassert(constraintExpr_isDefined(expr) );
+ return expr;
}
/*@special@*/
{
constraintExpr ret;
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);
return ret;
}
+/*@access exprNode@*/
constraintExpr constraintExpr_makeExprNode (exprNode e)
{
sRef s;
exprNode t, t1, t2;
lltok tok;
- llassert (e != NULL);
+ if (exprNode_isUndefined (e))
+ {
+ return constraintExpr_undefined;
+ }
data = e->edata;
size = (int) sRef_getArraySize(s);
ret = constraintExpr_makeIntLiteral (size);
}
- else if ( exprNode_isStringLiteral (t) )
+ else if (exprNode_isStringLiteral (t))
{
- cstring str;
- int size;
-
- str = multiVal_forceString(exprNode_getValue(t) );
- size = cstring_length (str) + 1;
- ret = constraintExpr_makeIntLiteral (size);
+ cstring str = multiVal_forceString (exprNode_getValue(t));
+ ret = constraintExpr_makeIntLiteral (size_toLong (cstring_length (str) + 1));
}
else
{
ret = constraintExpr_parseMakeBinaryOp (ce1, tok, ce2);
}
-
- /*@i333*/
- /* uncomment this block to activate the cheesy heuristic
- for handling sizeof expressions
+
+ /* define this block to activate the cheesy heuristic
+ for handling sizeof expressions*/
+#if 0
+
- / *
+ /*
drl 8-11-001
We handle expressions containing sizeof with the rule
This is the total wronge way to do this but...
it may be better than nothing
- * /
+ */
ret = oldconstraintExpr_makeTermExprNode (e);
}
}
- */
+#endif
+
else
ret = oldconstraintExpr_makeTermExprNode (e);
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);
ret = constraintExpr_makeExprNode (t);
break;
case XPR_COMMA:
- t = exprData_getPairA(data);
+ t = exprData_getPairA (data);
ret = constraintExpr_makeExprNode(t);
- /*@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)
{
return oldconstraintExpr_makeTermExprNode(e);
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 = 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();
}
-/*@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();
return ret;
}
-/*@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;
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;
}
-/*@only@*/
+/*@only@*/ /*@notnull@*/
constraintExpr constraintExpr_makeIntLiteral (long i)
{
constraintExpr ret;
}
*/
-/*@only@*/
+/*@only@*/ /*@notnull@*/
/*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
/*@allocates result->data @*/ /*@sets result->kind @*/
{
}
-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;
}
# endif
-static /*@only@*/
+static /*@notnull@*/ /*@only@*/
constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/ constraintExpr expr, int literal)
{
constraintExpr ret;
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)
}
-/*@only@*/ constraintExpr constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr c, /*@temp@*/ constraintExpr old, /*@temp@*/ constraintExpr newExpr )
+/*@only@*/ constraintExpr
+constraintExpr_searchandreplace (/*@only@*/ /*@unique@*/ constraintExpr c, /*@temp@*/ constraintExpr old,
+ /*@temp@*/ constraintExpr newExpr )
{
constraintExprKind kind;
constraintExpr temp;
constraintExpr ret;
+
+ llassert (constraintExpr_isDefined (newExpr) && (constraintExpr_isDefined (old) && constraintExpr_isDefined(c) ) );
- if ( constraintExpr_similar (c, old) )
+ if (constraintExpr_similar (c, old))
{
-
- ctype newType, cType;
-
+ ctype newType = ctype_unknown;
+ ctype cType = ctype_unknown;
ret = constraintExpr_copy (newExpr);
+ llassert(constraintExpr_isDefined(ret) );
+ /*drl if newExpr != NULL then ret will != NULL*/
+
+ DPRINTF (("Replacing %s with %s in %s",
+ constraintExpr_unparse (old), constraintExpr_unparse (newExpr),
+ constraintExpr_unparse (c)));
- DPRINTF((message ("Replacing %s with %s",
- constraintExpr_unparse(old), constraintExpr_unparse(newExpr)
- )));
-
- if (constraintExpr_canGetCType(c) && constraintExpr_canGetCType(newExpr) )
+ if (constraintExpr_canGetCType (c) && constraintExpr_canGetCType (newExpr))
{
cType = constraintExpr_getCType(c);
- newType = constraintExpr_getCType(newExpr);
+ newType = constraintExpr_getCType (newExpr);
- if (ctype_match(cType,newType) )
+ 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)
- )
- ));
+ DPRINTF (("constraintExpr_searchandreplace: replacing "
+ " %s with type %s with %s with type %s",
+ constraintExpr_unparse (c), ctype_unparse(cType),
+ constraintExpr_unparse (newExpr), ctype_unparse(newType)));
ret->ct = TRUE;
ret->origType = cType;
+ DPRINTF (("Type: %s", ctype_unparse (constraintExpr_getCType (ret))));
}
}
-
- if (constraintExpr_hasMaxSet(c) )
+
+ 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));
- }
+ if (constraintExpr_hasTypeChange (c))
+ {
+ fileloc loc = constraintExpr_loc (c);
+ DPRINTF (("constraintExpr_searchandreplace: encountered "
+ "MaxSet with changed type %s ",
+ constraintExpr_unparse (c)));
+
+ if (c->kind == unaryExpr)
+ {
+ constraintExpr ce = constraintExprData_unaryExprGetExpr (c->data);
+ DPRINTF (("Its a unary! %s / %s",
+ ctype_unparse (constraintExpr_getCType (ce)),
+ ctype_unparse (constraintExpr_getOrigType (ce))));
+ ret = constraintExpr_adjustMaxSetForCast (ret, constraintExpr_getCType (ce),
+ constraintExpr_getOrigType (ce),
+ loc);
+ }
+ else
+ {
+ /* fix this with a conversation */
+ DPRINTF (("Types: %s / %s", ctype_unparse (newType), ctype_unparse (cType)));
+ ret = constraintExpr_adjustMaxSetForCast (ret, constraintExpr_getCType (c),
+ constraintExpr_getOrigType(c),
+ loc);
+ }
+ }
}
- constraintExpr_free(c);
-
+
+ constraintExpr_free (c);
+ DPRINTF (("ret: %s", constraintExpr_unparse (ret)));
return ret;
}
case term:
break;
case unaryExpr:
+ DPRINTF (("Making unary expression!"));
temp = constraintExprData_unaryExprGetExpr (c->data);
- temp = constraintExpr_copy(temp);
+ temp = constraintExpr_copy (temp);
temp = constraintExpr_searchandreplace (temp, old, newExpr);
c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
break;
case binaryexpr:
-
+ DPRINTF (("Making binary expression!"));
temp = constraintExprData_binaryExprGetExpr1 (c->data);
- temp = constraintExpr_copy(temp);
+ temp = constraintExpr_copy (temp);
temp = constraintExpr_searchandreplace (temp, old, newExpr);
c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
temp = constraintExprData_binaryExprGetExpr2 (c->data);
- temp = constraintExpr_copy(temp);
+ temp = constraintExpr_copy (temp);
temp = constraintExpr_searchandreplace (temp, old, newExpr);
c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
break;
default:
- llassert(FALSE);
+ llassert (FALSE);
}
+
+ DPRINTF (("ret: %s", constraintExpr_unparse (c)));
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;
{
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);
-
+
+ llassert(constraintExpr_isDefined (expr1) && constraintExpr_isDefined (expr2) );
+
/* drl possible problem : warning make sure this works */
lexpr->kind = expr1->kind;
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) ) ) );
exp = constraintExprData_unaryExprGetExpr (c->data);
exp = constraintExpr_copy(exp);
+ llassert(constraintExpr_isDefined (exp) );
+
if (exp->kind == term)
{
constraintTerm cterm;
DPRINTF ((message ("Doing constraintExpr_simplify:%s", constraintExpr_unparse (c) ) ) );
- /*@i22*/
- /* 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);
}
/*@only@*/
-cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr ex) /*@*/
+cstring constraintExpr_unparse (/*@temp@*/ constraintExpr ex) /*@*/
{
cstring st;
constraintExprKind kind;
switch (kind)
{
case term:
-
- if (context_getFlag (FLG_PARENCONSTRAINT) )
- {
- st = message ("(%q) ", constraintTerm_print (constraintExprData_termGetTerm (ex->data)));
- }
- else
- {
- 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)",
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) )
- );
+ 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) )
+ constraintExpr_unparse (constraintExprData_binaryExprGetExpr1 (ex->data)),
+ constraintExprBinaryOpKind_print (constraintExprData_binaryExprGetOp (ex->data)),
+ constraintExpr_unparse (constraintExprData_binaryExprGetExpr2 (ex->data))
);
}
long constraintExpr_getValue (constraintExpr expr)
{
+ llassert (constraintExpr_isDefined(expr) );
llassert (expr->kind == term);
+
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:
BADEXIT;
}
-fileloc constraintExpr_getFileloc (constraintExpr expr)
+fileloc constraintExpr_loc (constraintExpr expr)
{
constraintExpr e;
constraintTerm t;
constraintExprKind kind;
+ llassert ( constraintExpr_isDefined (expr) );
+ if (constraintExpr_isUndefined (expr) )
+ {
+ return fileloc_undefined;
+ }
+
+
kind = expr->kind;
switch (kind)
break;
case unaryExpr:
e = constraintExprData_unaryExprGetExpr (expr->data);
- return (constraintExpr_getFileloc (e) );
+ return (constraintExpr_loc (e) );
/*@notreached@*/
break;
case binaryexpr:
e = constraintExprData_binaryExprGetExpr1 (expr->data);
- return (constraintExpr_getFileloc (e) );
+ return (constraintExpr_loc (e) );
/*@notreached@*/
break;
}
{
constraintTerm t;
sRef s;
- /*maybe this should move to cosntraintExpr.c -drl7x 5/18/01*/
- /*@i22*/
-
- constraintExprData data = e->data;
- constraintExprKind kind = e->kind;
-
+ constraintExprData data;
+ constraintExprKind kind;
constraintExpr ret;
-
- llassert(kind == term);
-
+
+ llassert (constraintExpr_isDefined (e) );
+
+ data = e->data;
+ kind = e->kind;
+
+ 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))
{
return ret;
}
-/*
+
+#if 0
+
+/*to be used for structure checking */
+
/ *@only@* / static constraintExpr
-doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e,
- sRef s, ctype ct)
+doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e, sRef s, ctype ct)
{
constraintTerm t;
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:
+ 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_print (t) ) ));
+ constraintTerm_unparse (t) ) ));
snew = fixSref (ct, s, constraintTerm_getSRef(t));
return ret;
}
-*/
+#endif
/*drl moved from constriantTerm.c 5/20/001*/
/*@only@*/ static constraintExpr
{
constraintTerm t;
- constraintExprData data = e->data;
+ constraintExprData data;
- constraintExprKind kind = e->kind;
+ constraintExprKind kind;
constraintExpr ret;
+
+ llassert(constraintExpr_isDefined (e) );
+
+ data = e->data;
+
+ kind = e->kind;
+
+
+
llassert(kind == term);
t = constraintExprData_termGetTerm (data);
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:
+ 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_print (t) ) ));
+ constraintTerm_unparse (t) ) ));
ret = sRef_fixConstraintParam (constraintTerm_getSRef(t), arglist);
constraintExpr_free (e);
}
-/* bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term) */
-/* { */
-/* if (constraintTerm_hasTerm (expr->term, term) ) */
-/* return TRUE; */
+#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; */
+ 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;
/*drl added 8/08/001 */
bool constraintExpr_isTerm (/*@observer@*/ constraintExpr c) /*@*/
{
+ llassert(constraintExpr_isDefined (c) );
+
if (c->kind == term)
return TRUE;
{
constraintTerm term;
+ llassert(constraintExpr_isDefined (c) );
+
llassert(constraintExpr_isTerm(c) );
term = constraintExprData_termGetTerm(c->data);
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);
constraintTerm t;
+ llassert(constraintExpr_isDefined(expr) );
+
DPRINTF((message("constraintExpr_dump:: dumping constraintExpr %s",
constraintExpr_unparse(expr)
) ));
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);
}
-bool constraintExpr_canGetCType (constraintExpr e) /*@*/
+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) ) ));
+ DPRINTF (("constraintExpr_canGetCType: can't get type for %s", constraintExpr_unparse (e)));
return FALSE;
}
}
ctype constraintExpr_getCType (constraintExpr e) /*@*/
{
constraintTerm t;
-
- llassert(constraintExpr_canGetCType(e) );
+
+ llassert (constraintExpr_isDefined (e));
+ llassert (constraintExpr_canGetCType (e));
switch (e->kind)
{
return (constraintTerm_getCType(t) );
/* assume that a unary expression will be an int ... */
case unaryExpr:
- return ctype_signedintegral;
-
+ return ctype_unknown; /* was ctype_signedintegral; */
/* drl for just return type of first operand */
case binaryexpr:
- return (
- constraintExpr_getCType
- (constraintExprData_binaryExprGetExpr1 (e->data) )
- );
+ return (constraintExpr_getCType (constraintExprData_binaryExprGetExpr1 (e->data)));
default:
BADEXIT;
}
/* drl add 10-5-001 */
-static bool constraintExpr_hasTypeChange(constraintExpr e)
+static bool constraintExpr_hasTypeChange (constraintExpr e)
{
- if (constraintExpr_isDefined((e)) && (e->ct == TRUE) )
+ llassert(constraintExpr_isDefined(e));
+
+ if (constraintExpr_isDefined((e)) && (e->ct == TRUE))
{
return TRUE;
}
{
if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
{
- constraintExpr ce;
-
- ce = constraintExprData_unaryExprGetExpr(e->data);
-
- return (constraintExpr_hasTypeChange(ce) );
+ constraintExpr ce = constraintExprData_unaryExprGetExpr(e->data);
+ DPRINTF (("Unary type change: [%x] %s", ce, constraintExpr_unparse (ce)));
+ DPRINTF (("Types: %s / %s", ctype_unparse (constraintExpr_getCType (ce)),
+ ctype_unparse (constraintExpr_getOrigType (ce))));
+ return (constraintExpr_hasTypeChange(ce));
}
-
}
+
return FALSE;
}
static ctype constraintExpr_getOrigType (constraintExpr e)
{
-
- llassert(constraintExpr_hasTypeChange(e) );
-
+ llassert (constraintExpr_isDefined (e));
+ llassert (constraintExpr_hasTypeChange (e));
if (e->ct == TRUE)
{
{
if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
{
- constraintExpr ce;
-
- ce = constraintExprData_unaryExprGetExpr(e->data);
-
- return (constraintExpr_getOrigType(ce) );
+ constraintExpr ce = constraintExprData_unaryExprGetExpr (e->data);
+ return (constraintExpr_getOrigType(ce));
}
}
/*drl added these around 10/18/001*/
-static /*@only@*/ constraintExpr constraintExpr_div (/*@only@*/ constraintExpr e, /*@unused@*/ ctype ct)
+static /*@only@*/ constraintExpr
+constraintExpr_div (/*@only@*/ constraintExpr e, ctype tfrom, ctype tto, fileloc loc)
{
+ int sizefrom = ctype_getSize (tfrom);
+ int sizeto = ctype_getSize (tto);
+
+ DPRINTF (("constraintExpr_div: %s", constraintExpr_unparse (e)));
+ DPRINTF (("Types: %s / %s",
+ ctype_unparse (tfrom),
+ ctype_unparse (tto)));
+
+ if (sizefrom == -1) {
+ llbug (message ("constraintExpr_div: type size unknown: %s", ctype_unparse (tfrom)));
+ }
+
+ if (sizeto == -1) {
+ llbug (message ("constraintExpr_div: type size unknown: %s", ctype_unparse (tto)));
+ }
+
+ if (sizeto == sizefrom)
+ {
+ DPRINTF (("Sizes match: %d / %d", sizeto, sizefrom));
+ ; /* Sizes match, a-ok */
+ }
+ else
+ {
+ float scale = (float) sizefrom / (float) sizeto;
+ constraintTerm ct;
+ long val;
+ float fnewval;
+ long newval;
+
+ llassert (e != NULL);
+ llassert (e->kind == term);
+ ct = constraintExprData_termGetTerm (e->data);
+ DPRINTF (("constraint: %s / %s", constraintExpr_unparse (e), constraintTerm_unparse (ct)));
+ llassert (constraintTerm_canGetValue (ct));
+ val = constraintTerm_getValue (ct);
+
+ DPRINTF (("Scaling constraints by: %ld * %f", val, scale));
+
+ fnewval = ((float) val) * scale;
+ newval = (long) fnewval;
+
+ DPRINTF (("Values: %f / %ld", fnewval, newval));
+
+ if ((fnewval - (float) newval) > FLT_EPSILON)
+ {
+ voptgenerror (FLG_ALLOCMISMATCH,
+ message ("Allocated memory is converted to type %s of (size %d), "
+ "which is not divisible into original allocation of space "
+ "for %d elements of type %s (size %d)",
+ ctype_unparse (tto), sizeto,
+ long_toInt (val), ctype_unparse (tfrom), sizefrom),
+ loc);
+ }
+
+ constraintTerm_setValue (ct, newval);
+ }
+
+ DPRINTF (("After div: %s", constraintExpr_unparse (e)));
return e;
}
-static /*@only@*/ constraintExpr constraintTerm_simpleDivTypeExprNode(/*@only@*/ constraintExpr e, ctype ct)
+
+/*@access exprNode@*/
+static /*@only@*/ constraintExpr
+constraintTerm_simpleDivTypeExprNode (/*@only@*/ constraintExpr e, ctype tfrom, ctype tto, fileloc loc)
{
exprData data;
exprNode t1, t2, expr;
lltok tok;
constraintTerm t;
- DPRINTF((
- message("constraintTerm_simpleDivTypeExprNode e=%s, ct=%s",
- constraintExpr_print(e), ctype_unparse(ct)
- )
- ));
+ llassert (constraintExpr_isDefined(e) );
+
+ DPRINTF (("constraintTerm_simpleDivTypeExprNode e=%s [%s => %s]", constraintExpr_print(e),
+ ctype_unparse(tfrom), ctype_unparse (tto)));
- t = constraintExprData_termGetTerm(e->data);
+ t = constraintExprData_termGetTerm (e->data);
- expr = constraintTerm_getExprNode(t);
+ expr = constraintTerm_getExprNode (t);
+
+ llassert (constraintExpr_isDefined(e));
+ llassert (exprNode_isDefined(expr));
if (expr->kind == XPR_OP)
{
t1 = exprData_getOpA (data);
t2 = exprData_getOpB (data);
tok = exprData_getOpTok (data);
- if (lltok_isMult(tok) )
+
+ if (lltok_isMult (tok))
{
+ /*
+ ** If the sizeof is first, flip them.
+ */
+
+ llassert (exprNode_isDefined(t1) && exprNode_isDefined(t2));
+
+ if (t2->kind == XPR_SIZEOF || t2->kind == XPR_SIZEOFT)
+ {
+ exprNode tmp = t1;
+ t1 = t2;
+ t2 = tmp;
+ }
+
+ /*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) )
+ if (t1->kind == XPR_SIZEOF || t1->kind == XPR_SIZEOFT)
{
- ctype ct2;
+ ctype multype;
if (t1->kind == XPR_SIZEOFT)
{
- ct2 = qtype_getType (exprData_getType (t1->edata));
+ multype = qtype_getType (exprData_getType (t1->edata));
}
else
{
- ct2 = qtype_getType (exprData_getType(exprData_getSingle (t1->edata)->edata ) );
+ exprNode tempE = exprData_getSingle (t1->edata);
+ multype = exprNode_getType (tempE);
}
- if (ctype_match (ctype_makePointer(ct2), ct) )
+
+ DPRINTF (("Here we go sizeof: %s / %s / %s",
+ ctype_unparse (multype), ctype_unparse (tfrom), ctype_unparse (tto)));
+ llassert (ctype_isPointer (tfrom));
+
+ if (ctype_almostEqual (ctype_makePointer (multype), tto))
{
/* 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));
+ constraintExpr_free (e);
+ DPRINTF (("Sizeof types match okay!"));
+ return constraintExpr_makeExprNode (t2);
}
else
{
- ct2 = qtype_getType (exprData_getType(exprData_getSingle (t2->edata)->edata ) );
- }
- if (ctype_match (ctype_makePointer(ct2),ct) )
- {
- /* sloopy way to do this... */ /*@i22*/
- constraintExpr_free(e);
- return constraintExpr_makeExprNode(t1);
+ int sizemul = ctype_getSize (multype);
+ ctype tobase = ctype_baseArrayPtr (tto);
+ int sizeto = ctype_getSize (tobase);
+
+ DPRINTF (("Types: %s / %s / %s",
+ ctype_unparse (tfrom), ctype_unparse (tto), ctype_unparse (multype)));
+
+ voptgenerror (FLG_ALLOCMISMATCH,
+ message ("Allocated memory is used as a different type (%s) from the sizeof type (%s)",
+ ctype_unparse (tobase), ctype_unparse (multype)),
+ loc);
+
+ if (sizemul == sizeto)
+ {
+ constraintExpr_free (e);
+ DPRINTF (("Sizeof types match okay!"));
+ return constraintExpr_makeExprNode (t2);
+ }
+ else
+ {
+ /* nothing was here */
+ DPRINTF (("MISMATCHING TYPES!"));
+ return (constraintExpr_div (constraintExpr_makeExprNode (t2), multype, tto, loc));
+ }
}
}
else
{
- /*empty*/
+ DPRINTF (("NOT A SIZEOF!"));
+ /* empty */
}
-
+ }
+ else
+ {
+ DPRINTF (("Not a mult: %s", constraintExpr_unparse (e)));
}
}
- return (constraintExpr_div (e, ct) );
+
+ return (constraintExpr_div (e, tfrom, tto, loc));
}
+/*@noaccess exprNode@*/
-static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype ct)
+static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype tfrom, ctype tto, fileloc loc)
{
- /*@i333*/
- DPRINTF(( (message("simpleDiv got %s ", constraintExpr_unparse(e) ) )
- ));
+ DPRINTF (("simpleDiv got %s", constraintExpr_unparse(e)));
+ DPRINTF (("Types: %s / %s",
+ ctype_unparse (tfrom),
+ ctype_unparse (tto)));
+ llassert (constraintExpr_isDefined(e));
+
switch (e->kind)
{
case term:
-
{
- constraintTerm t;
+ constraintTerm t = constraintExprData_termGetTerm (e->data);
- t = constraintExprData_termGetTerm(e->data);
-
+ DPRINTF (("Term: %s", constraintTerm_unparse (t)));
- if (constraintTerm_isExprNode (t) )
- {
- return constraintTerm_simpleDivTypeExprNode(e, ct);
-
- /* search for * size of ct and remove */
- }
- return constraintExpr_div (e, ct);
+ if (constraintTerm_isExprNode (t))
+ {
+ return constraintTerm_simpleDivTypeExprNode (e, tfrom, tto, loc);
+
+ /* search for * size of ct and remove */
+ }
+ DPRINTF (("Here: %s / %s -> %s", constraintExpr_unparse (e), ctype_unparse (tfrom), ctype_unparse (tto)));
+ return constraintExpr_div (e, tfrom, tto, loc);
}
case binaryexpr:
temp = constraintExprData_binaryExprGetExpr1 (e->data);
temp = constraintExpr_copy(temp);
- temp = simpleDivType (temp, ct);
+ temp = simpleDivType (temp, tfrom, tto, loc);
e->data = constraintExprData_binaryExprSetExpr1 (e->data, temp);
temp = constraintExprData_binaryExprGetExpr2 (e->data);
temp = constraintExpr_copy(temp);
- temp = simpleDivType (temp, ct);
+ temp = simpleDivType (temp, tfrom, tto, loc);
e->data = constraintExprData_binaryExprSetExpr2 (e->data, temp);
- DPRINTF(( (message("simpleDiv binaryexpr returning %s ", constraintExpr_unparse(e) ) )
- ));
-
+ DPRINTF (("simpleDiv binaryexpr returning %s ", constraintExpr_unparse(e)));
return e;
}
case unaryExpr:
- return constraintExpr_div (e, ct);
+ {
+ return constraintExpr_div (e, tfrom, tto, loc);
+ }
default:
BADEXIT;
}
}
-static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr e, ctype ct)
+static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast (/*@only@*/ constraintExpr e, ctype tfrom,
+ ctype tto, fileloc loc)
{
-
- DPRINTF(( (message("constraintExpr_adjustMaxSetForCast got %s ", constraintExpr_unparse(e) ) )
- ));
-
- e = constraintExpr_makeIncConstraintExpr(e);
+ DPRINTF (("constraintExpr_adjustMaxSetForCast got %s [%s => %s]", constraintExpr_unparse(e),
+ ctype_unparse (tfrom), ctype_unparse (tto)));
- e = constraintExpr_simplify(e);
+ e = constraintExpr_makeIncConstraintExpr (e);
+ e = constraintExpr_simplify (e);
+ e = simpleDivType (e, tfrom, tto, loc);
+ e = constraintExpr_makeDecConstraintExpr (e);
+ e = constraintExpr_simplify (e);
+ DPRINTF (("constraintExpr_adjustMaxSetForCast returning %s ", constraintExpr_unparse(e)));
+ return e;
+}
- e = simpleDivType (e, ct);
- e = constraintExpr_makeDecConstraintExpr(e);
-
- e = constraintExpr_simplify(e);
-
- DPRINTF(( (message("constraintExpr_adjustMaxSetForCast returning %s ", constraintExpr_unparse(e) ) )
- ));
+bool constraintExpr_isConstantOnly (constraintExpr e)
+{
+ DPRINTF (("constraintExpr_isConstantOnly %s ", constraintExpr_unparse(e)));
+ llassert (constraintExpr_isDefined(e));
- return e;
+ switch (e->kind)
+ {
+ case term:
+ {
+ constraintTerm t = constraintExprData_termGetTerm(e->data);
+
+ if (constraintTerm_isConstantOnly (t))
+ {
+ return TRUE;
+ }
+ else
+ {
+ return FALSE;
+ }
+ }
+
+ case binaryexpr:
+ {
+ constraintExpr temp1 = constraintExprData_binaryExprGetExpr1 (e->data);
+ constraintExpr 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