/*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2000 University of Virginia,
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2001 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
*/
/*
** clabstract.c
*/
/*drl*/
-static constraintList fcnConstraints = NULL;
+static /*@only@*/ constraintList implicitFcnConstraints = NULL;
-static constraintList fcnEnsuresConstraints = NULL;
-/*end drl*/
-
-//static constraintList fcnPreConditions = NULL;
-
-
-static /*@only@*/ sRefSet fcnModifies = sRefSet_undefined;
-static /*@only@*/ /*@null@*/ specialClauses specClauses = specialClauses_undefined;
+static void clabstract_prepareFunction (uentry p_e) /*@modifies p_e@*/ ;
static bool fcnNoGlobals = FALSE;
static bool ProcessingVars = FALSE;
static bool ProcessingParams = FALSE;
static bool ProcessingIterVars = FALSE;
static /*@only@*/ qtype processingType = qtype_undefined;
static uentry currentIter = uentry_undefined;
-static globSet currentGlobals = globSet_undefined;
static /*@dependent@*/ uentryList saveParamList; /* for old style functions */
static /*@owned@*/ uentry saveFunction = uentry_undefined;
static int saveIterParamNo;
static storageClassCode storageClass = SCNONE;
static void declareEnumList (/*@temp@*/ enumNameList p_el, ctype p_c, fileloc p_loc);
static void resetGlobals (void);
-static qual specialFunctionCode = QU_UNKNOWN;
+static /*@null@*/ qual specialFunctionCode;
static bool argsUsed = FALSE;
+extern void clabstract_initMod ()
+{
+ specialFunctionCode = qual_createUnknown ();
+ DPRINTF (("Initialized: %s", qual_unparse (specialFunctionCode)));
+}
+
static bool hasSpecialCode (void)
{
- return (specialFunctionCode != QU_UNKNOWN);
+ return (!qual_isUnknown (specialFunctionCode));
}
extern void setArgsUsed (void)
extern void setSpecialFunction (qual qu)
{
- if (specialFunctionCode != QU_UNKNOWN)
+ if (!qual_isUnknown (specialFunctionCode))
{
voptgenerror (FLG_SYNTAX,
message ("Multiple special function codes: %s, %s "
static void reflectSpecialCode (uentry ue)
{
- switch (specialFunctionCode)
- {
- case QU_UNKNOWN: break;
- case QU_PRINTFLIKE:
- uentry_setPrintfLike (ue);
- break;
- case QU_SCANFLIKE:
- uentry_setScanfLike (ue);
- break;
- case QU_MESSAGELIKE:
- uentry_setMessageLike (ue);
- break;
- BADDEFAULT;
- }
+ if (qual_isUnknown (specialFunctionCode)) {
+ ;
+ } else if (qual_isPrintfLike (specialFunctionCode)) {
+ uentry_setPrintfLike (ue);
+ } else if (qual_isScanfLike (specialFunctionCode)) {
+ uentry_setScanfLike (ue);
+ } else if (qual_isMessageLike (specialFunctionCode)) {
+ uentry_setMessageLike (ue);
+ } else {
+ BADBRANCH;
+ }
- specialFunctionCode = QU_UNKNOWN;
+ specialFunctionCode = qual_createUnknown ();
}
static void resetStorageClass (void)
storageClass = SCNONE;
}
-static void reflectModGlobs (uentry ue)
-{
- if (fcnNoGlobals)
- {
- llassert (globSet_isUndefined (currentGlobals));
-
- uentry_setGlobals (ue, globSet_undefined);
- fcnNoGlobals = FALSE;
- }
- else if (globSet_isDefined (currentGlobals))
- {
- uentry_setGlobals (ue, currentGlobals);
- currentGlobals = globSet_undefined;
- }
- else
- {
- ; /* no globals */
- }
-
- if (sRefSet_isDefined (fcnModifies))
- {
- uentry_setModifies (ue, fcnModifies);
- fcnModifies = sRefSet_undefined;
- }
- /*drl added*/
- if (fcnConstraints)
- {
- uentry_setPreconditions (ue, fcnConstraints);
- fcnConstraints = constraintList_undefined;
- }
-
- if (fcnEnsuresConstraints)
- {
- uentry_setPostconditions (ue, fcnEnsuresConstraints);
- fcnEnsuresConstraints = constraintList_undefined;
- }
- /*end drl*/
-
- if (uentry_isFunction (ue))
- {
- uentry_setSpecialClauses (ue, specClauses);
- specClauses = NULL;
- DPRINTF (("Done with spec clauses"));
- }
-}
-
static void reflectStorageClass (uentry u)
{
if (storageClass == SCSTATIC)
void setFunctionNoGlobals (void)
{
- llassert (globSet_isUndefined (currentGlobals));
fcnNoGlobals = TRUE;
}
-void
- setFunctionStateSpecialClause (lltok stok, specialClauseKind kind,
- sRefSet s,
- /*@unused@*/ lltok etok)
-{
- int tok = lltok_getTok (stok);
-
- switch (tok)
- {
- case QPRECLAUSE:
- specClauses = specialClauses_add (specClauses,
- specialClause_create (TK_BEFORE, kind, s));
- break;
- case QPOSTCLAUSE:
- specClauses = specialClauses_add (specClauses,
- specialClause_create (TK_AFTER, kind, s));
- break;
- default:
- sRefSet_free (s);
- BADBRANCH;
- }
-
- DPRINTF (("Added to specclauses: %s", specialClauses_unparse (specClauses)));
-}
-
-void setFunctionSpecialClause (lltok stok, sRefSet s,
- /*@unused@*/ lltok etok)
-{
- int tok = lltok_getTok (stok);
-
- switch (tok)
- {
- case QUSES:
- specClauses = specialClauses_add (specClauses, specialClause_createUses (s));
- break;
- case QDEFINES:
- specClauses = specialClauses_add (specClauses, specialClause_createDefines (s));
- break;
- case QALLOCATES:
- specClauses = specialClauses_add (specClauses, specialClause_createAllocates (s));
- break;
- case QSETS:
- specClauses = specialClauses_add (specClauses, specialClause_createSets (s));
- break;
- case QRELEASES:
- specClauses = specialClauses_add (specClauses, specialClause_createReleases (s));
- break;
- default:
- sRefSet_free (s);
- BADBRANCH;
- }
-
- DPRINTF (("Added to specclauses: %s", specialClauses_unparse (specClauses)));
-}
-
-/*drl
- */
-constraintList getFunctionConstraints (void)
-{
- return constraintList_copy (fcnConstraints);
-}
-
-
-constraintList getEnsuresConstraints (void)
-{
- return constraintList_copy (fcnEnsuresConstraints);
-}
-
-void setEnsuresConstraints (constraintList c)
-{
- #warning m leak
- fcnEnsuresConstraints = constraintList_copy (c);
-}
-
-void setFunctionConstraints (constraintList c)
-{
- #warning m leak
- fcnConstraints = constraintList_copy (c);
-}
-/* end drl*/
-
-void setFunctionModifies (sRefSet s)
-{
- sRefSet_free (fcnModifies);
- fcnModifies = s;
-}
-
static void reflectGlobalQualifiers (sRef sr, qualList quals)
{
+ DPRINTF (("Reflect global qualifiers: %s / %s",
+ sRef_unparseFull (sr), qualList_unparse (quals)));
+
qualList_elements (quals, qel)
{
if (qual_isGlobalQual (qel)) /* undef, killed */
}
sRef_setDefState (sr, defstate, fileloc_undefined);
+ DPRINTF (("State: %s", sRef_unparseFull (sr)));
}
else if (qual_isAllocQual (qel)) /* out, partial, reldef, etc. */
{
} end_qualList_elements;
}
-void globListAdd (sRef sr, qualList quals)
+sRef clabstract_createGlobal (sRef sr, qualList quals)
{
+ sRef res;
+
if (sRef_isValid (sr))
{
- sRef sc = sRef_copy (sr);
-
- reflectGlobalQualifiers (sc, quals);
- currentGlobals = globSet_insert (currentGlobals, sc);
+ res = sRef_copy (sr);
+ DPRINTF (("Reflecting quals: %s / %s", sRef_unparse (sr), qualList_unparse (quals)));
+ reflectGlobalQualifiers (res, quals);
+ DPRINTF (("==> %s", sRef_unparseFull (res)));
+ }
+ else
+ {
+ res = sRef_undefined;
}
+
+ qualList_free (quals);
+ return res;
}
extern void declareCIter (cstring name, /*@owned@*/ uentryList params)
fileloc_copy (g_currentloc));
usymtab_supEntry (uentry_makeEndIter (name, fileloc_copy (g_currentloc)));
-
- reflectModGlobs (ue);
-
ue = usymtab_supGlobalEntryReturn (ue);
}
static /*@dependent@*/ uentryList currentParamList;
+/*drl added 3-28-2001*/
+/* this function takes a list of paramentar and generates a list
+ of constraints.
+ Currently the only constraints gnerated are MaxSet(p) >= 0 for all pointers
+*/
+
+void setImplictfcnConstraints (void)
+{
+ uentryList params;
+ sRef s;
+ constraint c;
+ params = currentParamList;
+
+ if (constraintList_isDefined(implicitFcnConstraints) )
+ constraintList_free(implicitFcnConstraints);
+
+ implicitFcnConstraints = constraintList_makeNew();
+
+ uentryList_elements (params, el)
+ {
+ DPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) ));
+
+ s = uentry_getSref(el);
+ if (sRef_isReference (s) )
+ {
+ DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
+ }
+ else
+ {
+ DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
+ }
+ /*drl 4/26/01
+ chagned this is MaxSet(s) == 0 to MaxSet(s) >= 0 */
+
+ c = constraint_makeSRefWriteSafeInt (s, 0);
+ /* constraint_makeSRefSetBufferSize (s, 0); */
+ implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
+ }
+ end_uentryList_elements;
+}
+
+
+/*@observer@*/ constraintList getImplicitFcnConstraints (void)
+{
+ return implicitFcnConstraints;
+}
+
void setCurrentParams (/*@dependent@*/ uentryList ue)
{
currentParamList = ue;
usymtab_quietPlainExitScope ();
}
-static /*@exposed@*/ uentry globalDeclareFunction (idDecl tid)
+static /*@exposed@*/ uentry clabstract_globalDeclareFunction (idDecl tid)
{
ctype deftype = idDecl_getCtype (tid);
ctype rettype;
uentry ue;
DPRINTF (("Global function: %s", idDecl_unparse (tid)));
-
+
if (ctype_isFunction (deftype))
{
- rettype = ctype_returnValue (deftype);
+ rettype = ctype_getReturnType (deftype);
}
else
{
(tid, ctype_makeFunction (ctype_unknown, uentryList_undefined));
ue = uentry_makeIdFunction (tid);
}
-
- reflectStorageClass (ue);
+ reflectStorageClass (ue);
uentry_checkParams (ue);
- reflectModGlobs (ue);
+
+ DPRINTF (("Supercede function: %s", uentry_unparseFull (ue)));
ue = usymtab_supGlobalEntryReturn (ue);
+ DPRINTF (("After supercede function: %s", uentry_unparseFull (ue)));
+
+ DPRINTF (("Enter function: %s", uentry_unparseFull (ue)));
context_enterFunction (ue);
enterFunctionParams (uentry_getParams (ue));
resetStorageClass ();
+ DPRINTF (("Function: %s", uentry_unparseFull (ue)));
return (ue);
}
reflectSpecialCode (ue);
reflectArgsUsed (ue);
uentry_setDefined (ue, g_currentloc);
+ uentry_checkParams (ue);
+ resetStorageClass ();
- uentry_checkParams (ue);
-
- if (ProcessingGlobals)
- {
- uentry_setGlobals (ue, currentGlobals);
- }
+ /* context_enterOldStyleScope (); */
- resetStorageClass ();
return (ue);
}
llassert (ctype_isFunction (rt));
+ if (uentry_hasStateClauseList (e)
+ || uentry_hasConditions (e))
+ {
+ llfatalerror (message ("%q: Old-style function declaration uses a clause (rewrite with function parameters): %q",
+ fileloc_unparse (g_currentloc), uentry_unparse (e)));
+ }
+
e = usymtab_supGlobalEntryReturn (e);
context_enterFunction (e);
resetStorageClass ();
}
-void declareFunction (idDecl tid) /*@globals undef saveFunction; @*/
+static void oldStyleCompleteFunction (/*@only@*/ uentry e)
+{
+ uentryList params = saveParamList;
+ ctype rt = uentry_getType (e);
+
+ llassert (ctype_isFunction (rt));
+
+ if (uentry_hasStateClauseList (e)
+ || uentry_hasConditions (e))
+ {
+ llfatalerror (message ("%q: Old-style function declaration uses a clause (rewrite with function parameters): %q",
+ fileloc_unparse (g_currentloc), uentry_unparse (e)));
+ }
+
+ e = usymtab_supGlobalEntryReturn (e);
+
+ context_completeOldStyleFunction (e);
+ enterFunctionParams (params);
+ saveParamList = uentryList_undefined;
+ resetStorageClass ();
+}
+
+void clabstract_declareFunction (idDecl tid) /*@globals undef saveFunction; @*/
{
uentry ue;
{
ue = globalDeclareOldStyleFunction (tid);
saveFunction = ue;
+ DPRINTF (("Set save function: %s", uentry_unparseFull (ue)));
}
else
{
}
else
{
- ue = globalDeclareFunction (tid);
+ ue = clabstract_globalDeclareFunction (tid);
}
}
if (ctype_isFunction (deftype))
{
- rettype = ctype_returnValue (deftype);
+ rettype = ctype_getReturnType (deftype);
}
else
{
uentry_setStatic (ue);
uentry_checkParams (ue);
- reflectModGlobs (ue);
DPRINTF (("Sub global entry: %s", uentry_unparse (ue)));
ue = usymtab_supGlobalEntryReturn (ue);
{
cstring n = uentry_getName (e);
- DPRINTF (("Check type decl: %s", n));
+ DPRINTF (("Check type decl: %s", uentry_unparseFull (e)));
if (cstring_equal (context_getBoolName (), n))
{
uentry le = usymtab_getTypeEntry (llm);
uentry_setDeclared (e, g_currentloc);
- uentry_setSref (e, sRef_makeGlobal (llm, uentry_getType (le)));
+ uentry_setSref (e, sRef_makeGlobal (llm, uentry_getType (le), stateInfo_currentLoc ()));
DPRINTF (("Here we are: %s / %s",
n, context_getBoolName ()));
{
ctype rrep = ctype_realType (rep);
+ DPRINTF (("Abstract type: %s", uentry_unparseFull (le)));
+
/*
** for abstract enum types, we need to fix the enum members:
** they should have the abstract type, not the rep type.
setProcessingGlobalsList ()
{
ProcessingGlobals = TRUE;
-
- llassert (globSet_isUndefined (currentGlobals));
- currentGlobals = globSet_undefined;
-
- llassert (sRefSet_isUndefined (fcnModifies));
- fcnModifies = sRefSet_undefined;
-
- /*
- ** No, special clauses might have been processed first!
- llassert (specialClauses_isUndefined (specClauses));
- specClauses = specialClauses_undefined;
- */
-
fcnNoGlobals = FALSE;
}
static void resetGlobals (void)
{
ProcessingGlobals = FALSE;
- currentGlobals = globSet_undefined;
- llassert (sRefSet_isUndefined (fcnModifies));
- fcnModifies = sRefSet_undefined;
fcnNoGlobals = FALSE;
}
}
void
-setProcessingTypedef (/*@only@*/ qtype q)
+setProcessingTypedef (qtype q)
{
ProcessingTypedef = TRUE;
}
void
-doneParams ()
+oldStyleDoneParams ()
{
if (ProcessingParams)
{
if (uentry_isInvalid (saveFunction))
{
llbuglit ("unsetProcessingVars: no saved function\n");
-
- if (sRefSet_isDefined (fcnModifies)) {
- sRefSet_free (fcnModifies);
- fcnModifies = sRefSet_undefined;
- }
}
else
{
- ctype ct = ctype_returnValue (uentry_getType (saveFunction));
+ ctype ct = ctype_getReturnType (uentry_getType (saveFunction));
uentryList params = uentryList_copy (saveParamList);
ctype ct2 = ctype_makeFunction (ct, params);
uentry_setType (saveFunction, ct2);
ProcessingParams = FALSE;
- reflectModGlobs (saveFunction);
- oldStyleDeclareFunction (saveFunction);
+ oldStyleCompleteFunction (saveFunction);
saveFunction = uentry_undefined;
resetGlobals ();
}
** old style declaration
*/
- ctype ct = ctype_returnValue (uentry_getType (saveFunction));
+ ctype ct = ctype_getReturnType (uentry_getType (saveFunction));
ctype ct2;
+ DPRINTF (("save function: %s", uentry_unparseFull (saveFunction)));
+
uentryList_elements (saveParamList, current)
{
uentry_setType (current, ctype_int); /* all params are ints */
}
}
+void clabstract_declareType (/*@only@*/ exprNodeList decls, /*@only@*/ warnClause warn)
+{
+ llassert (ProcessingTypedef);
+
+ if (warnClause_isDefined (warn))
+ {
+ exprNodeList_elements (decls, el)
+ {
+ uentry ue = exprNode_getUentry (el);
+ cstring uname = uentry_getName (ue);
+
+ DPRINTF (("Entry: %s", exprNode_unparse (el)));
+
+ /*
+ ** Need to lookup again to make sure we have the right one...
+ */
+
+ ue = usymtab_lookupExposeGlob (uname);
+
+ llassert (uentry_isValid (ue));
+ llassert (uentry_isDatatype (ue));
+
+ DPRINTF (("Warning for %s: %s",
+ uentry_unparse (ue), warnClause_unparse (warn)));
+
+ uentry_addWarning (ue, warnClause_copy (warn));
+ cstring_free (uname);
+ } end_exprNodeList_elements;
+ }
+
+ warnClause_free (warn);
+ exprNodeList_free (decls);
+ unsetProcessingTypedef ();
+}
+
void
unsetProcessingTypedef ()
{
void checkConstant (qtype t, idDecl id)
{
uentry e;
-
+
id = idDecl_fixBase (id, t);
e = uentry_makeIdConstant (id);
-
+
reflectStorageClass (e);
resetStorageClass ();
+ DPRINTF (("Constant: %s", uentry_unparseFull (e)));
usymtab_supGlobalEntry (e);
}
{
uentry_mergeConstantValue (ue, multiVal_copy (exprNode_getValue (e)));
}
+ else
+ {
+ DPRINTF (("No value: %s", exprNode_unparse (e)));
+ }
}
}
+ DPRINTF (("Constant value: %s", uentry_unparseFull (ue)));
usymtab_supGlobalEntry (ue);
}
-
void processNamedDecl (idDecl t)
{
if (qtype_isUndefined (processingType))
t = idDecl_fixBase (t, processingType);
DPRINTF (("Declare: %s", idDecl_unparse (t)));
-
+
if (ProcessingGlobals)
{
cstring id = idDecl_getName (t);
uentry ue = usymtab_lookupSafe (id);
-
+
if (!uentry_isValid (ue))
{
llerror (FLG_UNRECOG,
else
{
sRef sr = sRef_copy (uentry_getSref (ue));
-
reflectGlobalQualifiers (sr, idDecl_getQuals (t));
-
- currentGlobals = globSet_insert (currentGlobals, sr);
}
}
}
{
uentry cparam = uentryList_getN (saveParamList, paramno);
+ DPRINTF (("Processing param: %s", uentry_unparseFull (cparam)));
uentry_setType (cparam, idDecl_getCtype (t));
uentry_reflectQualifiers (cparam, idDecl_getQuals (t));
uentry_setDeclaredOnly (cparam, context_getSaveLocation ());
+ DPRINTF (("Processing param: %s", uentry_unparseFull (cparam)));
}
else
{
cstring_free (pname);
if (uentry_isYield (p))
- {
- e = uentry_makeParam (t, sRef_getParam (uentry_getSref (p)));
-
- uentry_checkYieldParam (p, e);
-
- usymtab_supEntrySref (e);
- return;
- }
+ {
+ e = uentry_makeParam (t, sRef_getParam (uentry_getSref (p)));
+ uentry_checkYieldParam (p, e);
+ usymtab_supEntrySref (e);
+ return;
+ }
}
-
+
if ((hasSpecialCode () || argsUsed)
&& ctype_isFunction (idDecl_getCtype (t)))
- {
+ {
e = uentry_makeIdFunction (t);
reflectSpecialCode (e);
reflectArgsUsed (e);
- }
+ }
else
- {
- e = uentry_makeIdVariable (t);
- }
-
+ {
+ e = uentry_makeIdVariable (t);
+ }
+
loc = uentry_whereDeclared (e);
-
+
/*
- if (context_inGlobalScope ())
+ if (context_inGlobalScope ())
{
uentry_checkParams was here!
}
- */
-
+ */
+
if (ctype_isFunction (uentry_getType (e)))
{
- reflectModGlobs (e);
- }
- else
- {
- llassert (!globSet_isDefined (currentGlobals)
- && !sRefSet_isDefined (fcnModifies));
+ clabstract_prepareFunction (e);
}
+ DPRINTF (("Superceding... %s", uentry_unparseFull (e)));
e = usymtab_supEntrySrefReturn (e);
-
+ DPRINTF (("After superceding... %s", uentry_unparseFull (e)));
+
if (uentry_isExtern (e) && !context_inGlobalScope ())
{
voptgenerror
uentry_setDefined (e, fileloc_getExternal ());
sRef_setDefined (uentry_getSref (e), fileloc_getExternal ());
}
-
+
if (uentry_isFunction (e))
{
- uentry_checkParams (e);
- checkParamNames (e);
+ if (!context_inXHFile ())
+ {
+ checkParamNames (e);
+ }
}
-
- if (uentry_isVar (e)
- && uentry_isCheckedUnknown (e))
+
+ if (uentry_isVar (e) && uentry_isCheckedUnknown (e))
{
sRef sr = uentry_getSref (e);
-
+
if (sRef_isLocalVar (sr))
{
if (context_getFlag (FLG_IMPCHECKMODINTERNALS))
else /* real global */
{
llassert (sRef_isRealGlobal (sr));
-
+
if (context_getFlag (FLG_IMPCHECKEDSTRICTGLOBALS))
{
uentry_setCheckedStrict (e);
{
ctype ct = idDecl_getCtype (t);
uentry e;
-
+
DPRINTF (("Processing typedef: %s", ctype_unparse (ct)));
e = uentry_makeIdDatatype (t);
checkTypeDecl (e, ct);
e = usymtab_supReturnTypeEntry (e);
-
- if (uentry_isMaybeAbstract (e))
- {
- if (context_getFlag (FLG_IMPABSTRACT))
- {
- uentry_setAbstract (e);
- }
- else
- {
- uentry_setConcrete (e);
- }
- }
}
else
{
ctype
declareUnnamedStruct (/*@only@*/ uentryList f)
{
+ DPRINTF (("Unnamed struct: %s", uentryList_unparse (f)));
+
if (context_maybeSet (FLG_NUMSTRUCTFIELDS))
{
int num = uentryList_size (f);
uentry ue;
int num = uentryList_size (f);
+ DPRINTF (("Declare struct: %s / %s", id, uentryList_unparse (f)));
+
ct = ctype_createStruct (cstring_copy (id), f);
- DPRINTF (("Declare struct: %s [%d]", ctype_unparse (ct), ct));
+
+ DPRINTF (("Ctype: %s", ctype_unparse (ct)));
+
ue = uentry_makeStructTagLoc (id, ct);
+ DPRINTF (("ue: %s", uentry_unparseFull (ue)));
+
if (context_maybeSet (FLG_NUMSTRUCTFIELDS))
{
int max = context_getValue (FLG_NUMSTRUCTFIELDS);
cstring_makeLiteral ("Old style function declaration"),
g_currentloc);
+ DPRINTF (("Handle old style params: %s", uentryList_unparseFull (params)));
+
uentryList_elements (params, current)
{
uentry_setParam (current);
- uentry_setSref (current, sRef_makeParam (paramno, ctype_unknown));
+ uentry_setSref (current, sRef_makeParam (paramno, ctype_unknown, stateInfo_makeLoc (uentry_whereLast (current))));
paramno++;
} end_uentryList_elements;
if (i >= 0)
{
- e = uentry_makeVariableSrefParam (id, c, sRef_makeParam (i, c));
+ fileloc loc = context_getSaveLocation ();
+ e = uentry_makeVariableSrefParam (id, c, loc, sRef_makeParam (i, c, stateInfo_makeLoc (loc)));
}
else
{
usymtab_supEntrySref (e);
}
-/*@exposed@*/ sRef modListPointer (sRef s)
+/*@exposed@*/ sRef modListPointer (/*@exposed@*/ sRef s)
{
ctype ct = sRef_getType (s);
ctype rt = ctype_realType (ct);
}
}
-sRef globListUnrecognized (cstring s)
+/*@dependent@*/ sRef clabstract_unrecognizedGlobal (cstring s)
{
if (cstring_equalLit (s, "nothing"))
{
}
else
{
- if (ctype_isAbstract (ct))
+ if (ctype_isAbstract (rt))
{
voptgenerror
(FLG_ABSTRACT,
message
- ("Modifies clause in header file arrow accesses abstract "
+ ("Modifies clause arrow accesses inaccessible abstract "
"type %s (interface modifies clause should not depend "
"on or expose type representation): %q",
- ctype_unparse (ct),
+ ctype_unparse (rt),
sRef_unparse (s)),
g_currentloc);
}
return s;
}
-sRef checkSpecClausesId (uentry ue)
+sRef checkStateClausesId (uentry ue)
{
cstring s = uentry_rawName (ue);
- if (sRef_isGlobal (uentry_getSref (ue)))
+ if (sRef_isFileOrGlobalScope (uentry_getSref (ue)))
{
voptgenerror
- (FLG_SYNTAX,
+ (FLG_COMMENTERROR,
message ("Global variable %s used special clause. (Global variables "
"are not recognized in special clauses. If there is "
"sufficient interest in support for this, it may be "
based on checkSpecClausesId
called by grammar
*/
+
sRef checkbufferConstraintClausesId (uentry ue)
{
cstring s = uentry_rawName (ue);
+
if (cstring_equalLit (s, "result"))
{
if (optgenerror
(FLG_SYNTAX,
- message ("Special clause list uses %s which is a variable and has special "
+ message ("Function clause list uses %s which is a variable and has special "
"meaning in a modifies list. (Special meaning assumed.)", s),
g_currentloc))
{
}
}
- return uentry_getSref (ue);
+ DPRINTF (("constrant id: %s", uentry_unparseFull (ue)));
+ return sRef_saveCopy (uentry_getSref (ue)); /*@i523 why the saveCopy? */
}
void checkModifiesId (uentry ue)
return ret;
}
-sRef fixSpecClausesId (cstring s)
+sRef fixStateClausesId (cstring s)
{
sRef ret;
cstring pname = makeParam (s);
if (cstring_equalLit (s, "result"))
{
- ret = sRef_makeResult ();
+ ret = sRef_makeResult (ctype_unknown);
}
else
{
{
voptgenerror
(FLG_SYNTAX,
- message ("Special clause uses %s which is a parameter and has special "
- "meaning in a special clause. (Special meaning assumed.)", s),
+ message ("Function clause uses %s which is a parameter and has special "
+ "meaning in a function clause. (Special meaning assumed.)", s),
g_currentloc);
}
}
{
ret = uentry_getSref (ue);
- if (sRef_isGlobal (ret))
+ if (sRef_isFileOrGlobalScope (ret))
{
voptgenerror
(FLG_SYNTAX,
- message ("Global variable %s used special clause. (Global variables "
- "are not recognized in special clauses. If there is "
+ message ("Global variable %s used in function clause. (Global variables "
+ "are not recognized in function clauses. If there is "
"sufficient interest in support for this, it may be "
"added to a future release. Send mail to "
"lclint@cs.virginia.edu.)",
voptgenerror
(FLG_UNRECOG,
- message ("Unrecognized identifier in special clause: %s", s),
+ message ("Unrecognized identifier in function clause: %s", s),
loc);
fileloc_free (loc);
return ret;
}
-sRef modListArrayFetch (sRef s, /*@unused@*/ sRef mexp)
+sRef modListArrayFetch (/*@exposed@*/ sRef s, /*@unused@*/ sRef mexp)
{
ctype ct = sRef_getType (s);
ctype rt = ctype_realType (ct);
}
}
+static void clabstract_prepareFunction (uentry e)
+{
+ uentry_checkParams (e);
+ DPRINTF (("After prepare: %s", uentry_unparseFull (e)));
+}
+sRef clabstract_checkGlobal (exprNode e)
+{
+ sRef s;
+ llassert (exprNode_isInitializer (e));
+ s = exprNode_getSref (e);
+ DPRINTF (("Initializer: %s -> %s", exprNode_unparse (e), sRef_unparse (s)));
-
-
-
-
+ exprNode_free (e);
+ return sRef_copy (s);
+}
andersk / splint.git / blobdiff