/*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2001 University of Virginia,
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2002 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
**
** For information on lclint: lclint-request@cs.virginia.edu
** To report a bug: lclint-bug@cs.virginia.edu
-** For more information: http://lclint.cs.virginia.edu
+** For more information: http://www.splint.org
*/
/*
** storeRef.c
static void sRef_addDeriv (/*@notnull@*/ sRef p_s, /*@notnull@*/ /*@exposed@*/ sRef p_t);
static bool sRef_checkModify (sRef p_s, sRefSet p_sl) /*@*/ ;
+/*
+** If s is definitely null, it has no memory state.
+*/
+
+static void sRef_resetAliasKind (/*@notnull@*/ sRef s) /*@modifies s->aliaskind@*/
+{
+ if (s->nullstate == NS_DEFNULL)
+ {
+ /* s->aliaskind = AK_ERROR; */
+ }
+}
+
static void sRef_checkMutable (/*@unused@*/ sRef s)
{
/*@i235@*/
&& (s->expinfo != NULL) && (fileloc_isDefined (s->expinfo->loc)));
}
+# if 0
static /*@observer@*/ /*@unused@*/ stateInfo sRef_getInfo (sRef s, cstring key)
{
stateValue sv;
return stateInfo_undefined;
}
-
+# endif
static bool
sRef_hasNullInfoLoc (sRef s)
("Warning: reference base limit exceeded for %q. "
"This either means there is a variable with at least "
"%d indirections from this reference, or "
- "there is a bug in LCLint.",
+ "there is a bug in Splint.",
sRef_unparse (s),
MAXBASEDEPTH),
g_currentloc);
llassertfatal (sRef_isValid (res));
llassertfatal (sRef_isValid (other));
+ DPRINTF (("Merge aux: %s / %s",
+ bool_unparse (sRef_isDefinitelyNull (res)),
+ bool_unparse (sRef_isDefinitelyNull (other))));
+
sRef_checkMutable (res);
sRef_checkMutable (other);
bool sRef_isStrictReadable (sRef s)
{
- return (ynm_toBoolStrict (sRef_isReadable (s)));
+ return (ynm_toBoolStrict (sRef_isValidLvalue (s)));
}
-ynm sRef_isReadable (sRef s)
+/*
+** Is this what is does?
+** Returns YES if s can be used as an rvalue,
+** MAYBE if its not clear
+** NO if s cannot be safely used as an rvalue.
+*/
+
+ynm sRef_isValidLvalue (sRef s)
{
sstate ss;
if (sRef_isConj (s) && s->defstate == SS_UNKNOWN)
{
- if (ynm_toBoolStrict (sRef_isReadable (sRef_getConjA (s))))
+ if (ynm_toBoolStrict (sRef_isValidLvalue (sRef_getConjA (s))))
{
- if (ynm_toBoolStrict (sRef_isReadable (sRef_getConjB (s))))
+ if (ynm_toBoolStrict (sRef_isValidLvalue (sRef_getConjB (s))))
{
return YES;
}
}
else
{
- if (ynm_toBoolStrict (sRef_isReadable (sRef_getConjB (s))))
+ if (ynm_toBoolStrict (sRef_isValidLvalue (sRef_getConjB (s))))
{
return MAYBE;
}
|| ss == SS_FIXED
|| ss == SS_RELDEF
|| ss == SS_PDEFINED
- || ss == SS_PARTIAL
+ || ss == SS_PARTIAL
|| ss == SS_SPECIAL
- || ss == SS_ALLOCATED
+ || ss == SS_ALLOCATED
|| ss == SS_KILLED /* evans 2001-05-26: added this for killed globals */
|| ss == SS_UNKNOWN));
}
("Warning: check definition limit exceeded, checking %q. "
"This either means there is a variable with at least "
"%d indirections apparent in the program text, or "
- "there is a bug in LCLint.",
+ "there is a bug in Splint.",
sRef_unparse (fref),
MAXDEPTH),
g_currentloc);
void sRef_setDefinedComplete (sRef s, fileloc loc)
{
+ sRef_innerAliasSetComplete (sRef_setDefined, s, loc);
+}
+
+void sRef_setDefinedCompleteDirect (sRef s, fileloc loc)
+{
+ sRefSet aliases;
+
+ aliases = usymtab_allAliases (s);
DPRINTF (("Set defined complete: %s", sRef_unparseFull (s)));
+ DPRINTF (("All aliases: %s", sRefSet_unparseFull (aliases)));
+
+ sRef_setDefined (s, loc);
+
+ sRefSet_realElements (aliases, current)
+ {
+ if (sRef_isValid (current))
+ {
+ current = sRef_updateSref (current);
+ sRef_setDefined (current, loc);
+ }
+ } end_sRefSet_realElements;
+
+ sRefSet_free (aliases);
sRef_innerAliasSetComplete (sRef_setDefined, s, loc);
}
DPRINTF (("Set null state: %s / %s", sRef_unparse (s), nstate_unparse (ns)));
sRef_checkMutable (s);
s->nullstate = ns;
-
+ sRef_resetAliasKind (s);
+
if (fileloc_isDefined (loc))
{
s->nullinfo = stateInfo_updateLoc (s->nullinfo, loc);
{
sRef_checkMutable (s);
s->nullstate = n;
+ sRef_resetAliasKind (s);
}
void sRef_setNullState (sRef s, nstate n, fileloc loc)
}
}
-void sRef_setNullTerminatedStateInnerComplete (sRef s, struct s_bbufinfo b, /*@unused@*/ fileloc loc) {
-
+void sRef_setNullTerminatedStateInnerComplete (sRef s, struct s_bbufinfo b, /*@unused@*/ fileloc loc)
+{
switch (b.bufstate) {
case BB_NULLTERMINATED:
sRef_setNullTerminatedState (s);
static bool
sRef_isAllocatedStorage (sRef s)
{
- if (sRef_isValid (s) && ynm_toBoolStrict (sRef_isReadable (s)))
+ if (sRef_isValid (s) && ynm_toBoolStrict (sRef_isValidLvalue (s)))
{
return (ctype_isVisiblySharable (sRef_getType (s)));
}
inner = s->info->field->rec;
aliases = usymtab_allAliases (inner);
ct = sRef_getType (inner);
-
sRefSet_realElements (aliases, current)
{
inner = s->info->ref;
aliases = usymtab_allAliases (inner);
ct = sRef_getType (inner);
-
-
+
sRefSet_realElements (aliases, current)
{
if (sRef_isValid (current))
sRef_checkMutable (res);
+ DPRINTF (("Combine alias kinds: \n\t%s / \n\t%s",
+ sRef_unparseFull (res), sRef_unparseFull (other)));
if (alkind_equal (ares, aother)
|| aother == AK_UNKNOWN
|| aother == AK_ERROR)
res ->aliaskind = AK_ERROR;
}
else if (ares == AK_UNKNOWN || ares == AK_ERROR
- || sRef_isStateUndefined (res))
+ || sRef_isStateUndefined (res)
+ || sRef_isDefinitelyNull (res))
{
res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
res->aliaskind = aother;
}
- else if (sRef_isStateUndefined (other))
+ else if (sRef_isStateUndefined (other)
+ || sRef_isDefinitelyNull (other))
{
;
}
{
res->nullstate = other->nullstate;
res->nullinfo = stateInfo_update (res->nullinfo, other->nullinfo);
+ sRef_resetAliasKind (res);
}
void sRef_combineNullState (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other)
}
res->nullstate = nn;
+ sRef_resetAliasKind (res);
}
cstring sRef_nullMessage (sRef s)