static /*@exposed@*/ exprNode
exprNode_lastStatement (/*@returned@*/ exprNode p_e);
-static /*@null@*/ sRef defref = sRef_undefined;
-static /*@only@*/ exprNode mustExitNode = exprNode_undefined;
+static /*@only@*/ exprNode s_mustExitNode = exprNode_undefined;
static int checkArgsReal (uentry p_fcn, /*@dependent@*/ exprNode p_f,
uentryList p_cl,
ctypeType = ctype_unknown;
filelocType = ctype_unknown;
- defref = sRef_undefined;
-
if (usymtab_existsType (cstring_makeLiteralTemp ("cstring")))
{
cstringType = usymtab_lookupAbstractType (cstring_makeLiteralTemp ("cstring"));
void
exprNode_destroyMod (void)
/*@globals killed regArg, killed outArg, killed outStringArg,
- killed mustExitNode, initMod @*/
+ killed s_mustExitNode, initMod @*/
{
if (initMod)
{
uentry_free (outArg);
uentry_free (outStringArg);
- exprNode_free (mustExitNode);
+ exprNode_free (s_mustExitNode);
initMod = FALSE;
/*@-branchstate@*/
}
static void exprNode_resetSref (/*@notnull@*/ exprNode e)
{
- e->sref = defref;
+ e->sref = sRef_undefined;
}
exprNode exprNode_fakeCopy (exprNode e)
e->typ = c;
e->kind = XPR_EMPTY;
e->val = multiVal_undefined;
- e->sref = defref;
+ e->sref = sRef_undefined;
e->etext = cstring_undefined;
e->loc = fileloc_undefined;
e->guards = guardSet_undefined;
/*@observer@*/ exprNode exprNode_makeMustExit (void)
{
- if (exprNode_isUndefined (mustExitNode))
+ if (exprNode_isUndefined (s_mustExitNode))
{
- mustExitNode = exprNode_createPlain (ctype_unknown);
- mustExitNode->exitCode = XK_MUSTEXIT;
+ s_mustExitNode = exprNode_createPlain (ctype_unknown);
+ s_mustExitNode->exitCode = XK_MUSTEXIT;
}
- return mustExitNode;
+ return s_mustExitNode;
}
}
ret->kind = XPR_EMPTY;
- ret->sref = defref;
+ ret->sref = sRef_undefined;
ret->etext = cstring_undefined;
ret->exitCode = XK_NEVERESCAPE;
ret->canBreak = FALSE;
ret->val = multiVal_undefined;
ret->kind = XPR_EMPTY;
- ret->sref = defref;
+ ret->sref = sRef_undefined;
ret->etext = cstring_undefined;
ret->exitCode = XK_NEVERESCAPE;
ret->canBreak = FALSE;
ret->msets = sRefSet_undefined;
ret->kind = XPR_EMPTY;
- ret->sref = defref;
+ ret->sref = sRef_undefined;
ret->etext = cstring_undefined;
ret->exitCode = XK_NEVERESCAPE;
ret->canBreak = FALSE;
}
e->loc = loc; /* save loc was mangled */
- e->sref = defref;
+ e->sref = sRef_undefined;
if (usymtab_exists (c))
{
e->canBreak = FALSE;
e->mustBreak = FALSE;
- exprNode_defineConstraints(e);
-
+ exprNode_defineConstraints (e);
return e;
}
else
}
else
{
- /* a->sref = defref; */
+ /* a->sref = sRef_undefined; */
}
}
}
}
else
{
- ret->sref = defref;
+ ret->sref = sRef_undefined;
exprNode_checkSetAny (ret, uentry_rawName (le));
}
ret->kind = XPR_CAST;
ret->edata = exprData_makeCast (tok, e, q);
- if (ctype_isRealSU (ctype_getBaseType (sRef_getType (e->sref))))
+ ret->sref = sRef_copy (e->sref);
+
+ if (!sRef_isConst (e->sref))
{
- /*
- ** This is a bit of a hack to avoid a problem
- ** when the code does,
- ** (some other struct) x
- ** ...
- ** x->field
- */
-
- ret->sref = sRef_copy (e->sref);
usymtab_addForceMustAlias (ret->sref, e->sref);
- sRef_setTypeFull (ret->sref, c);
- DPRINTF (("Cast: %s -> %s", sRef_unparseFull (e->sref),
- sRef_unparseFull (ret->sref)));
- }
- else
- {
- ret->sref = e->sref;
- sRef_setTypeFull (ret->sref, c);
- DPRINTF (("Cast 2: -> %s", sRef_unparseFull (ret->sref)));
}
+
+ sRef_setTypeFull (ret->sref, c);
+ DPRINTF (("Cast 2: -> %s", sRef_unparseFull (ret->sref)));
/*
** we allow
exprData_free (ret->edata, ret->kind);
ret->edata = exprData_undefined;
-
ret->exitCode = XK_NEVERESCAPE;
ret->mustBreak = FALSE;
ret->kind = XPR_INIT;
uentry ue = usymtab_lookup (idDecl_observeId (t));
exprNode ret = exprNode_makeInitializationAux (t);
fileloc loc = exprNode_loc (e);
-
+
+ DPRINTF (("initialization: %s = %s", idDecl_unparse (t), exprNode_unparse (e)));
+
if (exprNode_isError (e))
{
e = exprNode_createUnknown ();
- idDecl_free (t);
-
/* error: assume initializer is defined */
sRef_setDefined (ret->sref, g_currentloc);
+ ret->edata = exprData_makeInit (t, e);
}
else
{
exprData_free (ret->edata, ret->kind);
ret->edata = exprData_makeInit (t, e);
+ DPRINTF (("ret: %s", exprNode_unparse (ret)));
exprNode_checkUse (ret, e->sref, e->loc);
{
sRef_setDefState (ret->sref, SS_PARTIAL, fileloc_undefined);
}
+# if 0
+ if (exprNode_isStringLiteral (e)
+ && (ctype_isArray (ct))
+ && (ctype_isChar (ctype_realType (ctype_baseArrayPtr (ct)))))
+ {
+ /*
+ ** If t is a char [], the literal is copied.
+ */
+
+ cstring slit;
- doAssign (ret, e, TRUE);
+ if (multiVal_isDefined (e->val))
+ {
+ slit = multiVal_forceString (e->val);
+ }
+ else
+ {
+ slit = cstring_undefined;
+ }
+
+ sRef_setDefState (ret->sref, SS_DEFINED, e->loc);
+ ret->val = multiVal_copy (e->val);
+
+ if (cstring_isDefined (slit))
+ {
+ if (ctype_isFixedArray (ct))
+ {
+ long int alength = ctype_getArraySize (ct);
+
+ if (alength < cstring_length (slit) + 1)
+ {
+ voptgenerror
+ (FLG_LITERALOVERSIZE,
+ ("Array initialized to string literal bigger than allocated size (literal is %d chars long (plus one for nul terminator), array size is %d): %s",
+ cstring_length (slit),
+ alength,
+ exprNode_unparse (e)),
+ e->loc);
+ }
+ else if (alength > cstring_length (slit))
+ {
+ voptgenerror
+ (FLG_LITERALUNDERSIZE,
+ ("Array initialized to string literal smaller than allocated size (literal is %d chars long (plus one for nul terminator), array size is %d), could waste storage: %s",
+ cstring_length (slit),
+ alength,
+ exprNode_unparse (e)),
+ e->loc);
+ }
+ else
+ {
+ ;
+ }
+ }
+ else
+ {
+ sRef_setNullTerminatedState (ret->sref);
+ sRef_setSize (ret->sref, cstring_length (slit) + 1);
+ sRef_setLen (ret->sref, cstring_length (slit) + 1);
+ }
+ }
+ }
+ else
+# endif
+ {
+ doAssign (ret, e, TRUE);
+ }
if (uentry_isStatic (ue))
{
sRef_setDefState (ret->sref, SS_DEFINED, fileloc_undefined);
}
}
-
+
if (context_inIterDef ())
{
/* should check if it is yield */
}
exprNode_mergeUSs (ret, e);
+ DPRINTF (("Ret: %s %p %p",
+ exprNode_unparse (ret),
+ ret->requiresConstraints,
+ ret->ensuresConstraints));
+
+ DPRINTF (("Ret: %s %s %s",
+ exprNode_unparse (ret),
+ constraintList_unparse (ret->requiresConstraints),
+ constraintList_unparse (ret->ensuresConstraints)));
return ret;
}
e->kind = XPR_VAR;
e->val = multiVal_unknown ();
e->guards = guardSet_new ();
- e->sref = defref;
+ e->sref = sRef_undefined;
e->isJumpPoint = FALSE;
e->exitCode = XK_NEVERESCAPE;
{
if (exprNode_isDefined (e))
{
- /*@access sRef@*/
- if (e->sref == defref) /*@noaccess sRef@*/
+ if (sRef_isInvalid (e->sref))
{
/*@-mods@*/
e->sref = sRef_makeUnknown ();
andersk / splint.git / blobdiff