/*
** Splint - annotation-assisted static program checker
** Copyright (C) 1994-2003 University of Virginia,
** Massachusetts Institute of Technology
**
** This program is free software; you can redistribute it and/or modify it
** under the terms of the GNU General Public License as published by the
** Free Software Foundation; either version 2 of the License, or (at your
** option) any later version.
**
** This program is distributed in the hope that it will be useful, but
** WITHOUT ANY WARRANTY; without even the implied warranty of
** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
** General Public License for more details.
**
** The GNU General Public License is available from http://www.gnu.org/ or
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
** For information on splint: info@splint.org
** To report a bug: splint-bug@splint.org
** For more information: http://www.splint.org
*/
/*
** stateClauseList.c
*/
# include "splintMacros.nf"
# include "basic.h"
static /*@notnull@*/ stateClauseList stateClauseList_new (void)
{
stateClauseList s = (stateClauseList) dmalloc (sizeof (*s));
s->nelements = 0;
s->nspace = stateClauseListBASESIZE;
s->elements = (stateClause *)
dmalloc (sizeof (*s->elements) * stateClauseListBASESIZE);
return (s);
}
static void
stateClauseList_grow (stateClauseList s)
{
int i;
stateClause *newelements;
llassert (stateClauseList_isDefined (s));
s->nspace += stateClauseListBASESIZE;
newelements = (stateClause *)
dmalloc (sizeof (*newelements) * (s->nelements + s->nspace));
for (i = 0; i < s->nelements; i++)
{
newelements[i] = s->elements[i];
}
sfree (s->elements);
s->elements = newelements;
}
stateClauseList stateClauseList_add (stateClauseList s, stateClause el)
{
DPRINTF (("Adding: %s", stateClause_unparse (el)));
if (stateClauseList_isUndefined (s))
{
s = stateClauseList_new ();
}
else
{
stateClauseList_elements (s, cl)
{
if (stateClause_sameKind (cl, el))
{
voptgenerror
(FLG_SYNTAX,
message ("Multiple %q clauses for one function (ignoring second)",
stateClause_unparseKind (cl)),
g_currentloc);
stateClause_free (el);
return s;
}
} end_stateClauseList_elements ;
}
if (s->nspace <= 0)
{
stateClauseList_grow (s);
}
s->nspace--;
s->elements[s->nelements] = el;
s->nelements++;
return s;
}
cstring stateClauseList_unparse (stateClauseList s)
{
cstring st = cstring_undefined;
int i;
if (stateClauseList_isDefined (s))
{
for (i = 0; i < stateClauseList_size (s); i++)
{
if (i == 0)
{
st = message ("%q;", stateClause_unparse (s->elements[i]));
}
else
st = message ("%q %q;", st, stateClause_unparse (s->elements[i]));
}
}
return (st);
}
stateClauseList stateClauseList_copy (stateClauseList s)
{
if (stateClauseList_isDefined (s))
{
stateClauseList t = (stateClauseList) dmalloc (sizeof (*t));
int i;
t->nelements = s->nelements;
t->nspace = 0;
if (s->nelements > 0)
{
t->elements = (stateClause *) dmalloc (sizeof (*t->elements) * t->nelements);
for (i = 0; i < s->nelements; i++)
{
t->elements[i] = stateClause_copy (s->elements[i]);
}
}
else
{
t->elements = NULL;
}
return t;
}
else
{
return stateClauseList_undefined;
}
}
void
stateClauseList_free (stateClauseList s)
{
if (!stateClauseList_isUndefined (s))
{
int i;
for (i = 0; i < s->nelements; i++)
{
stateClause_free (s->elements[i]);
}
sfree (s->elements);
sfree (s);
}
}
cstring stateClauseList_dump (stateClauseList s)
{
cstring st = cstring_undefined;
if (stateClauseList_isUndefined (s)) return st;
stateClauseList_elements (s, current)
{
st = message ("%q%q$", st, stateClause_dump (current));
} end_stateClauseList_elements;
return st;
}
stateClauseList stateClauseList_undump (char **s)
{
char c;
stateClauseList pn = stateClauseList_new ();
int paramno = 0;
c = **s;
while (c != '#' && c != '@')
{
stateClause sc = stateClause_undump (s);
pn = stateClauseList_add (pn, sc);
reader_checkChar (s, '$');
c = **s;
paramno++;
}
return pn;
}
int stateClauseList_compare (stateClauseList s1, stateClauseList s2)
{
if (stateClauseList_isUndefined (s1)
&& stateClauseList_isUndefined (s2))
{
return 0;
}
else
{
if (s1 - s2 > 0) /* evans 2001-08-21: was (int) s1 > (int) s2) */
{
return 1;
}
else
{
return -1;
}
}
}
static /*@exposed@*/ sRefSet
stateClauseList_getClause (stateClauseList s, stateClause k)
{
stateClauseList_elements (s, el)
{
if (stateClause_matchKind (el, k))
{
return stateClause_getRefs (el);
}
} end_stateClauseList_elements ;
return sRefSet_undefined;
}
void stateClauseList_checkAll (uentry ue)
{
stateClauseList clauses = uentry_getStateClauseList (ue);
sRef res = uentry_getSref (ue);
bool specialResult = FALSE;
DPRINTF (("Check state clauses: %s", uentry_unparseFull (ue)));
stateClauseList_elements (clauses, cl)
{
bool isPre = stateClause_isBeforeOnly (cl);
if (stateClause_isGlobal (cl))
{
;
}
else
{
sRefSet refs = stateClause_getRefs (cl);
sRefSet_allElements (refs, el)
{
sRef rb = sRef_getRootBase (el);
DPRINTF (("Check: %s", sRef_unparse (el)));
if (sRef_isResult (rb))
{
/*
** The result type is now know, need to set it:
*/
if (ctype_isUnknown (sRef_getType (rb)))
{
ctype utype = uentry_getType (ue);
llassert (ctype_isFunction (utype));
sRef_setTypeFull (rb, ctype_getReturnType (utype));
DPRINTF (("el: %s", sRef_unparseFull (el)));
}
}
if (stateClause_setsMetaState (cl))
{
qual q = stateClause_getMetaQual (cl);
annotationInfo qa = qual_getAnnotationInfo (q);
if (!annotationInfo_matchesContextRef (qa, el))
{
if (optgenerror
(FLG_ANNOTATIONERROR,
message ("Attribute annotation %s used on inappropriate reference %q in %q clause of %q: %q",
qual_unparse (q),
sRef_unparse (el),
stateClause_unparseKind (cl),
uentry_getName (ue),
stateClause_unparse (cl)),
uentry_whereLast (ue)))
{
/* annotationInfo_showContextError (ainfo, ue); */
}
}
}
if (sRef_isResult (rb))
{
if (isPre)
{
voptgenerror
(FLG_INCONDEFS,
message ("Function result is used in %q clause of %q "
"(%q applies to the state before function is "
"called, so should not use result): %q",
stateClause_unparseKind (cl),
uentry_getName (ue),
stateClause_unparseKind (cl),
sRef_unparse (el)),
uentry_whereLast (ue));
}
else
{
if (!sRef_isStateSpecial (res))
{
DPRINTF (("Here we are: %s", sRef_unparseFull (res)));
if (!specialResult)
{
sstate pstate = sRef_getDefState (res);
if (!sRef_makeStateSpecial (res))
{
if (optgenerror
(FLG_INCONDEFS,
message ("Function result is used in %q clause of %q "
"but was previously annotated with %s: %q",
stateClause_unparseKind (cl),
uentry_getName (ue),
sstate_unparse (pstate),
sRef_unparse (el)),
uentry_whereLast (ue)))
{
specialResult = TRUE;
}
}
}
}
DPRINTF (("Fixing result type! %s", sRef_unparseFull (el)));
(void) sRef_fixResultType (el, sRef_getType (res), ue);
}
}
else if (sRef_isParam (rb))
{
DPRINTF (("Make special: %s", sRef_unparseFull (rb)));
if (!sRef_makeStateSpecial (rb))
{
if (fileloc_isXHFile (uentry_whereLast (ue)))
{
; /* Okay to override in .xh files */
}
else if (stateClause_isQual (cl))
{
; /* qual clauses don't interfere with definition state */
}
else
{
voptgenerror
(FLG_INCONDEFS,
message ("Reference %q used in %q clause of %q, "
"but was previously annotated with %s: %q",
sRef_unparse (rb),
stateClause_unparseKind (cl),
uentry_getName (ue),
sstate_unparse (sRef_getDefState (res)),
sRef_unparse (el)),
uentry_whereLast (ue));
}
}
DPRINTF (("Made special: %s", sRef_unparseFull (rb)));
}
else if (sRef_isInvalid (rb))
{
/*@innercontinue@*/ continue;
}
else
{
BADBRANCHCONT;
/*@innercontinue@*/ continue;
}
if (stateClause_isMemoryAllocation (cl))
{
if (!ctype_isVisiblySharable (sRef_getType (el)))
{
voptgenerror
(FLG_ANNOTATIONERROR,
/*@-sefparams@*/ /* This is okay because its fresh storage. */
message
("%q clauses includes %q of "
"non-dynamically allocated type %s",
cstring_capitalizeFree (stateClause_unparseKind (cl)),
sRef_unparse (el),
ctype_unparse (sRef_getType (el))),
uentry_whereLast (ue));
/*@=sefparams@*/
}
}
} end_sRefSet_allElements ;
}
} end_stateClauseList_elements ;
}
void stateClauseList_checkEqual (uentry old, uentry unew)
{
stateClauseList oldClauses = uentry_getStateClauseList (old);
stateClauseList newClauses = uentry_getStateClauseList (unew);
if (stateClauseList_isDefined (newClauses))
{
stateClauseList_elements (newClauses, cl)
{
if (stateClause_isGlobal (cl))
{
;
}
else
{
sRefSet sc = stateClauseList_getClause (oldClauses, cl);
if (!sRefSet_equal (sc, stateClause_getRefs (cl)))
{
if (optgenerror
(FLG_INCONDEFS,
message ("Function %q %rdeclared with inconsistent %q clause: %q",
uentry_getName (old),
uentry_isDeclared (old),
stateClause_unparseKind (cl),
sRefSet_unparsePlain (stateClause_getRefs (cl))),
g_currentloc))
{
uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc));
}
}
}
} end_stateClauseList_elements ;
stateClauseList_elements (oldClauses, cl)
{
if (stateClause_isGlobal (cl))
{
; /* Don't handle globals for now */
}
else
{
sRefSet sc = stateClauseList_getClause (newClauses, cl);
if (sRefSet_isUndefined (sc) && !sRefSet_isEmpty (stateClause_getRefs (cl)))
{
if (optgenerror
(FLG_INCONDEFS,
message ("Function %q %rdeclared without %q clause (either "
"use no special clauses in redeclaration, or "
"they must match exactly: %q",
uentry_getName (old),
uentry_isDeclared (old),
stateClause_unparseKind (cl),
sRefSet_unparsePlain (stateClause_getRefs (cl))),
g_currentloc))
{
uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc));
}
}
}
} end_stateClauseList_elements ;
}
}
syntax highlighted by Code2HTML, v. 0.9.1