/*
** 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) /*@*/;
static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr p_e, ctype p_ct);
-/*@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;
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();
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;
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)
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)
)));
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;
/* 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);
if (context_getFlag (FLG_PARENCONSTRAINT) )
{
- st = message ("(%q) ", constraintTerm_print (constraintExprData_termGetTerm (ex->data)));
+ st = message ("(%q) ", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
}
else
{
- st = message ("%q", constraintTerm_print (constraintExprData_termGetTerm (ex->data)));
+ st = message ("%q", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
}
break;
case unaryExpr:
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:
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;
- 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)
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) /*@*/
{
+ if (constraintExpr_isUndefined(e) )
+ return FALSE;
+
if (e->kind == term)
{
return TRUE;
ctype constraintExpr_getCType (constraintExpr e) /*@*/
{
constraintTerm t;
-
+
+ llassert(constraintExpr_isDefined(e) );
+
llassert(constraintExpr_canGetCType(e) );
switch (e->kind)
static bool constraintExpr_hasTypeChange(constraintExpr e)
{
+ llassert(constraintExpr_isDefined(e) );
if (constraintExpr_isDefined((e)) && (e->ct == TRUE) )
{
return TRUE;
static ctype constraintExpr_getOrigType (constraintExpr e)
{
+ llassert(constraintExpr_isDefined(e) );
llassert(constraintExpr_hasTypeChange(e) );
return e;
}
+
+/*@access exprNode@*/
static /*@only@*/ constraintExpr constraintTerm_simpleDivTypeExprNode(/*@only@*/ constraintExpr e, ctype ct)
{
exprData data;
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)
{
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) )
{
}
else
{
- ct2 = qtype_getType (exprData_getType(exprData_getSingle (t2->edata)->edata ) );
+ 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) )
{
}
return (constraintExpr_div (e, ct) );
}
+/*@noaccess exprNode@*/
static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype ct)
{
DPRINTF(( (message("simpleDiv got %s ", constraintExpr_unparse(e) ) )
));
+ llassert(constraintExpr_isDefined(e) );
+
switch (e->kind)
{
case term:
constraintExpr_unparse(e) ) )
));
+ llassert(constraintExpr_isDefined(e) );
+
switch (e->kind)
{
case term:
andersk / splint.git / blobdiff