/*
** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2000 University of Virginia,
+** Copyright (C) 1994-2001 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
# include "cgrammar_tokens.h"
# include "exprChecks.h"
-# include "aliasChecks.h"
+# include "transferChecks.h"
# include "exprNodeSList.h"
-# include "exprData.i"
static bool exprNode_isEmptyStatement (exprNode p_e);
static /*@exposed@*/ exprNode exprNode_firstStatement (/*@returned@*/ exprNode p_e);
static bool exprNode_isFalseConstant (exprNode p_e) /*@*/ ;
static bool exprNode_isBlock (exprNode p_e);
static void checkGlobUse (uentry p_glob, bool p_isCall, /*@notnull@*/ exprNode p_e);
-static void exprNode_addUse (exprNode p_e, sRef p_s);
+static void exprNode_addUse (exprNode p_e, /*@exposed@*/ sRef p_s);
static bool exprNode_matchArgType (ctype p_ct, exprNode p_e);
- exprNode exprNode_fakeCopy (exprNode p_e) /*@*/ ;
+static exprNode exprNode_fakeCopy (exprNode p_e) /*@*/ ;
static exprNode exprNode_statementError (/*@only@*/ exprNode p_e, /*@only@*/ lltok p_t);
static bool exprNode_matchTypes (exprNode p_e1, exprNode p_e2);
static void checkUniqueParams (exprNode p_fcn,
static ctype checkNumerics (ctype p_tr1, ctype p_tr2, ctype p_te1, ctype p_te2,
/*@notnull@*/ exprNode p_e1, /*@notnull@*/ exprNode p_e2, lltok p_op);
static void doAssign (/*@notnull@*/ exprNode p_e1, /*@notnull@*/ exprNode p_e2, bool p_isInit);
-static void checkSafeUse (exprNode p_e, sRef p_s);
+static void checkSafeUse (exprNode p_e, /*@exposed@*/ sRef p_s);
static void reflectNullTest (/*@notnull@*/ exprNode p_e, bool p_isnull);
static void checkMacroParen (exprNode p_e);
static exprNodeSList exprNode_flatten (/*@dependent@*/ exprNode p_e);
static void exprNode_checkSetAny (exprNode p_e, /*@dependent@*/ cstring p_name);
-static void exprNode_checkUse (exprNode p_e, sRef p_s, fileloc p_loc);
+static void exprNode_checkUse (exprNode p_e, /*@exposed@*/ sRef p_s, fileloc p_loc);
static void exprNode_mergeUSs (exprNode p_res, exprNode p_other);
static void exprNode_mergeCondUSs (exprNode p_res, exprNode p_other1, exprNode p_other2);
static /*@only@*/ /*@notnull@*/ exprNode exprNode_fromIdentifierAux (/*@observer@*/ uentry p_c);
static ctype filelocType;
static bool initMod = FALSE;
+static void exprNode_defineConstraints(/*@sef@*/ /*@special@*/ /*@notnull@*/ exprNode e)
+ /*@defines e->requiresConstraints, e->ensuresConstraints,
+ e->trueEnsuresConstraints, e->falseEnsuresConstraints @*/
+{
+ e->requiresConstraints = constraintList_makeNew ();
+ e->ensuresConstraints = constraintList_makeNew ();
+ e->trueEnsuresConstraints = constraintList_makeNew ();
+ e->falseEnsuresConstraints = constraintList_makeNew ();
+}
+
/*
** must occur after library has been read
*/
e->sref = defref;
}
+exprNode exprNode_fakeCopy (exprNode e)
+{
+ /*@-temptrans@*/ /*@-retalias@*/
+ return e;
+ /*@=temptrans@*/ /*@=retalias@*/
+}
+
static bool isFlagKey (char key)
{
return (key == '-' || key == '+' || key == ' ' || key == '#');
switch (e->kind)
{
case XPR_FACCESS:
+ /*
+ ** Its a fake copy, don't free the field->rec and field->field
+ ** fields.
+ */
+
+ /*@-compdestroy@*/
sfree (e->edata->field);
+ /*@=compdestroy@*/
+
sfree (e->edata);
break;
case XPR_FETCH:
sRefSet_free (e->sets);
sRefSet_free (e->msets);
guardSet_free (e->guards);
+
+ constraintList_free(e->requiresConstraints);
+ constraintList_free(e->ensuresConstraints);
+ constraintList_free(e->trueEnsuresConstraints);
+ constraintList_free(e->falseEnsuresConstraints);
+
+ e->requiresConstraints = NULL;
+ e->ensuresConstraints = NULL;
+ e->trueEnsuresConstraints = NULL;
+ e->falseEnsuresConstraints = NULL;
+
sfree (e);
}
}
guardSet_free (e->guards);
exprData_free (e->edata, e->kind);
+ constraintList_free(e->requiresConstraints);
+ constraintList_free(e->ensuresConstraints);
+ constraintList_free(e->trueEnsuresConstraints);
+ constraintList_free(e->falseEnsuresConstraints);
+
+ e->requiresConstraints = NULL;
+ e->ensuresConstraints = NULL;
+ e->trueEnsuresConstraints = NULL;
+ e->falseEnsuresConstraints = NULL;
+
nowalloc--;
sfree (e);
/*@-branchstate@*/
static /*@notnull@*/ /*@special@*/ exprNode
exprNode_createPlain (ctype c)
/*@defines result@*/
- /*@post:isnull result->edata, result->loc, result->val, result->guards,
- result->uses, result->sets, result->msets, result->etext @*/
+ /*@ensures isnull result->edata, result->loc, result->val, result->guards,
+ result->uses, result->sets, result->msets, result->etext @*/
/*@*/
{
exprNode e = exprNode_new ();
e->canBreak = FALSE;
e->mustBreak = FALSE;
e->isJumpPoint = FALSE;
- e->environment = environmentTable_undefined;
- e->requiresConstraints = constraintList_new();
- e->ensuresConstraints = constraintList_new();
-
+
+ exprNode_defineConstraints(e);
+
return (e);
}
ret->isJumpPoint = FALSE;
ret->edata = exprData_undefined;
+ exprNode_defineConstraints(ret);
+
return (ret);
}
ret->isJumpPoint = FALSE;
ret->edata = exprData_undefined;
+ exprNode_defineConstraints(ret);
+
return (ret);
}
ret->isJumpPoint = FALSE;
ret->edata = exprData_undefined;
+ exprNode_defineConstraints(ret);
+
return (ret);
}
}
}
/*@only@*/ exprNode
-exprNode_stringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc)
+exprNode_combineLiterals (exprNode e, exprNode rest)
+{
+ cstring ns;
+
+ /* Both must be string literals. */
+
+ if (exprNode_isUndefined (rest) || exprNode_isUndefined (e))
+ {
+ exprNode_free (rest);
+ return e;
+ }
+
+ if (!exprNode_isStringLiteral (e))
+ {
+ voptgenerror
+ (FLG_SYNTAX,
+ message ("Constant concatentation is ungrammatical: %s %s", exprNode_unparse (e),
+ exprNode_unparse (rest)),
+ e->loc);
+ exprNode_free (rest);
+ return e;
+ }
+
+ if (!exprNode_isStringLiteral (rest))
+ {
+ voptgenerror
+ (FLG_SYNTAX,
+ message ("Constant concatentation is ungrammatical: %s %s", exprNode_unparse (e), exprNode_unparse (rest)),
+ rest->loc);
+
+ exprNode_free (rest);
+ return e;
+ }
+
+ ns = cstring_concat (multiVal_forceString (exprNode_getValue (e)),
+ multiVal_forceString (exprNode_getValue (rest)));
+
+ multiVal_free (e->val);
+ exprData_free (e->edata, e->kind);
+ e->edata = exprData_makeLiteral (cstring_copy (ns));
+ e->val = multiVal_makeString (ns);
+ exprNode_free (rest);
+ return e;
+}
+
+/*@only@*/ exprNode
+exprNode_rawStringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc)
{
exprNode e = exprNode_createLoc (ctype_string, loc);
- int len = cstring_length (t) - 2;
- char *ts = cstring_toCharsSafe (t);
- char *s = cstring_toCharsSafe (cstring_create (len + 1));
+ int len = cstring_length (t);
if (context_getFlag (FLG_STRINGLITERALLEN))
{
voptgenerror (FLG_STRINGLITERALLEN,
message
("String literal length (%d) exceeds maximum "
- "length (%d): %s",
+ "length (%d): \"%s\"",
len,
context_getValue (FLG_STRINGLITERALLEN),
t),
}
}
- strncpy (s, ts+1, size_fromInt (len));
- *(s + len) = '\0';
-
-
e->kind = XPR_STRINGLITERAL;
- e->val = multiVal_makeString (cstring_fromCharsO (s));
+ e->val = multiVal_makeString (cstring_copy (t));
e->edata = exprData_makeLiteral (t);
e->sref = sRef_makeType (ctype_string);
- /* Start modifications */
- /* This expr is null terminated, so we set the len and size */
- sRef_setNullTerminatedState(e->sref);
- /*
- TPRINTF("Len is set to : %d\n\n", strlen((char *)multiVal_forceString(e->val)));
- TPRINTF("Size is set to : %d\n\n", strlen((char *)multiVal_forceString(e->val)));
- TPRINTF("State is set to: %d\n\n", e->sref->bufinfo.bufstate);
- */
- sRef_setLen(e->sref, strlen((char *)multiVal_forceString(e->val)));
- sRef_setSize(e->sref, strlen((char *)multiVal_forceString(e->val)));
if (context_getFlag (FLG_READONLYSTRINGS))
{
return (e); /* s released */
}
+/*@only@*/ exprNode
+exprNode_stringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc)
+{
+ int len = cstring_length (t) - 2;
+ char *ts = cstring_toCharsSafe (t);
+ char *s = cstring_toCharsSafe (cstring_create (len + 1));
+
+ llassert (*ts == '\"' && *(ts + len + 1) == '\"');
+ strncpy (s, ts+1, size_fromInt (len));
+ *(s + len) = '\0';
+ cstring_free (t);
+ return exprNode_rawStringLiteral (cstring_fromCharsO (s), loc);
+}
+
exprNode exprNode_fromUIO (cstring c)
{
fileloc loc = context_getSaveLocation ();
else
{
voptgenerror
- (FLG_UNRECOG, message ("Unrecognized identifier: %s", c),
- e->loc);
+ (FLG_UNRECOG, message ("Unrecognized identifier: %s", c), e->loc);
}
}
e->canBreak = FALSE;
e->mustBreak = FALSE;
+ exprNode_defineConstraints(e);
+
return e;
}
else
{
- return exprNode_createUnknown ();
+ return exprNode_createUnknown ();
}
}
uentry_setUsed (c, e->loc);
- if (uentry_isVar (c) && sRef_isGlobal (sr))
+ if (uentry_isVar (c) && sRef_isFileOrGlobalScope (sr))
{
checkGlobUse (c, FALSE, e);
}
}
else
{
- ret->sref = sRef_makeArrayFetch (arr->sref);
+ ret->sref = sRef_makeArrayFetch (arr->sref);
}
ret->sets = sRefSet_realNewUnion (arr->sets, ind->sets);
while ((code = strchr (code, '%')) != NULL)
{
char *origcode = code;
+ cstring codetext = cstring_newEmpty ();
char key = *(++code);
ctype modtype = ctype_int;
bool modified = FALSE;
fileloc_addColumn (formatloc, code - ocode);
+ codetext = cstring_appendChar (codetext, key);
+
/* ignore flags */
while (isFlagKey (key))
{
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
}
while (isdigit ((int) key) != 0)
{
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
}
if (key == '.')
{
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
/*
while (isdigit ((int) key) != 0)
{
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
}
}
{
modtype = ctype_sint; /* short */
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
}
else if (key == 'l' || key == 'L')
{
modtype = ctype_lint; /* long */
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
if (key == 'l' || key == 'L') {
modtype = ctype_llint; /* long long */
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
}
}
if (optgenerror
(FLG_TYPE,
message ("No argument corresponding to %q format "
- "code %d (%%%h): \"%s\"",
+ "code %d (%%%s): \"%s\"",
uentry_getName (fcn),
- i, key,
+ i, codetext,
cstring_fromChars (format)),
f->loc))
{
expecttype = ctype_combine (ctype_int, modtype);
/*@switchbreak@*/ break;
- case 'x': /* unsigned int */
+ case 'x': /* unsigned int */
case 'X':
- expecttype = ctype_combine (ctype_uint, modtype);
+ expecttype = ctype_combine (ctype_uint, modtype);
+
/*@switchbreak@*/ break;
case 'e':
while (((key = *(++code)) != ']')
&& (key != '\0'))
{
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
}
case 'p': /* pointer */
expecttype = ctype_makePointer (ctype_void);
- /* really! */
+ uentry_setDefState (regArg, SS_RELDEF); /* need not be defined */
+ sRef_setPosNull (uentry_getSref (regArg), fileloc_undefined); /* could be null */
/*@switchbreak@*/ break;
case 'n': /* pointer to int, modified by call! */
if (llgenformattypeerror
(expecttype, exprNode_undefined,
a->typ, a,
- message ("Format argument %d to %q (%%%h) expects "
+ message ("Format argument %d to %q (%%%s) expects "
"%t gets %t: %s",
i - argno,
uentry_getName (fcn),
- key, expecttype,
+ codetext,
+ expecttype,
a->typ, exprNode_unparse (a)),
a->loc))
{
uentry_setType (regArg, ctype_unknown);
uentry_fixupSref (regArg);
-
+
if (modified)
{
exprNode_checkCallModifyVal (a->sref, args, f, ret);
}
}
}
+
ocode = code;
+ cstring_free (codetext);
}
if (i < nargs)
{
voptgenerror (FLG_TYPE,
- message ("Format string for %q has %d arg%p, given %d",
+ message ("Format string for %q has %d arg%&, given %d",
uentry_getName (fcn), i - argno, nargs - argno),
f->loc);
}
else
{
/* no checking possible for compile-time unknown format strings */
+ if (exprNode_isDefined (a))
+ {
+ voptgenerror
+ (FLG_FORMATCONST,
+ message ("Format string parameter to %s is not a compile-time constant: %s",
+ exprNode_unparse (f),
+ exprNode_unparse (a)),
+ f->loc);
+ }
}
-
+
fileloc_free (formatloc);
}
{
char *origcode = code;
char key = *(++code);
+ cstring codetext = cstring_newEmpty ();
ctype modtype = ctype_int;
char modifier = '\0';
bool modified = TRUE;
bool ignore = FALSE;
+ codetext = cstring_appendChar (codetext, key);
fileloc_addColumn (formatloc, code - ocode);
/*
if (key == '*')
{
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
modified = FALSE;
ignore = TRUE;
fileloc_incColumn (formatloc);
while (isdigit ((int) key) != 0)
{
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
}
{
modtype = ctype_sint; /* short */
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
}
else if (key == 'l' || key == 'L')
modifier = key;
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
+
fileloc_incColumn (formatloc);
if (key == 'l' || key == 'L') {
modtype = ctype_llint; /* long long */
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
}
}
if (optgenerror
(FLG_TYPE,
message ("No argument corresponding to %q format "
- "code %d (%%%h): \"%s\"",
+ "code %d (%%%s): \"%s\"",
uentry_getName (fcn),
- i, key,
+ i, codetext,
cstring_fromChars (format)),
f->loc))
{
while (((key = *(++code)) != ']')
&& (key != '\0'))
{
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
}
expecttype = ctype_string;
/*@switchbreak@*/ break;
+
case 'p': /* pointer */
+ voptgenerror
+ (FLG_FORMATCODE,
+ message ("Format code should not be used in scanf: %s",
+ cstring_fromChars (origcode)),
+ fileloc_isDefined (formatloc)
+ ? formatloc : g_currentloc);
+
expecttype = ctype_unknown;
- /* really! */
/*@switchbreak@*/ break;
case 'n': /* pointer to int, modified by call! */
}
else
{
- if (modifier != '\0')
- {
- if (llgenformattypeerror
- (expecttype, exprNode_undefined,
- a->typ, a,
- message ("Format argument %d to %q (%%%h%h) expects "
- "%t gets %t: %s",
- i - argno,
- uentry_getName (fcn),
- modifier,
- key, expecttype,
- a->typ, exprNode_unparse (a)),
- a->loc))
- {
- if (fileloc_isDefined (formatloc)
- && context_getFlag (FLG_SHOWCOL))
- {
- llgenindentmsg
- (cstring_makeLiteral
- ("Corresponding format code"),
- formatloc);
- }
- }
-
- }
- else
+ if (llgenformattypeerror
+ (expecttype, exprNode_undefined,
+ a->typ, a,
+ message ("Format argument %d to %q (%%%s) expects "
+ "%t gets %t: %s",
+ i - argno,
+ uentry_getName (fcn),
+ codetext, expecttype,
+ a->typ, exprNode_unparse (a)),
+ a->loc))
{
- if (llgenformattypeerror
- (expecttype, exprNode_undefined,
- a->typ, a,
- message ("Format argument %d to %q (%%%h) expects "
- "%t gets %t: %s",
- i - argno,
- uentry_getName (fcn),
- key, expecttype,
- a->typ, exprNode_unparse (a)),
- a->loc))
+ if (fileloc_isDefined (formatloc)
+ && context_getFlag (FLG_SHOWCOL))
{
- if (fileloc_isDefined (formatloc)
- && context_getFlag (FLG_SHOWCOL))
- {
- llgenindentmsg
- (cstring_makeLiteral
- ("Corresponding format code"),
- formatloc);
- }
+ llgenindentmsg
+ (cstring_makeLiteral
+ ("Corresponding format code"),
+ formatloc);
}
}
}
}
}
}
+
ocode = code;
+ cstring_free (codetext);
}
if (i < nargs)
{
voptgenerror (FLG_TYPE,
- message ("Format string for %q has %d arg%p, given %d",
+ message ("Format string for %q has %d arg%&, given %d",
uentry_getName (fcn), i - argno, nargs - argno),
f->loc);
}
{
char *origcode = code;
char key = *(++code);
+ cstring codetext = cstring_newEmpty ();
bool isOnly = FALSE;
+ codetext = cstring_appendChar (codetext, key);
+
fileloc_addColumn (formatloc, code - ocode);
while (key >= '0' && key <= '9')
{
key = *(++code);
+ codetext = cstring_appendChar (codetext, key);
fileloc_incColumn (formatloc);
}
if (key != '%')
{
- if (key == 'p')
+ if (key == '&') /* plural marker */
{
goto nextKey;
}
{
voptgenerror
(FLG_TYPE,
- message ("Message missing format arg %d (%%%h): \"%s\"",
- i + 1, key, format),
+ message ("Message missing format arg %d (%%%s): \"%s\"",
+ i + 1, codetext, format),
f->loc);
i++;
}
case 'b': expecttype = ctype_bool; break;
case 't': expecttype = ctypeType; break;
case 'l': expecttype = filelocType; break;
- case 'p': /* a wee bit of a hack methinks */
+ case '&': /* a wee bit of a hack methinks */
expecttype = ctype_int;
break;
case 'r': expecttype = ctype_bool; break;
if (llgenformattypeerror
(expecttype, exprNode_undefined,
a->typ, a,
- message ("Format argument %d to %q (%%%h) expects "
+ message ("Format argument %d to %q (%%%s) expects "
"%t gets %t: %s",
i - argno,
uentry_getName (fcn),
- key, expecttype,
+ codetext, expecttype,
a->typ, exprNode_unparse (a)),
a->loc))
{
}
}
}
+
+ cstring_free (codetext);
}
if (i < nargs)
{
voptgenerror (FLG_TYPE,
- message ("Format string for %q has %d arg%p, given %d",
+ message ("Format string for %q has %d arg%&, given %d",
uentry_getName (fcn), i - argno, nargs -argno),
f->loc);
}
{
bool hadUncon = FALSE;
- if (sRef_isGlobal (sRef_getRootBase (e1->sref)) &&
+ if (sRef_isFileOrGlobalScope (sRef_getRootBase (e1->sref)) &&
sRefSet_hasUnconstrained (sets2))
{
voptgenerror
e2->loc);
}
- if (sRef_isGlobal (sRef_getRootBase (e2->sref)) &&
+ if (sRef_isFileOrGlobalScope (sRef_getRootBase (e2->sref)) &&
sRefSet_hasUnconstrained (sets1))
{
voptgenerror
{
sRefSet otheruses = jl->uses;
- if (sRef_isGlobal (sRef_getRootBase (jl->sref)) &&
+ if (sRef_isFileOrGlobalScope (sRef_getRootBase (jl->sref)) &&
sRefSet_hasUnconstrained (thissets))
{
voptgenerror
bool freshMods = FALSE;
uentryList params = uentryList_undefined;
+ DPRINTF (("Check glob mods: %s", exprNode_unparse (ret)));
+
/*
** check globals and modifies
*/
if (!context_getFlag (FLG_MODNOMODS)
&& !context_getFlag (FLG_GLOBUNSPEC))
{
- checkUnspecCall (f, params, args);
+ checkUnspecCall (f, params, args);
}
return;
uentry_unparse (le)));
params = ctype_argsFunction (ct);
+ return; /*@32 ! remove this? */
}
/*
*/
setCodePoint ();
-
globSet_allElements (usesGlobs, el)
{
sRefSet_allElements (mods, s) /* s is something which may be modified */
{
+ DPRINTF (("Check modify: %s", sRef_unparse (s)));
+
if (sRef_isKindSpecial (s))
{
if (sRef_isSpecInternalState (s))
{
sRef rb = sRef_getRootBase (s);
- if (sRef_isGlobal (rb))
+ if (sRef_isFileOrGlobalScope (rb))
{
context_usedGlobal (rb);
}
}
}
+static void
+reflectEnsuresClause (uentry le, exprNode f, exprNodeList args)
+{
+ DPRINTF (("Reflect ensures clause: %s(%s) / %s / %s",
+ exprNode_unparse (f), exprNodeList_unparse (args),
+ uentry_unparseFull (le),
+ stateClauseList_unparse (uentry_getStateClauseList (le))));
+
+ if (uentry_isValid (le) && uentry_isFunction (le))
+ {
+ stateClauseList sclauses = uentry_getStateClauseList (le);
+
+ if (stateClauseList_isDefined (sclauses))
+ {
+ DPRINTF (("Reflect ensures: %s / %s / %s",
+ uentry_unparse (le),
+ exprNode_unparse (f), exprNodeList_unparse (args)));
+
+ stateClauseList_elements (sclauses, cl)
+ {
+ if (stateClause_hasEnsures (cl))
+ {
+ /* Same in usymtab.c:1904 */
+ if (stateClause_setsMetaState (cl))
+ {
+ qual q = stateClause_getMetaQual (cl);
+ annotationInfo ainfo = qual_getAnnotationInfo (q);
+ metaStateInfo minfo = annotationInfo_getState (ainfo);
+ cstring key = metaStateInfo_getName (minfo);
+ int mvalue = annotationInfo_getValue (ainfo);
+
+ sRefSet osrs = sRefSet_undefined;
+ sRefSet srs;
+
+ if (stateClause_isGlobal (cl))
+ {
+ srs = sRefSet_single (usymtab_lookupGlobalMarker ());
+ osrs = srs;
+ }
+ else
+ {
+ srs = stateClause_getRefs (cl);
+ }
+
+ DPRINTF (("Reflect ensures clause: %s", stateClause_unparse (cl)));
+
+
+ DPRINTF (("Sets meta state! %s", stateClause_unparse (cl)));
+
+ sRefSet_elements (srs, sel)
+ {
+ sRef s;
+
+ if (sRef_isResult (sRef_getRootBase (sel)))
+ {
+ ; /*@i423 what do we do about results */
+ }
+ else
+ {
+ s = sRef_fixBaseParam (sel, args);
+ DPRINTF (("Reflecting state clause on: %s / %s",
+ sRef_unparse (sel), sRef_unparse (s)));
+
+ sRef_setMetaStateValueComplete (s, key, mvalue, exprNode_loc (f));
+ }
+ } end_sRefSet_elements;
+
+ sRefSet_free (osrs);
+ }
+ else
+ {
+ sRefSet srs = stateClause_getRefs (cl);
+ sRefModVal modf = stateClause_getEnsuresFunction (cl);
+ int eparam = stateClause_getStateParameter (cl);
+
+ DPRINTF (("Reflect after clause: %s / %s",
+ stateClause_unparse (cl),
+ sRefSet_unparse (srs)));
+
+ sRefSet_elements (srs, sel)
+ {
+ sRef s;
+
+ DPRINTF (("elements: %s", sRef_unparse (sel)));
+ DPRINTF (("elements: %s", sRef_unparseFull (sel)));
+
+ if (sRef_isResult (sRef_getRootBase (sel)))
+ {
+ ; /*@i423 what do we do about results */
+ }
+ else
+ {
+ s = sRef_fixBaseParam (sel, args);
+
+ DPRINTF (("elements: %s", sRef_unparse (s)));
+ DPRINTF (("elements: %s", sRef_unparseFull (s)));
+
+ DPRINTF (("Reflecting state clause on: %s / %s",
+ sRef_unparse (sel), sRef_unparse (s)));
+
+ modf (s, eparam, exprNode_loc (f));
+ }
+ } end_sRefSet_elements;
+ }
+ }
+ } end_stateClauseList_elements ;
+ }
+
+ DPRINTF (("Here: %s / %s",
+ uentry_unparseFull (le),
+ bool_unparse (uentry_hasMetaStateEnsures (le))));
+
+ if (uentry_hasMetaStateEnsures (le))
+ {
+ metaStateConstraint msc = uentry_getMetaStateEnsures (le);
+
+ TPRINTF (("Meta state constraint for %s: %s", uentry_unparse (le),
+ metaStateConstraint_unparse (msc)));
+
+ }
+ }
+}
+
+static void
+checkRequiresClause (uentry le, exprNode f, exprNodeList args)
+{
+ DPRINTF (("Check requires clause: %s(%s) / %s / %s",
+ exprNode_unparse (f), exprNodeList_unparse (args),
+ uentry_unparseFull (le),
+ stateClauseList_unparse (uentry_getStateClauseList (le))));
+
+ if (uentry_isValid (le) && uentry_isFunction (le))
+ {
+ stateClauseList sclauses = uentry_getStateClauseList (le);
+
+ if (stateClauseList_isDefined (sclauses))
+ {
+ DPRINTF (("Check requires: %s / %s / %s",
+ uentry_unparse (le),
+ exprNode_unparse (f), exprNodeList_unparse (args)));
+
+ stateClauseList_elements (sclauses, cl)
+ {
+ DPRINTF (("Check clause: %s / %s",
+ stateClause_unparse (cl),
+ bool_unparse (stateClause_hasRequires (cl))));
+
+ if (stateClause_hasRequires (cl))
+ {
+ sRefSet osrs = sRefSet_undefined;
+ sRefSet srs;
+
+ if (stateClause_isGlobal (cl))
+ {
+ srs = sRefSet_single (usymtab_lookupGlobalMarker ());
+ osrs = srs;
+ }
+ else
+ {
+ srs = stateClause_getRefs (cl);
+ }
+
+ DPRINTF (("Refs: %s", sRefSet_unparse (srs)));
+
+ if (stateClause_setsMetaState (cl))
+ {
+ qual q = stateClause_getMetaQual (cl);
+ annotationInfo ainfo = qual_getAnnotationInfo (q);
+ metaStateInfo minfo = annotationInfo_getState (ainfo);
+ cstring key = metaStateInfo_getName (minfo);
+ int mvalue = annotationInfo_getValue (ainfo);
+
+ DPRINTF (("Requires meta state! %s = %d", key, mvalue));
+
+ sRefSet_elements (srs, sel)
+ {
+ sRef s = sRef_fixBaseParam (sel, args);
+
+ if (sRef_isResult (sRef_getRootBase (sel)))
+ {
+ ; /*@i423 what do we do about results */
+ }
+ else
+ {
+ DPRINTF (("Checking state clause on: %s / %s / %s = %d",
+ sRef_unparseFull (sel), sRef_unparseFull (s),
+ key, mvalue));
+
+ if (!sRef_checkMetaStateValue (s, key, mvalue))
+ {
+ DPRINTF (("HERE: %s", sRef_unparse (s)));
+ if (optgenerror
+ (FLG_STATETRANSFER,
+ message
+ ("Requires clause of called function %q not satisfied%q (state is %q): %q",
+ uentry_getName (le),
+ sRef_isGlobalMarker (s)
+ ? message ("")
+ : message (" by %q", sRef_unparse (s)),
+ stateValue_unparseValue (sRef_getMetaStateValue (s, key),
+ minfo),
+ stateClause_unparse (cl)),
+ exprNode_loc (f)))
+ {
+ sRef_showAliasInfo (s);
+ }
+ else
+ {
+ DPRINTF (("Error supressed!"));
+ DPRINTF (("Loc: %s", fileloc_unparse (exprNode_loc (f))));
+ DPRINTF (("Context supress: %s",
+ bool_unparse (context_suppressFlagMsg (FLG_STATETRANSFER, exprNode_loc (f)))));
+ }
+ }
+ }
+ } end_sRefSet_elements;
+ }
+ else
+ {
+ sRefModVal modf = stateClause_getRequiresBodyFunction (cl);
+ int eparam = stateClause_getStateParameter (cl);
+
+ DPRINTF (("Reflect after clause: %s / %s",
+ stateClause_unparse (cl),
+ sRefSet_unparse (srs)));
+
+ sRefSet_elements (srs, sel)
+ {
+ sRef s;
+
+ DPRINTF (("elements: %s", sRef_unparse (sel)));
+ DPRINTF (("elements: %s", sRef_unparseFull (sel)));
+
+ s = sRef_fixBaseParam (sel, args);
+
+ DPRINTF (("elements: %s", sRef_unparse (s)));
+ DPRINTF (("elements: %s", sRef_unparseFull (s)));
+
+ if (sRef_isResult (sRef_getRootBase (sel)))
+ {
+ ; /*@i423 what do we do about results */
+ }
+ else
+ {
+ DPRINTF (("Reflecting state clause on: %s / %s",
+ sRef_unparse (sel), sRef_unparse (s)));
+
+ modf (s, eparam, exprNode_loc (f));
+ }
+ } end_sRefSet_elements;
+ }
+
+ sRefSet_free (osrs);
+ }
+ } end_stateClauseList_elements ;
+ }
+ }
+}
+
static /*@only@*/ exprNode
functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f,
ctype t, /*@keep@*/ exprNodeList args)
int special;
setCodePoint ();
-
- ret->typ = ctype_returnValue (t);
+
+ DPRINTF (("Call: %s %s",exprNode_unparse (f), exprNodeList_unparse (args)));
+
+ ret->typ = ctype_getReturnType (t);
ret->kind = XPR_CALL;
ret->edata = exprData_makeCall (f, args);
special = checkArgs (le, f, t, args, ret);
checkGlobMods (f, le, args, ret, special);
+ checkRequiresClause (le, f, args);
+ setCodePoint ();
+ DPRINTF (("Reflect: %s", uentry_unparseFull (le)));
+ reflectEnsuresClause (le, f, args);
setCodePoint ();
if (uentry_isValid (le)
/* f->typ is already set to the return type */
ret->sref = uentry_returnedRef (le, args);
+ DPRINTF (("Returned: %s / %s",
+ uentry_unparseFull (le),
+ sRef_unparseFull (ret->sref)));
if (uentry_isFunction (le) && exprNodeList_size (args) >= 1)
{
}
}
-exprNode
-exprNode_fieldAccess (/*@only@*/ exprNode s, /*@only@*/ cstring f)
+static exprNode
+exprNode_fieldAccessAux (/*@only@*/ exprNode s, /*@observer@*/ fileloc loc,
+ /*@only@*/ cstring f)
{
exprNode ret = exprNode_createPartialCopy (s);
{
ctype t = exprNode_getType (s);
ctype tr = ctype_realType (t);
-
+
checkMacroParen (s);
ret->edata = exprData_makeField (s, f);
-
+
if (ctype_isStructorUnion (tr))
{
uentry tf = uentryList_lookupField (ctype_getFields (tr), f);
voptgenerror (FLG_TYPE,
message ("Access non-existent field %s of %t: %s", f, t,
exprNode_unparse (ret)),
- s->loc);
-
+ loc);
+ /*! cstring_free (f); */ /* evans 2001-03-25 self-detect */
return (ret);
}
else
checkSafeUse (ret, s->sref);
ret->sref = sRef_makeField (s->sref, uentry_rawName (tf));
+ /*!? exprNode_free (s); */ /* evans 2001-03-25 self-detect */
return (ret);
}
}
(FLG_ABSTRACT,
message ("Access field of abstract type (%t): %s.%s",
t, exprNode_unparse (s), f),
- s->loc);
+ loc);
ret->typ = ctype_unknown;
}
else
message
("Access field of non-struct or union (%t): %s.%s",
t, exprNode_unparse (s), f),
- s->loc);
+ loc);
ret->typ = ctype_unknown;
}
else
{
cstring sn = cstring_copy (f);
-
+
checkSafeUse (ret, s->sref);
cstring_markOwned (sn);
ret->sref = sRef_makeField (s->sref, sn);
-
return (ret);
}
}
+
return (ret);
}
}
BADEXIT;
}
+exprNode
+exprNode_fieldAccess (/*@only@*/ exprNode s, /*@only@*/ lltok dot,
+ /*@only@*/ cstring f)
+{
+ exprNode res = exprNode_fieldAccessAux (s, lltok_getLoc (dot), f);
+ lltok_release (dot);
+ return res;
+}
+
exprNode
exprNode_addParens (/*@only@*/ lltok lpar, /*@only@*/ exprNode e)
{
return ret;
}
-exprNode
-exprNode_arrowAccess (/*@only@*/ exprNode s, /*@only@*/ cstring f)
+static exprNode
+exprNode_arrowAccessAux (/*@only@*/ exprNode s, /*@observer@*/ fileloc loc,
+ /*@only@*/ cstring f)
{
exprNode ret = exprNode_createPartialCopy (s);
ret->edata = exprData_makeField (s, f);
ret->kind = XPR_ARROW;
-
+
if (exprNode_isError (s))
{
return (ret);
}
else
{
- ctype t = exprNode_getType (s);
- ctype tr = ctype_realType (t);
-
- checkMacroParen (s);
-
- (void) ctype_fixArrayPtr (tr); /* REWRITE THIS */
-
- if (ctype_isRealPointer (tr))
- {
- ctype b = ctype_realType (ctype_baseArrayPtr (tr));
-
- if (ctype_isStructorUnion (b))
- {
- uentry fentry = uentryList_lookupField (ctype_getFields (b), f);
-
- if (sRef_isKnown (s->sref) && sRef_possiblyNull (s->sref))
- {
- if (!usymtab_isGuarded (s->sref) && !context_inProtectVars ())
- {
- if (optgenerror
- (FLG_NULLDEREF,
- message ("Arrow access from %s pointer%q: %s",
- sRef_nullMessage (s->sref),
- sRef_unparsePreOpt (s->sref),
- exprNode_unparse (ret)),
- s->loc))
- {
- sRef_showNullInfo (s->sref);
- sRef_setNullError (s->sref);
- }
- }
- }
-
- if (uentry_isUndefined (fentry))
- {
- voptgenerror
- (FLG_TYPE,
- message ("Access non-existent field %s of %t: %s",
- f, t, exprNode_unparse (ret)),
- s->loc);
- ret->typ = ctype_unknown;
-
- return (ret);
- }
- else
- {
- /*
- ** was safeUse: shouldn't be safe!
- **
- ** to do rec->field
- ** rec must be defined,
- ** *rec must be allocated
- ** rec->field need only be defined it if is an rvalue
- */
-
- uentry_setUsed (fentry, exprNode_loc (ret));
- ret->typ = uentry_getType (fentry);
-
- exprNode_checkUse (ret, s->sref, s->loc);
-
- /* exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc); */
- ret->sref = sRef_makeArrow (s->sref, uentry_rawName (fentry));
- return (ret);
- }
- }
- else /* Pointer to something that is not a struct or union*/
- {
- if (ctype_isRealAbstract (tr))
- {
- ctype xrt = ctype_forceRealType (tr);
-
- voptgenerror
- (FLG_ABSTRACT,
- message ("Arrow access field of abstract type (%t): %s->%s",
- t, exprNode_unparse (s), f),
- s->loc);
-
- /*
- ** Set the state correctly, as if the abstraction is broken.
- */
-
- if (ctype_isRealPointer (xrt) &&
- (b = ctype_realType (ctype_baseArrayPtr (xrt)),
- ctype_isStructorUnion (b)))
- {
- uentry fentry = uentryList_lookupField (ctype_getFields (b), f);
- ret->typ = uentry_getType (fentry);
- ret->sref = sRef_makeArrow (s->sref, uentry_rawName (fentry));
- }
- else
- {
- ret->typ = ctype_unknown;
- ret->sref = sRef_undefined;
- }
- }
- else /* not a struct, union or abstract */
- {
- if (ctype_isUnknown (tr)) {
- cstring sn = cstring_copy (f);
-
- DPRINTF (("Here: %s", exprNode_unparse (s)));
-
- exprNode_checkUse (ret, s->sref, s->loc);
- exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc);
-
- cstring_markOwned (sn);
- ret->sref = sRef_makeArrow (s->sref, sn);
-
- ret->kind = XPR_ARROW;
- return (ret);
- } else {
- voptgenerror
- (FLG_TYPE,
- message ("Arrow access field of non-struct or union "
- "pointer (%t): %s->%s",
- t, exprNode_unparse (s), f),
- s->loc);
-
- ret->typ = ctype_unknown;
- ret->sref = sRef_undefined;
- }
- }
- }
- }
- else /* its not a pointer */
- {
- if (!ctype_isUnknown (tr))
- {
- voptgenerror
- (FLG_TYPE,
- message ("Arrow access of non-pointer (%t): %s->%s",
- t, exprNode_unparse (s), f),
- s->loc);
-
- ret->typ = ctype_unknown;
- ret->sref = sRef_undefined;
- }
- else
- {
- cstring sn = cstring_copy (f);
-
- DPRINTF (("Here: %s", exprNode_unparse (s)));
-
- exprNode_checkUse (ret, s->sref, s->loc);
- exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc);
-
- cstring_markOwned (sn);
- ret->sref = sRef_makeArrow (s->sref, sn);
-
- ret->kind = XPR_ARROW;
- return (ret);
- }
- }
-
+ ctype t = exprNode_getType (s);
+ ctype tr = ctype_realType (t);
+
+ checkMacroParen (s);
+
+ (void) ctype_fixArrayPtr (tr); /* REWRITE THIS */
+
+ if (ctype_isRealPointer (tr))
+ {
+ ctype b = ctype_realType (ctype_baseArrayPtr (tr));
+
+ if (ctype_isStructorUnion (b))
+ {
+ uentry fentry = uentryList_lookupField (ctype_getFields (b), f);
+
+ if (sRef_isKnown (s->sref) && sRef_possiblyNull (s->sref))
+ {
+ if (!usymtab_isGuarded (s->sref) && !context_inProtectVars ())
+ {
+ if (optgenerror
+ (FLG_NULLDEREF,
+ message ("Arrow access from %s pointer%q: %s",
+ sRef_nullMessage (s->sref),
+ sRef_unparsePreOpt (s->sref),
+ exprNode_unparse (ret)),
+ loc))
+ {
+ sRef_showNullInfo (s->sref);
+ sRef_setNullError (s->sref);
+ }
+ }
+ }
+
+ if (uentry_isUndefined (fentry))
+ {
+ voptgenerror
+ (FLG_TYPE,
+ message ("Access non-existent field %s of %t: %s",
+ f, t, exprNode_unparse (ret)),
+ loc);
+ ret->typ = ctype_unknown;
+ return (ret);
+ }
+ else
+ {
+ /*
+ ** was safeUse: shouldn't be safe!
+ **
+ ** to do rec->field
+ ** rec must be defined,
+ ** *rec must be allocated
+ ** rec->field need only be defined it if is an rvalue
+ */
+
+ uentry_setUsed (fentry, exprNode_loc (ret));
+ ret->typ = uentry_getType (fentry);
+
+ exprNode_checkUse (ret, s->sref, s->loc);
+
+ /* exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc); */
+ ret->sref = sRef_makeArrow (s->sref, uentry_rawName (fentry));
+ return (ret);
+ }
+ }
+ else /* Pointer to something that is not a struct or union*/
+ {
+ if (ctype_isRealAbstract (tr))
+ {
+ ctype xrt = ctype_forceRealType (tr);
+
+ voptgenerror
+ (FLG_ABSTRACT,
+ message ("Arrow access field of abstract type (%t): %s->%s",
+ t, exprNode_unparse (s), f),
+ loc);
+
+ /*
+ ** Set the state correctly, as if the abstraction is broken.
+ */
+
+ if (ctype_isRealPointer (xrt) &&
+ (b = ctype_realType (ctype_baseArrayPtr (xrt)),
+ ctype_isStructorUnion (b)))
+ {
+ uentry fentry = uentryList_lookupField (ctype_getFields (b), f);
+ ret->typ = uentry_getType (fentry);
+ ret->sref = sRef_makeArrow (s->sref, uentry_rawName (fentry));
+ }
+ else
+ {
+ ret->typ = ctype_unknown;
+ ret->sref = sRef_undefined;
+ }
+ }
+ else /* not a struct, union or abstract */
+ {
+ if (ctype_isUnknown (tr)) {
+ cstring sn = cstring_copy (f);
+
+ DPRINTF (("Here: %s", exprNode_unparse (s)));
+
+ exprNode_checkUse (ret, s->sref, s->loc);
+ exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc);
+
+ cstring_markOwned (sn);
+ ret->sref = sRef_makeArrow (s->sref, sn);
+
+ ret->kind = XPR_ARROW;
+ return (ret);
+ } else {
+ voptgenerror
+ (FLG_TYPE,
+ message ("Arrow access field of non-struct or union "
+ "pointer (%t): %s->%s",
+ t, exprNode_unparse (s), f),
+ loc);
+
+ ret->typ = ctype_unknown;
+ ret->sref = sRef_undefined;
+ }
+ }
+ }
+ }
+ else /* its not a pointer */
+ {
+ if (!ctype_isUnknown (tr))
+ {
+ voptgenerror
+ (FLG_TYPE,
+ message ("Arrow access of non-pointer (%t): %s->%s",
+ t, exprNode_unparse (s), f),
+ loc);
+
+ ret->typ = ctype_unknown;
+ ret->sref = sRef_undefined;
+ }
+ else
+ {
+ cstring sn = cstring_copy (f);
+
+ DPRINTF (("Here: %s", exprNode_unparse (s)));
+
+ exprNode_checkUse (ret, s->sref, s->loc);
+ exprNode_checkUse (ret, sRef_makePointer (s->sref), s->loc);
+
+ cstring_markOwned (sn);
+ ret->sref = sRef_makeArrow (s->sref, sn);
+
+ ret->kind = XPR_ARROW;
+ return (ret);
+ }
+ }
+
return (ret);
}
BADEXIT;
}
+exprNode
+exprNode_arrowAccess (/*@only@*/ exprNode s,
+ /*@only@*/ lltok arrow,
+ /*@only@*/ cstring f)
+{
+ exprNode res = exprNode_arrowAccessAux (s, lltok_getLoc (arrow), f);
+ lltok_release (arrow);
+ return res;
+}
+
/*
** only postOp's in C: i++ and i--
*/
exprNode_checkModify (e, ret);
/* added 7/11/2000 D.L */
-
- updateEnvironmentForPostOp (e);
+ /*@i223*/
+ /*DRL 6/8/01 I decided to disable all LCLint Warning here since the code
+ probably needs a rewrite any way */
+
+ /*@ignore@*/
+
+ // updateEnvironmentForPostOp (e);
/* start modifications */
/* added by Seejo on 4/16/2000 */
}
}
}
-
+ /*@end@*/
/* end modifications */
return ret;
{
case INC_OP:
case DEC_OP: /* should also check modification! */
-
if (sRef_isMacroParamRef (e->sref))
{
voptgenerror
case TEXCL: /* maybe this should be restricted */
guardSet_flip (ret->guards);
- if (ctype_isRealBool (te))
+ if (ctype_isRealBool (te) || ctype_isUnknown (te))
{
;
}
{
ret->guards = guardSet_addFalseGuard (ret->guards, e->sref);
}
-
+
voptgenerror2n
(FLG_BOOLOPS, FLG_PTRNEGATE,
message ("Operand of %s is non-boolean (%t): %s",
}
else
{
+ DPRINTF (("No access to: %s / %d",
+ ctype_unparse (bc), ctype_typeId (bc)));
+ DPRINTF (("Context %s %s",
+ bool_unparse (context_inFunctionLike ()),
+ context_unparse ()));
voptgenerror
(FLG_ABSTRACT,
message ("Cast to abstract type %t: %s", bc,
default: {
llfatalbug
(cstring_makeLiteral
- ("There has been a problem in the parser. This is due to a bug "
- "in either lclint, bison or gcc version 2.95 optimizations, "
- "but it has not been confirmed. Please try rebuidling LCLint "
- "without the -O<n> option."));
+ ("There has been a problem in the parser. This is believed to result "
+ "from a problem with bison v. 1.25. Please try rebuidling LCLint "
+ "using the pre-compiled grammar files by commenting out the "
+ "BISON= line in the top-level Makefile."));
}
}
}
sRef_unparseFull (ref)));
if (sRef_isObserver (ref)
- || ((sRef_isFileStatic (ref) || sRef_isGlobal (ref))
+ || ((sRef_isFileStatic (ref) || sRef_isFileOrGlobalScope (ref))
&& ctype_isArray (ctype_realType (sRef_getType (ref)))))
{
sRef base = sRef_getBase (ref);
{
exprNode ret = exprNode_createPartialCopy (e1);
+ DPRINTF (("Concat: %s / %s", exprNode_unparse (e1), exprNode_unparse (e2)));
+
ret->edata = exprData_makePair (e1, e2);
ret->kind = XPR_STMTLIST;
}
exprNode_mergeUSs (ret, e2);
- ret = exprNode_mergeEnvironments (ret, e1, e2);
+
usymtab_setExitCode (ret->exitCode);
if (ret->mustBreak)
exprNode exprNode_createTok (/*@only@*/ lltok t)
{
- exprNode ret = exprNode_create (ctype_unknown);
+ exprNode ret; /*@i23 if on same line, bad things happen...!@*/
+ ret = exprNode_create (ctype_unknown);
ret->kind = XPR_TOK;
ret->edata = exprData_makeTok (t);
return ret;
{
exprNode ret;
bool emptyErr = FALSE;
- char *s;
- // s = exprNode_generateConstraints (t);
- // printf("pred: %s\n", s);
- // s = exprNode_generateConstraints (b);
- //printf ("body: %s\n", s);
- //constraintList_print(b->constraints);
if (context_maybeSet (FLG_WHILEEMPTY))
{
** forgot the copy's --- why wasn't this detected??
*/
- ret->sets = sRefSet_copy (ret->sets, b->sets);
- ret->msets = sRefSet_copy (ret->msets, b->msets);
- ret->uses = sRefSet_copy (ret->uses, b->uses);
+ ret->sets = sRefSet_copyInto (ret->sets, b->sets);
+ ret->msets = sRefSet_copyInto (ret->msets, b->msets);
+ ret->uses = sRefSet_copyInto (ret->uses, b->uses);
/* left this out --- causes and aliasing bug (infinite loop)
should be detected?? */
context_clearMessageAnnote ();
- ret->uses = sRefSet_copy (ret->uses, inc->uses);
- ret->sets = sRefSet_copy (ret->sets, inc->sets);
- ret->msets = sRefSet_copy (ret->msets, inc->msets);
+ ret->uses = sRefSet_copyInto (ret->uses, inc->uses);
+ ret->sets = sRefSet_copyInto (ret->sets, inc->sets);
+ ret->msets = sRefSet_copyInto (ret->msets, inc->msets);
}
}
hasError = optgenerror
(FLG_FULLINITBLOCK,
message ("Initializer block for "
- "%s has %d field%p, but %s has %d field%p: %q",
+ "%s has %d field%&, but %s has %d field%&: %q",
exprNode_unparse (el),
exprNodeList_size (vals),
ctype_unparse (t1),
hasError = optgenerror
(FLG_TYPE,
message ("Initializer block for "
- "%s has %d field%p, but %s has %d field%p: %q",
+ "%s has %d field%&, but %s has %d field%&: %q",
exprNode_unparse (el),
exprNodeList_size (vals),
ctype_unparse (t1),
{
uentry thisfield = uentryList_getN (fields, i);
exprNode newel =
- exprNode_fieldAccess (exprNode_fakeCopy (el),
- uentry_getName (thisfield));
+ exprNode_fieldAccessAux (exprNode_fakeCopy (el),
+ exprNode_loc (el),
+ uentry_getName (thisfield));
if (exprNode_isDefined (newel))
{
return hasError;
}
+static exprNode
+exprNode_makeInitializationAux (/*@temp@*/ idDecl t)
+{
+ exprNode ret;
+
+ if (usymtab_exists (idDecl_observeId (t)))
+ {
+ uentry ue = usymtab_lookup (idDecl_observeId (t));
+ ret = exprNode_createId (ue);
+
+ /*@i723 don't do this...but why? */
+# if 0
+ ct = ctype_realishType (ret->typ);
+
+ DPRINTF (("Type: %s", ctype_unparse (ret->typ)));
+
+ if (ctype_isUnknown (ct))
+ {
+ if (uentry_isAnyTag (ue))
+ {
+ voptgenerror
+ (FLG_IMPTYPE,
+ message ("%s used but not previously declared: %s",
+ uentry_ekindName (ue),
+ idDecl_getName (t)),
+ g_currentloc);
+
+ }
+ else
+ {
+ voptgenerror
+ (FLG_IMPTYPE,
+ message ("Variable has unknown (implicitly int) type: %s",
+ idDecl_getName (t)),
+ g_currentloc);
+ }
+
+ ct = ctype_int;
+ }
+# endif
+ }
+ else
+ {
+ uentry ue = uentry_makeUnrecognized (idDecl_observeId (t),
+ g_currentloc);
+ ret = exprNode_fromIdentifierAux (ue);
+
+ /*
+ ** No error - this happens in old style declarations:
+
+ voptgenerror
+ (FLG_UNRECOG,
+ message ("Unrecognized identifier in intializer: %s", idDecl_observeId (t)),
+ g_currentloc);
+
+ **
+ */
+ }
+
+ exprData_free (ret->edata, ret->kind);
+ ret->edata = exprData_undefined;
+ ret->exitCode = XK_NEVERESCAPE;
+ ret->mustBreak = FALSE;
+ ret->kind = XPR_INIT;
+ return ret;
+}
+
+exprNode exprNode_makeEmptyInitialization (/*@only@*/ idDecl t)
+{
+ exprNode ret = exprNode_makeInitializationAux (t);
+ llassert (ret->edata == exprData_undefined);
+ ret->edata = exprData_makeInit (t, exprNode_undefined);
+ return ret;
+}
+
exprNode exprNode_makeInitialization (/*@only@*/ idDecl t,
/*@only@*/ exprNode e)
{
uentry ue = usymtab_lookup (idDecl_observeId (t));
- bool isUsed = uentry_isUsed (ue);
- exprNode ret = exprNode_fromIdentifierAux (ue);
- ctype ct = ctype_realishType (ret->typ);
- fileloc loc;
-
- if (ctype_isUnknown (ct))
- {
- voptgenerror (FLG_IMPTYPE,
- message ("Variable has unknown (implicitly int) type: %s",
- idDecl_getName (t)),
- exprNode_isDefined (e) ? exprNode_loc (e) : g_currentloc);
-
- ct = ctype_int;
- }
+ exprNode ret = exprNode_makeInitializationAux (t);
+ fileloc loc = exprNode_loc (e);
if (exprNode_isError (e))
{
e = exprNode_createUnknown ();
- loc = g_currentloc;
+ idDecl_free (t);
/* error: assume initializer is defined */
- sRef_setDefined (ret->sref, loc);
+ sRef_setDefined (ret->sref, g_currentloc);
}
else
{
- loc = exprNode_loc (e);
-
+ ctype ct = ctype_realishType (ret->typ);
+
/*
** evs - 9 Apr 1995
**
** int x = 3, y = x ?
*/
+ exprData_free (ret->edata, ret->kind);
+ ret->edata = exprData_makeInit (t, e);
+
exprNode_checkUse (ret, e->sref, e->loc);
if (ctype_isUnknown (e->typ) && uentry_isValid (ue))
(void) gentypeerror
(exprNode_getType (e), e, exprNode_getType (ret), ret,
message
- ("Variable %s initialized to type %t, expects %t: %s",
- exprNode_unparse (ret), exprNode_getType (e),
+ ("Variable %q initialized to type %t, expects %t: %s",
+ uentry_getName (ue), exprNode_getType (e),
exprNode_getType (ret),
exprNode_unparse (e)),
e->loc);
}
else
{
- if (!isUsed) /* could be @unused@-qualified variable */
- {
- uentry_setNotUsed (ue);
- }
+ ;
}
- ret->exitCode = XK_NEVERESCAPE;
- ret->mustBreak = FALSE;
-
- /*
- ** Must be before new kind is assigned!
- */
-
- exprData_free (ret->edata, ret->kind);
-
- ret->kind = XPR_INIT;
- ret->edata = exprData_makeInit (t, e);
exprNode_mergeUSs (ret, e);
return ret;
}
cstring_free (s);
+
+ exprNode_defineConstraints(e);
return (e);
}
}
/*@observer@*/ cstring
-exprNode_unparse (exprNode e)
+exprNode_unparse (/*@temp@*/ exprNode e)
{
if (exprNode_isError (e))
{
break;
case XPR_FACCESS:
- ret = exprNode_fieldAccess (exprNode_effect (exprData_getFieldNode (data)),
- cstring_copy (exprData_getFieldName (data)));
+ ret = exprNode_fieldAccessAux
+ (exprNode_effect (exprData_getFieldNode (data)),
+ exprNode_loc (exprData_getFieldNode (data)),
+ cstring_copy (exprData_getFieldName (data)));
break;
case XPR_ARROW:
- ret = exprNode_arrowAccess (exprNode_effect (exprData_getFieldNode (data)),
- cstring_copy (exprData_getFieldName (data)));
+ ret = exprNode_arrowAccessAux
+ (exprNode_effect (exprData_getFieldNode (data)),
+ exprNode_loc (exprData_getFieldNode (data)),
+ cstring_copy (exprData_getFieldName (data)));
break;
case XPR_STRINGLITERAL:
return ret;
}
-
static /*@only@*/ cstring exprNode_doUnparse (exprNode e)
{
cstring ret;
break;
case XPR_INIT:
- ret = message ("%s = %s",
- idDecl_getName (exprData_getInitId (data)),
- exprNode_unparse (exprData_getInitNode (data)));
+ if (exprNode_isError (exprData_getInitNode (data)))
+ {
+ ret = message ("%q", idDecl_unparseC (exprData_getInitId (data)));
+ }
+ else
+ {
+ ret = message ("%q = %s",
+ idDecl_unparseC (exprData_getInitId (data)),
+ exprNode_unparse (exprData_getInitNode (data)));
+ }
break;
case XPR_FACCESS:
break;
case XPR_STRINGLITERAL:
- ret = cstring_copy (exprData_getLiteral (data));
+ ret = message ("\"%s\"", exprData_getLiteral (data));
break;
case XPR_NUMLIT:
return ret;
}
+bool
+exprNode_isInitializer (exprNode e)
+{
+ return (exprNode_isDefined (e)
+ && e->kind == XPR_INIT);
+}
+
bool
exprNode_isCharLit (exprNode e)
{
*/
static void
-exprNode_addUse (exprNode e, sRef s)
+exprNode_addUse (exprNode e, /*@exposed@*/ sRef s)
{
if (exprNode_isDefined (e))
{
}
void
-exprNode_checkUse (exprNode e, sRef s, fileloc loc)
+exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc)
{
if (sRef_isKnown (s) && !sRef_isConst (s))
{
DPRINTF (("Check use: %s / %s",
exprNode_unparse (e), sRef_unparse (s)));
-
+
exprNode_addUse (e, s);
if (!context_inProtectVars ())
{
ynm readable = sRef_isReadable (s);
+ DPRINTF (("Readable: %s / %s",
+ sRef_unparseFull (s), ynm_unparse (readable)));
+
if (!(ynm_toBoolStrict (readable)))
{
if (ynm_isMaybe (readable))
}
else
{
- DPRINTF (("HERE: %s", sRef_unparse (errorRef)));
+ DPRINTF (("HERE: %s", sRef_unparseFull (errorRef)));
voptgenerror
(FLG_USEDEF,
}
static void
-checkSafeUse (exprNode e, sRef s)
+checkSafeUse (exprNode e, /*@exposed@*/ sRef s)
{
if (exprNode_isDefined (e) && sRef_isKnown (s))
{
}
void
-exprNode_checkSet (exprNode e, sRef s)
+exprNode_checkSet (exprNode e, /*@exposed@*/ sRef s)
{
sRef defines = sRef_undefined;
}
void
-exprNode_checkMSet (exprNode e, sRef s)
+exprNode_checkMSet (exprNode e, /*@exposed@*/ sRef s)
{
if (sRef_isValid (s) && !sRef_isNothing (s))
{
if (specialArgs == 0
|| (paramno < specialArgs))
{
- checkOneArg (ucurrent, current, fcn, isSpec, paramno, nargs);
+ checkOneArg (ucurrent, current, fcn, isSpec, paramno, nargs);
if (context_maybeSet (FLG_ALIASUNIQUE))
{
sRef fb;
sRef rb = sRef_getRootBase (s);
- if (sRef_isGlobal (rb))
+ if (sRef_isFileOrGlobalScope (rb))
{
context_usedGlobal (rb);
}
sRef s2b)
{
if (!(sRef_isOnly (ysr) || sRef_isKeep (ysr)
- || sRef_isOwned (ysr) || sRef_isExposed (ysr)))
+ || sRef_isOwned (ysr)
+ || sRef_isExposed (ysr)))
{
- if (sRef_isAnyParam (base) && !sRef_isExposed (base))
+ if (sRef_isAnyParam (base) && !sRef_isExposed (base)
+ && !sRef_isObserver (base)) /* evans 2001-07-11: added isObserver */
+
{
if (sRef_isIReference (ysr))
{
}
}
- if (sRef_isGlobal (s2b))
+ if (sRef_isFileOrGlobalScope (s2b))
{
if (sRef_sameName (base, sRef_getRootBase (e2->sref)))
{
}
}
- if (sRef_isGlobal (s2b))
+ if (sRef_isFileOrGlobalScope (s2b))
{
voptgenerror
(FLG_ASSIGNEXPOSE,
{
if (isInit)
{
+ DPRINTF (("Check init: %s / %s",
+ exprNode_unparse (e1), exprNode_unparse (e2)));
checkInitTransfer (e1, e2);
}
else
}
}
- if (isInit && sRef_isGlobal (e1->sref))
+ if (isInit && sRef_isFileOrGlobalScope (e1->sref))
{
;
}
else
{
+ DPRINTF (("Update aliases: %s / %s", exprNode_unparse (e1), exprNode_unparse (e2)));
updateAliases (e1, e2);
}
- updateEnvironment (e1, e2);
}
static void
if (!ctype_isRealSU (t1))
{
+ DPRINTF (("Copying real! %s", ctype_unparse (t1)));
sRef_copyRealDerivedComplete (s1, s2);
}
+ else
+ {
+ /*
+ ** Fields should alias
+ */
+
+ DPRINTF (("Not COPYING!: %s", ctype_unparse (t1)));
+ }
if (ctype_isMutable (t1) && sRef_isKnown (s1))
{
usymtab_clearAlias (s1);
usymtab_addMustAlias (s1, s2);
+ DPRINTF (("Add must alias: %s / %s", sRef_unparse (s1), sRef_unparse (s2)));
+ }
+ else
+ {
+ DPRINTF (("Not mutable: %s", ctype_unparse (t1)));
}
if (sRef_possiblyNull (s1) && usymtab_isGuarded (s1))
return value;
}
-fileloc exprNode_getfileloc (exprNode p_e)
+/*@observer@*/ fileloc exprNode_getfileloc (exprNode p_e)
{
- if (p_e)
- return fileloc_copy ( p_e->loc );
+ if (exprNode_isDefined (p_e) )
+ return ( p_e->loc );
else
return fileloc_undefined;
}
-fileloc exprNode_getNextSequencePoint (exprNode e)
+/*@only@*/ fileloc exprNode_getNextSequencePoint (exprNode e)
{
/*
** Returns the location of the sequence point following e.
if (exprNode_isDefined (e) && e->kind == XPR_STMT) {
lltok t = exprData_getUopTok (e->edata);
- return lltok_getLoc (t);
+ return fileloc_copy(lltok_getLoc (t));
} else {
- #warning fix
+ //drl possible problem : warning fix
// llcontbug (message ("Cannot get next sequence point: %s", exprNode_unparse (e)));
return fileloc_undefined;
}
}
-
-/*drl added
- */
-exprNode exprNode_fakeCopy (exprNode e)
-{
- /*@-temptrans@*/ /*@-retalias@*/
- return e;
- /*@=temptrans@*/ /*@=retalias@*/
-}
-
exprNode exprNode_createNew(ctype c)
{
exprNode ret;
andersk / splint.git / blobdiff