# 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! */
-
-/*@only@*/ /*@notnull@*/
-constraintExpr constraintExpr_makeIntLiteral (long i);
static ctype constraintExpr_getOrigType (constraintExpr p_e);
static bool constraintExpr_hasTypeChange(constraintExpr p_e) /*@*/;
constraintExpr_free(expr1);
constraintExpr_free(expr);
-
+
+ llassert (constraintExpr_isDefined(temp) );
return temp;
}
else
}
}
DPRINTF ((message ("After combine %s", constraintExpr_unparse(expr) ) ) );
- return expr;
+
+ llassert(constraintExpr_isDefined(expr) );
+ return expr;
}
/*@special@*/
return ret;
}
+/*@access exprNode@*/
constraintExpr constraintExpr_makeExprNode (exprNode e)
{
sRef s;
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_COMMA:
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);
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;
}
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) )
{
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:
{
constraintTerm t;
sRef s;
-
-
constraintExprData data;
constraintExprKind kind;
-
constraintExpr ret;
-
- llassert(constraintExpr_isDefined (e) );
+
+ llassert (constraintExpr_isDefined (e) );
data = e->data;
kind = e->kind;
-
- llassert(kind == term);
-
+
+ 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
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);
/*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) )
{
- /* sloopy way to do this... */ /*@i22*/
+ /*a bit of a sloopy way to do this but... */
constraintExpr_free(e);
return constraintExpr_makeExprNode(t1);
}
}
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:
constraintExpr_unparse(e) ) )
));
+ llassert(constraintExpr_isDefined(e) );
+
switch (e->kind)
{
case term:
andersk / splint.git / blobdiff