# include <ctype.h> /* for isdigit */
# include "lclintMacros.nf"
# include "basic.h"
-# include "mtincludes.h"
# include "cgrammar.h"
# include "cgrammar_tokens.h"
static ctype filelocType;
static bool initMod = FALSE;
+/*@function void exprNode_swap (sef exprNode, sef exprNode)@*/
+/*@-macroassign@*/
+# define exprNode_swap(e1,e2) do { exprNode m_tmp = (e1); (e1) = (e2); (e2) = m_tmp; } while (FALSE)
+/*@=macroassign@*/
+
static void exprNode_defineConstraints(/*@sef@*/ /*@special@*/ /*@notnull@*/ exprNode e)
/*@defines e->requiresConstraints, e->ensuresConstraints,
e->trueEnsuresConstraints, e->falseEnsuresConstraints @*/
e->kind = XPR_STRINGLITERAL;
e->val = multiVal_makeString (cstring_copy (t));
e->edata = exprData_makeLiteral (t);
- e->sref = sRef_makeType (ctype_string);
+ e->sref = sRef_makeConst (ctype_string);
if (context_getFlag (FLG_READONLYSTRINGS))
{
}
ret = exprNode_fromIdentifierAux (c);
-
return ret;
}
hasError = optgenerror
(FLG_EVALORDER,
message ("Expression has undefined behavior "
- "(value of left operand is modified "
- "by right operand): %s %s %s",
+ "(value of left operand %s is modified "
+ "by right operand %s): %s %s %s",
+ exprNode_unparse (e1),
+ exprNode_unparse (e2),
exprNode_unparse (e1), lltok_unparse (op),
exprNode_unparse (e2)),
e2->loc);
}
static void
-reflectEnsuresClause (uentry le, exprNode f, exprNodeList args)
+reflectEnsuresClause (exprNode ret, uentry le, exprNode f, exprNodeList args)
{
DPRINTF (("Reflect ensures clause: %s(%s) / %s / %s",
exprNode_unparse (f), exprNodeList_unparse (args),
if (sRef_isResult (sRef_getRootBase (sel)))
{
- ; /*@i423 what do we do about results */
+ s = exprNode_getSref (ret);
}
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));
}
+
+ 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);
if (sRef_isResult (sRef_getRootBase (sel)))
{
- ; /*@i423 what do we do about results */
+ DPRINTF (("Fix base: %s / %s",
+ sRef_unparse (sel), sRef_unparse (exprNode_getSref (ret))));
+ s = sRef_fixBase (sel, exprNode_getSref (ret));
+ DPRINTF (("==> %s", sRef_unparseFull (s)));
}
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));
}
+
+ DPRINTF (("elements: %s", sRef_unparse (s)));
+ DPRINTF (("elements: %s", sRef_unparseFull (s)));
+
+ DPRINTF (("Reflecting state clause on: %s / %s",
+ sRef_unparseFull (sel), sRef_unparseFull (s)));
+
+ /* evans 2001-08-24 - added aliasSetCompleteParam */
+ sRef_aliasSetCompleteParam (modf, s, eparam, exprNode_loc (f));
+
+ DPRINTF (("After reflecting state clause on: %s / %s",
+ sRef_unparseFull (sel), sRef_unparseFull (s)));
} end_sRefSet_elements;
}
}
if (uentry_hasMetaStateEnsures (le))
{
- metaStateConstraint msc = uentry_getMetaStateEnsures (le);
- metaStateSpecifier msspec = metaStateConstraint_getSpecifier (msc);
- metaStateInfo msinfo = metaStateSpecifier_getMetaStateInfo (msspec);
- metaStateExpression msexpr = metaStateConstraint_getExpression (msc);
- cstring key = metaStateInfo_getName (msinfo);
- sRef mlsr = metaStateSpecifier_getSref (msspec);
- sRef s;
- stateValue sval = stateValue_undefined;
-
- DPRINTF (("Meta state constraint for %s: %s", uentry_unparse (le),
- metaStateConstraint_unparse (msc)));
- DPRINTF (("Matches left: %s", sRef_unparseDebug (mlsr)));
-
- if (sRef_isResult (sRef_getRootBase (mlsr)))
- {
- s = sRef_undefined; /*@i423 what about results? */
- }
- else
- {
- s = sRef_fixBaseParam (mlsr, args);
- DPRINTF (("Setting state: %s", sRef_unparseFull (s)));
- }
+ fileloc loc = exprNode_loc (f);
- /* while (metaStateExpression_isDefined (msexpr)) */
- {
- metaStateSpecifier ms = metaStateExpression_getSpecifier (msexpr);
- sRef msr = metaStateSpecifier_getSref (ms);
- metaStateInfo msi = metaStateSpecifier_getMetaStateInfo (ms);
- sRef fs;
+ metaStateConstraintList mscl = uentry_getMetaStateEnsures (le);
- if (metaStateInfo_isDefined (msi))
+ metaStateConstraintList_elements (mscl, msc)
+ {
+ metaStateSpecifier msspec = metaStateConstraint_getSpecifier (msc);
+ metaStateInfo msinfo = metaStateSpecifier_getMetaStateInfo (msspec);
+ metaStateExpression msexpr = metaStateConstraint_getExpression (msc);
+ cstring key = metaStateInfo_getName (msinfo);
+ sRef mlsr = metaStateSpecifier_getSref (msspec);
+ sRef s;
+ sRef lastref = sRef_undefined;
+ stateValue sval = stateValue_undefined;
+
+ DPRINTF (("Meta state constraint for %s: %s", uentry_unparse (le),
+ metaStateConstraint_unparse (msc)));
+ DPRINTF (("Matches left: %s", sRef_unparseDebug (mlsr)));
+
+ if (sRef_isResult (sRef_getRootBase (mlsr)))
+ {
+ s = exprNode_getSref (ret);
+ }
+ else
{
- /* Must match lhs state */
- llassert (metaStateInfo_equal (msinfo, msi));
+ s = sRef_fixBaseParam (mlsr, args);
}
+
+ DPRINTF (("Setting state: %s", sRef_unparseFull (s)));
+
+ while (metaStateExpression_isDefined (msexpr))
+ {
+ metaStateSpecifier ms = metaStateExpression_getSpecifier (msexpr);
+ metaStateInfo msi = metaStateSpecifier_getMetaStateInfo (ms);
+ sRef msr, fs;
+
+ DPRINTF (("Check expression: %s", metaStateExpression_unparse (msexpr)));
+
+ if (metaStateExpression_isMerge (msexpr))
+ {
+ msexpr = metaStateExpression_getRest (msexpr);
+ }
+ else
+ {
+ msexpr = metaStateExpression_undefined;
+ }
+
+ if (metaStateInfo_isDefined (msi))
+ {
+ /* Must match lhs state */
+ llassert (metaStateInfo_equal (msinfo, msi));
+ }
+
+ if (metaStateSpecifier_isElipsis (ms))
+ {
+ /*
+ ** For elipsis, we need to merge all the relevant elipsis parameters
+ **
+ */
+
+ uentryList params = uentry_getParams (le);
+ int paramno = uentryList_size (params) - 1;
- llassert (sRef_isParam (sRef_getRootBase (msr)));
- fs = sRef_fixBaseParam (msr, args);
+ if (!uentry_isElipsisMarker (uentryList_getN (params, paramno)))
+ {
+ voptgenerror
+ (FLG_TYPE,
+ message ("Ensures clauses uses ... for function without ... in parameter list: %q",
+ uentry_getName (le)),
+ uentry_whereLast (le));
+ /*@innerbreak@*/ break;
+ }
- sval = sRef_getMetaStateValue (fs, key);
- }
+ while (paramno < exprNodeList_size (args))
+ {
+ exprNode arg = exprNodeList_getN (args, paramno);
+ fs = exprNode_getSref (arg);
+ DPRINTF (("Merge arg: %s", exprNode_unparse (arg)));
+
+ /* cut and pasted... gack*/
+ if (stateValue_isDefined (sval))
+ {
+ /* Use combination table to merge old state value with new one: */
+ stateValue tval = sRef_getMetaStateValue (fs, key);
+
+ if (stateValue_isDefined (tval))
+ {
+ stateCombinationTable sctable = metaStateInfo_getMergeTable (msinfo);
+ cstring msg = cstring_undefined;
+ int nval = stateCombinationTable_lookup (sctable,
+ stateValue_getValue (sval),
+ stateValue_getValue (tval),
+ &msg);
+ DPRINTF (("Combining: %s + %s -> %d",
+ stateValue_unparseValue (sval, msinfo),
+ stateValue_unparseValue (tval, msinfo),
+ nval));
+
+ if (nval == stateValue_error)
+ {
+ if (optgenerror
+ (FLG_STATEMERGE,
+ message
+ ("Attributes merged in ensures clause in states that "
+ "cannot be combined (%q is %q, %q is %q)%q",
+ sRef_unparse (lastref),
+ stateValue_unparseValue (sval, msinfo),
+ sRef_unparse (fs),
+ stateValue_unparseValue (tval, msinfo),
+ cstring_isDefined (msg) ?
+ message (": %s", msg) : cstring_undefined),
+ exprNode_loc (f)))
+ {
+ sRef_showMetaStateInfo (fs, key);
+ }
+ }
+
+ stateValue_updateValueLoc (sval, nval, fileloc_undefined);
+ loc = exprNode_loc (arg);
+ }
+ else
+ {
+ DPRINTF (("No value for: %s:%s", sRef_unparse (fs), key));
+ }
+ }
+ else
+ {
+ sval = sRef_getMetaStateValue (fs, key);
+ }
+
+ lastref = fs;
+
+ if (stateValue_isError (sval))
+ {
+ /*@innerbreak@*/ break; /* Don't merge any more values if here was an error */
+ }
+
+
+ paramno++;
+ }
+ }
+ else
+ {
+ msr = metaStateSpecifier_getSref (ms);
+
+
+ llassert (sRef_isParam (sRef_getRootBase (msr)));
+ fs = sRef_fixBaseParam (msr, args);
+
+ if (stateValue_isDefined (sval))
+ {
+ /* Use combination table to merge old state value with new one: */
+ stateValue tval = sRef_getMetaStateValue (fs, key);
+
+ if (stateValue_isDefined (tval))
+ {
+ stateCombinationTable sctable = metaStateInfo_getMergeTable (msinfo);
+ cstring msg = cstring_undefined;
+ int nval = stateCombinationTable_lookup (sctable,
+ stateValue_getValue (sval),
+ stateValue_getValue (tval),
+ &msg);
+ DPRINTF (("Combining: %s + %s -> %d",
+ stateValue_unparseValue (sval, msinfo),
+ stateValue_unparseValue (tval, msinfo),
+ nval));
+
+ if (nval == stateValue_error)
+ {
+ if (optgenerror
+ (FLG_STATEMERGE,
+ message
+ ("Attributes merged in ensures clause in states that "
+ "cannot be combined (%q is %q, %q is %q)%q",
+ sRef_unparse (lastref),
+ stateValue_unparseValue (sval, msinfo),
+ sRef_unparse (fs),
+ stateValue_unparseValue (tval, msinfo),
+ cstring_isDefined (msg)
+ ? message (": %s", msg) : cstring_undefined),
+ exprNode_loc (f)))
+ {
+ sRef_showMetaStateInfo (fs, key);
+ }
+ }
+
+ stateValue_updateValueLoc (sval, nval, fileloc_undefined);
+ }
+ else
+ {
+ DPRINTF (("No value for: %s:%s", sRef_unparse (fs), key));
+ }
+ }
+ else
+ {
+ sval = sRef_getMetaStateValue (fs, key);
+ }
+
+ lastref = fs;
+
+ if (stateValue_isError (sval))
+ {
+ /*@innerbreak@*/ break; /* Don't merge any more values if here was an error */
+ }
+ }
+ }
- DPRINTF (("Setting: %s:%s <- %s", sRef_unparse (s), key, stateValue_unparse (sval)));
- sRef_setMetaStateValueComplete (s, key, stateValue_getValue (sval), exprNode_loc (f));
+ DPRINTF (("Setting: %s:%s <- %s", sRef_unparse (s), key, stateValue_unparse (sval)));
+
+ if (stateValue_isDefined (sval))
+ {
+ sRef_setMetaStateValueComplete (s, key, stateValue_getValue (sval), loc);
+ }
+ else
+ {
+ DPRINTF (("Undefined state: %s", cstring_toCharsSafe (sRef_unparse (s))));
+ }
+ } end_metaStateConstraintList_elements ;
+
+ metaStateConstraintList_free (mscl);
}
}
}
if (sRef_isResult (sRef_getRootBase (sel)))
{
- ; /*@i423 what do we do about results */
+ BADBRANCH;
}
else
{
checkRequiresClause (le, f, args);
setCodePoint ();
- DPRINTF (("Reflect: %s", uentry_unparseFull (le)));
- reflectEnsuresClause (le, f, args);
- setCodePoint ();
-
if (uentry_isValid (le)
&& (uentry_isFunction (le)
|| (uentry_isVariable (le)
/* f->typ is already set to the return type */
+ DPRINTF (("Function: %s", uentry_unparseFull (le)));
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)
{
qual nullPred = uentry_nullPred (le);
exprNode_checkSetAny (ret, uentry_rawName (le));
}
+ DPRINTF (("Before reflect: %s", sRef_unparseFull (ret->sref)));
+ DPRINTF (("Reflect: %s", uentry_unparseFull (le)));
+ reflectEnsuresClause (ret, le, f, args);
+ setCodePoint ();
+
return (ret);
}
** this is yucky! should keep the uentry as part of exprNode!
*/
-/*@observer@*/ uentry
-exprNode_getUentry (exprNode e)
+uentry exprNode_getUentry (exprNode e)
{
if (exprNode_isError (e))
{
/*DRL 6/8/01 I decided to disable all LCLint Warning here since the code
probably needs a rewrite any way */
+ /*@i65234@*/
/*@ignore@*/
- // updateEnvironmentForPostOp (e);
-
- /* start modifications */
- /* added by Seejo on 4/16/2000 */
-
- /* Arithmetic operations on pointers wil modify the size/len/null terminated
- status */
- if ((sRef_isPossiblyNullTerminated (e->sref)) || (sRef_isNullTerminated(e->sref))) {
-
- ret->sref = sRef_copy (e->sref);
-
- /* Operator : ++ */
- if (lltok_getTok (op) == INC_OP) {
- if (sRef_getSize(e->sref) > 0) {
-
- sRef_setSize (ret->sref, sRef_getSize(e->sref) - 1);
-
- if (sRef_getLen(e->sref) == 1) { /* i.e. the first character is \0 */
- /* Assumption: there is only 1 \0 in the buffer */
- /* This will not be correct if there are 2 \0's in the buffer */
- sRef_setNotNullTerminatedState(ret->sref);
- sRef_resetLen(ret->sref);
- } else {
- sRef_setNullTerminatedState(ret->sref);
- sRef_setLen (ret->sref, sRef_getLen(e->sref) - 1);
- }
- if (sRef_isNullTerminated (ret->sref))
- printf ("ret->sref is Null Terminated\n");
- else if (sRef_isPossiblyNullTerminated (ret->sref))
- printf ("ret->sref is Possibly Null Terminated\n");
- else if (sRef_isNotNullTerminated (ret->sref))
- printf ("ret->sref is Not Null Terminated\n");
- }
- }
-
- /* Operator : -- */
- if (lltok_getTok (op) == DEC_OP) {
- if (sRef_getSize(e->sref) >= 0) {
- sRef_setSize (ret->sref, sRef_getSize(e->sref) + 1);
- sRef_setLen (ret->sref, sRef_getLen(e->sref) + 1);
- }
- }
- }
- /*@end@*/
- /* end modifications */
+ /* updateEnvironmentForPostOp (e); */
+
+ /* start modifications */
+ /* added by Seejo on 4/16/2000 */
+
+ /* Arithmetic operations on pointers wil modify the size/len/null terminated
+ status */
+ if ((sRef_isPossiblyNullTerminated (e->sref)) || (sRef_isNullTerminated(e->sref))) {
+
+ ret->sref = sRef_copy (e->sref);
+
+ /* Operator : ++ */
+ if (lltok_getTok (op) == INC_OP) {
+ if (sRef_getSize(e->sref) > 0) {
+
+ sRef_setSize (ret->sref, sRef_getSize(e->sref) - 1);
+
+ if (sRef_getLen(e->sref) == 1) { /* i.e. the first character is \0 */
+ /* Assumption: there is only 1 \0 in the buffer */
+ /* This will not be correct if there are 2 \0's in the buffer */
+ sRef_setNotNullTerminatedState(ret->sref);
+ sRef_resetLen(ret->sref);
+ } else {
+ sRef_setNullTerminatedState(ret->sref);
+ sRef_setLen (ret->sref, sRef_getLen(e->sref) - 1);
+ }
+ if (sRef_isNullTerminated (ret->sref))
+ printf ("ret->sref is Null Terminated\n");
+ else if (sRef_isPossiblyNullTerminated (ret->sref))
+ printf ("ret->sref is Possibly Null Terminated\n");
+ else if (sRef_isNotNullTerminated (ret->sref))
+ printf ("ret->sref is Not Null Terminated\n");
+ }
+ }
+
+ /* Operator : -- */
+ if (lltok_getTok (op) == DEC_OP) {
+ if (sRef_getSize(e->sref) >= 0) {
+ sRef_setSize (ret->sref, sRef_getSize(e->sref) + 1);
+ sRef_setLen (ret->sref, sRef_getLen(e->sref) + 1);
+ }
+ }
+ }
+ /*@end@*/
+ /* end modifications */
return ret;
}
e1->loc);
}
+ /*
+ ** Swap terms so e1 is always the pointer
+ */
+
+ if (ctype_isRealPointer (tr1))
+ {
+ ;
+ }
+ else
+ {
+ exprNode_swap (e1, e2);
+ }
+
+
if (sRef_possiblyNull (e1->sref)
&& !usymtab_isGuarded (e1->sref))
{
ret->sref = sRef_copy (e1->sref);
- /* start modifications */
- /* added by Seejo on 4/16/2000 */
-
- /* Arithmetic operations on pointers wil modify the size/len/null terminated
- status */
- if ((sRef_isPossiblyNullTerminated (e1->sref)) || (sRef_isNullTerminated(e1->sref))) {
- //if (sRef_isKnown (e->sref)) {
- //ret->sref = sRef_makeAddress (e->sref);
- //}
-
- int val;
- /*drl 1-4-2001
- added ugly fixed to stop
- program from crashing on point + int +int
- one day I'll fix this or ask Seejo wtf the codes supposed to do. */
-
- if (!multiVal_isInt (e2->val) )
- break;
- /*end drl*/
+ /* start modifications */
+ /* added by Seejo on 4/16/2000 */
+
+ /* Arithmetic operations on pointers wil modify the size/len/null terminated
+ status */
+ if ((sRef_isPossiblyNullTerminated (e1->sref)) || (sRef_isNullTerminated(e1->sref))) {
+ int val;
+ /*drl 1-4-2001
+ added ugly fixed to stop
+ program from crashing on point + int +int
+ one day I'll fix this or ask Seejo wtf the codes supposed to do. */
+
+ if (!multiVal_isInt (e2->val) )
+ break;
+ /*end drl*/
+
+ val = (int) multiVal_forceInt (e2->val);
+
+ /* Operator : + or += */
+ if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) {
+ if (sRef_getSize(e1->sref) >= val) {/* Incrementing the pointer by
+ val should not result in a
+ size < 0 (size = 0 is ok !) */
+
+ sRef_setSize (ret->sref, sRef_getSize(e1->sref) - val);
+
+ if (sRef_getLen(e1->sref) == val) { /* i.e. the character at posn val is \0 */
+ sRef_setNotNullTerminatedState(ret->sref);
+ sRef_resetLen (ret->sref);
+ } else {
+ sRef_setNullTerminatedState(ret->sref);
+ sRef_setLen (ret->sref, sRef_getLen(e1->sref) - val);
+ }
+ }
+ }
+
+ /* Operator : - or -= */
+ if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) {
+ if (sRef_getSize(e1->sref) >= 0) {
+ sRef_setSize (ret->sref, sRef_getSize(e1->sref) + val);
+ sRef_setLen (ret->sref, sRef_getLen(e1->sref) + val);
+ }
+ }
+ }
- val = (int) multiVal_forceInt (e2->val);
-
- /* Operator : + or += */
- if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) {
- if (sRef_getSize(e1->sref) >= val) {/* Incrementing the pointer by
- val should not result in a
- size < 0 (size = 0 is ok !) */
-
- sRef_setSize (ret->sref, sRef_getSize(e1->sref) - val);
-
- if (sRef_getLen(e1->sref) == val) { /* i.e. the character at posn val is \0 */
- sRef_setNotNullTerminatedState(ret->sref);
- sRef_resetLen (ret->sref);
- } else {
- sRef_setNullTerminatedState(ret->sref);
- sRef_setLen (ret->sref, sRef_getLen(e1->sref) - val);
- }
- }
- }
-
- /* Operator : - or -= */
- if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) {
- if (sRef_getSize(e1->sref) >= 0) {
- sRef_setSize (ret->sref, sRef_getSize(e1->sref) + val);
- sRef_setLen (ret->sref, sRef_getLen(e1->sref) + val);
- }
- }
- }
-
- /* end modifications */
+ /* end modifications */
sRef_setNullError (ret->sref);
status */
if ((sRef_isPossiblyNullTerminated (e2->sref)) || (sRef_isNullTerminated(e2->sref))) {
- //if (sRef_isKnown (e->sref)) {
- //ret->sref = sRef_makeAddress (e->sref);
- //}
-
- int val = (int) multiVal_forceInt (e1->val);
-
- /* Operator : + or += */
- if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) {
- if (sRef_getSize(e2->sref) >= val) {/* Incrementing the pointer by
- val should not result in a
- size < 0 (size = 0 is ok !) */
-
- sRef_setSize (ret->sref, sRef_getSize(e2->sref) - val);
-
- if (sRef_getLen(e2->sref) == val) { /* i.e. the character at posn val is \0 */
- sRef_setNotNullTerminatedState(ret->sref);
- sRef_resetLen (ret->sref);
- } else {
- sRef_setNullTerminatedState(ret->sref);
- sRef_setLen (ret->sref, sRef_getLen(e2->sref) - val);
- }
- }
- }
-
- /* Operator : - or -= */
- if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) {
- if (sRef_getSize(e2->sref) >= 0) {
- sRef_setSize (ret->sref, sRef_getSize(e2->sref) + val);
- sRef_setLen (ret->sref, sRef_getLen(e2->sref) + val);
- }
- }
- }
-
- /* end modifications */
-
- sRef_setNullError (ret->sref);
-
- /*
- ** Fixed for 2.2c: the alias state of ptr + int is dependent,
- ** since is points to storage that should not be deallocated
- ** through this pointer.
- */
-
- if (sRef_isOnly (ret->sref)
- || sRef_isFresh (ret->sref)) {
- sRef_setAliasKind (ret->sref, AK_DEPENDENT, exprNode_loc (ret));
+ int val = (int) multiVal_forceInt (e1->val);
+
+ /* Operator : + or += */
+ if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) {
+ if (sRef_getSize(e2->sref) >= val) {/* Incrementing the pointer by
+ val should not result in a
+ size < 0 (size = 0 is ok !) */
+
+ sRef_setSize (ret->sref, sRef_getSize(e2->sref) - val);
+
+ if (sRef_getLen(e2->sref) == val) { /* i.e. the character at posn val is \0 */
+ sRef_setNotNullTerminatedState(ret->sref);
+ sRef_resetLen (ret->sref);
+ } else {
+ sRef_setNullTerminatedState(ret->sref);
+ sRef_setLen (ret->sref, sRef_getLen(e2->sref) - val);
+ }
+ }
}
-
- tret = e2->typ;
- ret->sref = e2->sref;
+
+ /* Operator : - or -= */
+ if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) {
+ if (sRef_getSize(e2->sref) >= 0) {
+ sRef_setSize (ret->sref, sRef_getSize(e2->sref) + val);
+ sRef_setLen (ret->sref, sRef_getLen(e2->sref) + val);
+ }
+ }
+ }
+
+ /* end modifications */
+
+ sRef_setNullError (ret->sref);
+
+ /*
+ ** Fixed for 2.2c: the alias state of ptr + int is dependent,
+ ** since is points to storage that should not be deallocated
+ ** through this pointer.
+ */
+
+ if (sRef_isOnly (ret->sref)
+ || sRef_isFresh (ret->sref)) {
+ sRef_setAliasKind (ret->sref, AK_DEPENDENT, exprNode_loc (ret));
+ }
+
+ tret = e2->typ;
+ ret->sref = e2->sref;
}
else
{
tret = ctype_bool;
}
+ /* certain comparisons on unsigned's and zero look suspicious */
+
+ if (opid == TLT || opid == LE_OP || opid == GE_OP)
+ {
+ if ((ctype_isUnsigned (tr1) && exprNode_isZero (e2))
+ || (ctype_isUnsigned (tr2) && exprNode_isZero (e1)))
+ {
+ voptgenerror
+ (FLG_UNSIGNEDCOMPARE,
+ message ("Comparison of unsigned value involving zero: %s",
+ exprNode_unparse (ret)),
+ e1->loc);
+ }
+ }
+
/* EQ_OP should NOT be used with booleans (unless one is FALSE) */
if ((opid == EQ_OP || opid == NE_OP) &&
sRef_unparse (e1->sref)),
g_currentloc);
}
+
+ exprNode_checkAssignMod (e1, ret); /* evans 2001-07-22 */
}
}
else
/*
** be careful! this defines e1->sref.
*/
-
- if (!sRef_isMacroParamRef (e1->sref))
- {
- exprNode_checkSet (ret, e1->sref);
- }
+
+ /* evans 2001-07-22: removed if (!sRef_isMacroParamRef (e1->sref)) */
+
+ DPRINTF (("Setting: %s -> %s", exprNode_unparse (ret), sRef_unparse (e1->sref)));
+ exprNode_checkSet (ret, e1->sref);
if (isjustalloc)
{
}
else /* all errors! */
{
- ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+ ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
}
}
{
if (exprNode_isError (tclause))
{
- ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+ ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
}
else
{
{
if (exprNode_isError (eclause))
{
- ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+ ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
}
else
{
{
if (exprNode_isError (b))
{
- ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+ ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
}
else
{
{
if (exprNode_isError (b))
{
- ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+ ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
}
else
{
ret->kind = XPR_DOWHILE;
ret->edata = exprData_makePair (t, b);
- return ret;
+ return ret;
}
exprNode exprNode_for (/*@keep@*/ exprNode inc, /*@keep@*/ exprNode body)
{
if (exprNode_isError (e2))
{
- ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+ ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
}
else
{
int i = 0;
int nerrors = 0;
+ /*@i423 check number of entries int a[3] = { 1, 2, 3, 4 } ; */
+
exprNodeList_elements (vals, oneval)
{
cstring istring = message ("%d", i);
}
else
{
- uentry ue = uentry_makeUnrecognized (idDecl_observeId (t),
- g_currentloc);
+ uentry ue;
+
+ DPRINTF (("Unrecognized: %s", idDecl_unparse (t)));
+
+ ue = uentry_makeUnrecognized (idDecl_observeId (t), fileloc_copy (g_currentloc));
+ /*!! fileloc_copy (g_currentloc)); */
+ /*@i32!!! should get error without this */
ret = exprNode_fromIdentifierAux (ue);
/*
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);
-
+
if (exprNode_isError (e))
{
e = exprNode_createUnknown ();
case XPR_VAR:
ret = exprData_getId (data);
break;
+ case XPR_INIT:
+ ret = idDecl_getName (exprData_getInitId (data));
+ break;
case XPR_LABEL:
case XPR_TOK:
case XPR_ITERCALL:
case XPR_BLOCK:
case XPR_STMT:
case XPR_STMTLIST:
- case XPR_INIT:
case XPR_FACCESS:
case XPR_ARROW:
case XPR_NODE:
{
lastRef = errorRef;
errorRef = s;
+ DPRINTF (("Setting ERROR: %s", sRef_unparseFull (s)));
deadRef = sRef_isPossiblyDead (errorRef);
unuseable = sRef_isUnuseable (errorRef);
errorMaybe = TRUE;
if (!sRef_isPartial (s))
{
+ DPRINTF (("Defining! %s", sRef_unparseFull (s)));
sRef_setDefined (s, fileloc_undefined);
}
}
sRef_unparseOpt (errorRef),
cstring_makeLiteral (errorMaybe ? "may be " : "")),
loc);
+
+ DPRINTF (("Error: %s", sRef_unparseFull (errorRef)));
}
sRef_setDefined (errorRef, loc);
}
if (sRef_isMeaningful (s))
- {
-
+ {
if (sRef_isDead (s))
{
sRef base = sRef_getBaseSafe (s);
lltok t = exprData_getUopTok (e->edata);
return fileloc_copy(lltok_getLoc (t));
} else {
- //drl possible problem : warning fix
- // llcontbug (message ("Cannot get next sequence point: %s", exprNode_unparse (e)));
+ /* drl possible problem : warning fix
+ llcontbug (message ("Cannot get next sequence point: %s", exprNode_unparse (e)));
+ */
return fileloc_undefined;
}
}
return ret;
}
+
+bool exprNode_isInitBlock (exprNode e)
+{
+ return (exprNode_isDefined(e) && e->kind == XPR_INITBLOCK);
+}
andersk / splint.git / blobdiff