/*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2000 University of Virginia,
+** 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
** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
** MA 02111-1307, USA.
**
-** 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 information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
*/
/*
** clabstract.c
**
*/
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
# include "llbasic.h"
# include "cgrammar.h"
-
-# ifndef NOLCL
# include "usymtab_interface.h"
-# endif
# include "structNames.h"
# include "nameChecks.h"
+# include "cscannerHelp.h"
+
# ifdef SANITIZER
# include "sgrammar_tokens.h"
# else
*/
/*drl*/
-/*@only@*/ static constraintList fcnConstraints = NULL;
-
-/*@only@*/ static constraintList fcnEnsuresConstraints = NULL;
-/*end drl*/
-
-/*drl */
-/*@only@*/ constraintList implicitFcnConstraints = NULL;
-
-
-//static constraintList fcnPreConditions = NULL;
-
+static /*@only@*/ constraintList implicitFcnConstraints = 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 ProcessingGlobals = FALSE;
-static bool ProcessingTypedef = FALSE;
-static bool ProcessingIterVars = FALSE;
+static void processVariable (/*@temp@*/ idDecl p_t) /*@modifies internalState@*/ ;
+
+static bool s_processingVars = FALSE;
+static bool s_processingParams = FALSE;
+static bool s_processingGlobals = FALSE;
+static bool s_processingTypedef = FALSE;
+static bool s_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)
-{
- if (fcnEnsuresConstraints != NULL)
- constraintList_free(fcnEnsuresConstraints);
- fcnEnsuresConstraints = constraintList_copy (c);
-}
-
-void setFunctionConstraints (constraintList c)
-{
- if (fcnConstraints != NULL)
- constraintList_free(fcnConstraints);
- 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);
}
extern void nextIterParam (void)
{
- llassert (ProcessingIterVars);
+ llassert (s_processingIterVars);
saveIterParamNo++;
}
extern int iterParamNo (void)
{
- llassert (ProcessingIterVars);
+ llassert (s_processingIterVars);
return saveIterParamNo;
}
static /*@dependent@*/ uentryList currentParamList;
-/*drl added 3-28-2001*/
+/*drl added 3-28-2002*/
/* 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
*/
+
+/* drl modified 10/23/2002
+
+The current semantics are generated constraints of the form MaxSet(p) >= 0 and MaxRead(p) >= 0 for all pointers
+unless the @out@ annotation has been applied to a parameter, then we only want to generate maxSet(p) > = 0
+*/
+
void setImplictfcnConstraints (void)
{
uentryList params;
constraint c;
params = currentParamList;
- if (implicitFcnConstraints != NULL)
+ 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) )
+ if ( uentry_isVariable (el) )
{
- DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
+ s = uentry_getSref(el);
+ if (sRef_isReference (s) )
+ {
+
+ DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
+ /*drl 4/26/01
+ chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0 */
+ c = constraint_makeSRefWriteSafeInt (s, 0);
+
+ implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
+
+ /*drl 10/23/2002 added support for out*/
+
+ if (!uentry_isOut(el) )
+ {
+ c = constraint_makeSRefReadSafeInt (s, 0);
+
+ implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
+ }
+ }
+ else
+ {
+ DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
+ }
+ } /*end uentry_isVariable*/
+
+ else if (uentry_isElipsisMarker (el) )
+ {
+ /*just ignore these*/
+ ;
}
+
else
{
- DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
+ /*just ignore this
+ I'm not sure if this is possible though
+ */
+ /*@warning take this out befor@*/
+ llassert(FALSE);
}
- /*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;
+ DPRINTF((message("implicitFcnConstraints has been set to %s\n",
+ constraintList_print(implicitFcnConstraints) ) ));
+
+}
+
+
+/*@observer@*/ constraintList getImplicitFcnConstraints (void)
+{
+ return implicitFcnConstraints;
}
void setCurrentParams (/*@dependent@*/ uentryList 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
{
ue = uentry_makeIdFunction (tid);
reflectSpecialCode (ue);
reflectArgsUsed (ue);
+ reflectStorageClass (ue);
+ uentry_checkParams (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);
}
else
{
- llparseerror (message ("Inconsistent function declaration: %q",
+ llparseerror (message ("Non-function declaration: %q",
idDecl_unparse (tid)));
-
- tid = idDecl_replaceCtype
- (tid, ctype_makeFunction (ctype_unknown, uentryList_undefined));
- ue = uentry_makeIdFunction (tid);
+ return (uentry_undefined);
}
-
- reflectStorageClass (ue);
-
- uentry_checkParams (ue);
- reflectModGlobs (ue);
-
- ue = usymtab_supGlobalEntryReturn (ue);
- context_enterFunction (ue);
- enterFunctionParams (uentry_getParams (ue));
-
- resetStorageClass ();
- 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;
DPRINTF (("Declare function: %s", idDecl_unparse (tid)));
- if (ProcessingParams)
+ if (ctype_isUnknown (idDecl_getCtype (tid)))
{
- ue = globalDeclareOldStyleFunction (tid);
- saveFunction = ue;
+ /*
+ ** No type, its really a plain name (int) declaration
+ */
+
+ voptgenerror (FLG_IMPTYPE,
+ message ("No type before declaration name (implicit int type): %q",
+ idDecl_unparse (tid)),
+ g_currentloc);
+ tid = idDecl_replaceCtype (tid, ctype_int);
+ processVariable (tid);
+ saveFunction = uentry_undefined;
}
else
{
- saveFunction = uentry_undefined;
-
- if (context_inRealFunction ())
+ if (s_processingParams)
{
- ue = uentry_makeVariableLoc (idDecl_observeId (tid), ctype_unknown);
-
- llparseerror (message ("Function declared inside function: %q",
- idDecl_unparse (tid)));
-
- context_quietExitFunction ();
- ue = usymtab_supEntryReturn (ue);
+ ue = globalDeclareOldStyleFunction (tid);
+ saveFunction = ue;
+ DPRINTF (("Set save function: %s", uentry_unparseFull (ue)));
}
else
{
- if (context_inInnerScope ())
+ saveFunction = uentry_undefined;
+
+ if (context_inRealFunction ())
{
- llparseerror (message ("Declaration in inner context: %q",
+ ue = uentry_makeVariableLoc (idDecl_observeId (tid), ctype_unknown);
+
+ llparseerror (message ("Function declared inside function: %q",
idDecl_unparse (tid)));
- sRef_setGlobalScope ();
- ue = uentry_makeVariableLoc (idDecl_observeId (tid),
- ctype_unknown);
- ue = usymtab_supGlobalEntryReturn (ue);
- sRef_clearGlobalScope ();
+ context_quietExitFunction ();
+ ue = usymtab_supEntryReturn (ue);
}
else
{
- ue = globalDeclareFunction (tid);
+ if (context_inInnerScope ())
+ {
+ llparseerror (message ("Declaration in inner context: %q",
+ idDecl_unparse (tid)));
+
+ sRef_setGlobalScope ();
+ ue = uentry_makeVariableLoc (idDecl_observeId (tid),
+ ctype_unknown);
+ ue = usymtab_supGlobalEntryReturn (ue);
+ sRef_clearGlobalScope ();
+ }
+ else
+ {
+ ue = clabstract_globalDeclareFunction (tid);
+ }
}
+
+ resetGlobals ();
}
-
- resetGlobals ();
+
+ resetStorageClass ();
}
- resetStorageClass ();
idDecl_free (tid);
}
DPRINTF (("Declare static funciton: %s", idDecl_unparse (tid)));
- if (ProcessingParams)
+ if (s_processingParams)
{
ue = globalDeclareOldStyleFunction (tid);
saveFunction = ue;
if (ctype_isFunction (deftype))
{
- rettype = ctype_returnValue (deftype);
+ rettype = ctype_getReturnType (deftype);
}
else
{
}
else
{
+ DPRINTF (("Here we are!"));
llparseerror (message ("Inconsistent function declaration: %q",
idDecl_unparse (tid)));
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.
uentry ue = usymtab_lookupSafe (ye);
llassert (uentry_isEitherConstant (ue));
- llassertprint (ctype_match (uentry_getType (ue), rrep),
- ("Bad enum: %s / %s",
- uentry_unparse (ue),
- ctype_unparse (rrep)));
-
- uentry_setType (ue, at);
+
+ /* evans 2002-04-22 */
+ if (ctype_isBool (uentry_getType (ue)))
+ {
+ /*
+ ** If set using -booltrue or -boolfalse, don't change the type.
+ */
+ }
+ else
+ {
+ llassertprint (ctype_match (uentry_getType (ue), rrep),
+ ("Bad enum: %s / %s",
+ uentry_unparse (ue),
+ ctype_unparse (rrep)));
+
+ uentry_setType (ue, at);
+ }
}
} end_enumNameList_elements;
}
** Microsoft VC++. It is not supported by the ANSI standard.
**
** The inner fields are added to the outer structure. This is meaningful
-** for nesting structs inside unions, but lclint does no related
+** for nesting structs inside unions, but Splint does no related
** checking.
*/
if (ctype_isStruct (ct) || ctype_isUnion (ct))
{
- uentryList res = ctype_getFields (ct);
-
- return (uentryList_copy (res));
+ return uentryList_single (uentry_makeUnnamedVariable (ct));
+ }
+ else if (ctype_isEnum (ct))
+ {
+ /* evans 2002-02-05: nothing to do for unnamed enum lists */
+ return uentryList_undefined;
}
else
- {
- BADBRANCHCONT;
+ {
+ voptgenerror
+ (FLG_SYNTAX,
+ message ("Type name in field declarations: %s", qtype_unparse (q)),
+ g_currentloc);
}
return uentryList_undefined;
void
setProcessingIterVars (uentry iter)
{
- ProcessingIterVars = TRUE;
+ s_processingIterVars = TRUE;
currentIter = iter;
saveIterParamNo = 0;
}
void
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;
- */
-
+ s_processingGlobals = TRUE;
fcnNoGlobals = FALSE;
}
static void resetGlobals (void)
{
- ProcessingGlobals = FALSE;
- currentGlobals = globSet_undefined;
- llassert (sRefSet_isUndefined (fcnModifies));
- fcnModifies = sRefSet_undefined;
+ s_processingGlobals = FALSE;
fcnNoGlobals = FALSE;
}
void
unsetProcessingGlobals ()
{
- ProcessingGlobals = FALSE;
+ s_processingGlobals = FALSE;
}
void
setProcessingVars (/*@only@*/ qtype q)
{
- ProcessingVars = TRUE;
+ s_processingVars = TRUE;
qtype_free (processingType);
processingType = q;
}
static void
setGenericParamList (/*@dependent@*/ uentryList pm)
{
- ProcessingParams = TRUE;
+ s_processingParams = TRUE;
saveParamList = pm;
}
void
-setProcessingTypedef (/*@only@*/ qtype q)
+setProcessingTypedef (qtype q)
{
- ProcessingTypedef = TRUE;
+ s_processingTypedef = TRUE;
qtype_free (processingType);
processingType = q;
unsetProcessingVars ()
{
resetStorageClass ();
- ProcessingVars = FALSE;
+ s_processingVars = FALSE;
}
void
-doneParams ()
+oldStyleDoneParams ()
{
- if (ProcessingParams)
+ if (s_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;
+ s_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 */
ct2 = ctype_makeParamsFunction (ct, uentryList_copy (saveParamList));
uentry_setType (saveFunction, ct2);
- ProcessingParams = FALSE;
+ s_processingParams = FALSE;
oldStyleDeclareFunction (saveFunction);
saveFunction = uentry_undefined;
}
}
+void clabstract_declareType (/*@only@*/ exprNodeList decls, /*@only@*/ warnClause warn)
+{
+ llassert (s_processingTypedef);
+
+ DPRINTF (("Declare type: %s", exprNodeList_unparse (decls)));
+
+ if (warnClause_isDefined (warn))
+ {
+ DPRINTF (("Has a warn clause!"));
+ DPRINTF (("Warn: %s", warnClause_unparse (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));
+ DPRINTF (("After add warning: %s", uentry_unparseFull (ue)));
+ cstring_free (uname);
+ } end_exprNodeList_elements;
+ }
+
+ warnClause_free (warn);
+ exprNodeList_free (decls);
+ unsetProcessingTypedef ();
+}
+
void
unsetProcessingTypedef ()
{
- ProcessingTypedef = FALSE;
+ s_processingTypedef = FALSE;
}
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);
}
+static void processVariable (idDecl t)
+{
+ uentry e;
+ ctype ct;
+
+ ct = ctype_realType (idDecl_getCtype (t));
+
+ if (s_processingParams)
+ {
+ cstring id = idDecl_getName (t);
+ int paramno = uentryList_lookupRealName (saveParamList, id);
+
+ if (paramno >= 0)
+ {
+ 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
+ {
+ llfatalerrorLoc
+ (message ("Old style declaration uses unlisted parameter: %s",
+ id));
+ }
+ }
+ else
+ {
+ fileloc loc;
+
+ if (context_inIterDef ())
+ {
+ cstring pname = makeParam (idDecl_observeId (t));
+ uentry p = usymtab_lookupSafe (pname);
+
+ cstring_free (pname);
+
+ if (uentry_isYield (p))
+ {
+ 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);
+ }
+
+ loc = uentry_whereDeclared (e);
+
+ /*
+ if (context_inGlobalScope ())
+ {
+ uentry_checkParams was here!
+ }
+ */
+
+ if (ctype_isFunction (uentry_getType (e)))
+ {
+ 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
+ (FLG_NESTEDEXTERN,
+ message ("Declaration using extern inside function scope: %q",
+ uentry_unparse (e)),
+ g_currentloc);
+
+ uentry_setDefined (e, fileloc_getExternal ());
+ sRef_setDefined (uentry_getSref (e), fileloc_getExternal ());
+ }
+
+ if (uentry_isFunction (e))
+ {
+ if (!context_inXHFile ())
+ {
+ checkParamNames (e);
+ }
+ }
+
+ if (uentry_isVar (e) && uentry_isCheckedUnknown (e))
+ {
+ sRef sr = uentry_getSref (e);
+
+ if (sRef_isLocalVar (sr))
+ {
+ if (context_getFlag (FLG_IMPCHECKMODINTERNALS))
+ {
+ uentry_setCheckMod (e);
+ }
+ else
+ {
+ uentry_setUnchecked (e);
+ }
+ }
+ else if (sRef_isFileStatic (sr))
+ {
+ if (context_getFlag (FLG_IMPCHECKEDSTRICTSTATICS))
+ {
+ uentry_setCheckedStrict (e);
+ }
+ else if (context_getFlag (FLG_IMPCHECKEDSTATICS))
+ {
+ uentry_setChecked (e);
+ }
+ else if (context_getFlag (FLG_IMPCHECKMODSTATICS))
+ {
+ uentry_setCheckMod (e);
+ }
+ else
+ {
+ ;
+ }
+ }
+ else /* real global */
+ {
+ llassert (sRef_isRealGlobal (sr));
+
+ if (context_getFlag (FLG_IMPCHECKEDSTRICTGLOBALS))
+ {
+ uentry_setCheckedStrict (e);
+ }
+ else if (context_getFlag (FLG_IMPCHECKEDGLOBALS))
+ {
+ uentry_setChecked (e);
+ }
+ else if (context_getFlag (FLG_IMPCHECKMODGLOBALS))
+ {
+ uentry_setCheckMod (e);
+ }
+ else
+ {
+ ;
+ }
+ }
+ }
+ }
+}
void processNamedDecl (idDecl t)
{
if (qtype_isUndefined (processingType))
{
- llparseerror (message ("No type before declaration name: %q", idDecl_unparse (t)));
+ processingType = qtype_create (ctype_int);
+ t = idDecl_fixBase (t, processingType);
- processingType = qtype_create (ctype_unknown);
+ voptgenerror (FLG_IMPTYPE,
+ message ("No type before declaration name (implicit int type): %q",
+ idDecl_unparse (t)),
+ g_currentloc);
+ }
+ else
+ {
+ t = idDecl_fixBase (t, processingType);
}
-
- t = idDecl_fixBase (t, processingType);
DPRINTF (("Declare: %s", idDecl_unparse (t)));
-
- if (ProcessingGlobals)
+
+ if (s_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);
}
}
}
- else if (ProcessingVars)
+ else if (s_processingVars)
{
- uentry e;
- ctype ct;
-
- ct = ctype_realType (idDecl_getCtype (t));
-
- if (ProcessingParams)
- {
- cstring id = idDecl_getName (t);
- int paramno = uentryList_lookupRealName (saveParamList, id);
-
- if (paramno >= 0)
- {
- uentry cparam = uentryList_getN (saveParamList, paramno);
-
- uentry_setType (cparam, idDecl_getCtype (t));
- uentry_reflectQualifiers (cparam, idDecl_getQuals (t));
- uentry_setDeclaredOnly (cparam, context_getSaveLocation ());
- }
- else
- {
- llfatalerrorLoc
- (message ("Old style declaration uses unlisted parameter: %s",
- id));
- }
- }
- else
- {
- fileloc loc;
-
- if (context_inIterDef ())
- {
- cstring pname = makeParam (idDecl_observeId (t));
- uentry p = usymtab_lookupSafe (pname);
-
- cstring_free (pname);
-
- if (uentry_isYield (p))
- {
- 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);
- }
-
- loc = uentry_whereDeclared (e);
-
- /*
- if (context_inGlobalScope ())
- {
- uentry_checkParams was here!
- }
- */
-
- if (ctype_isFunction (uentry_getType (e)))
- {
- reflectModGlobs (e);
- }
- else
- {
- llassert (!globSet_isDefined (currentGlobals)
- && !sRefSet_isDefined (fcnModifies));
- }
-
- e = usymtab_supEntrySrefReturn (e);
-
- if (uentry_isExtern (e) && !context_inGlobalScope ())
- {
- voptgenerror
- (FLG_NESTEDEXTERN,
- message ("Declaration using extern inside function scope: %q",
- uentry_unparse (e)),
- g_currentloc);
-
- uentry_setDefined (e, fileloc_getExternal ());
- sRef_setDefined (uentry_getSref (e), fileloc_getExternal ());
- }
-
- if (uentry_isFunction (e))
- {
- uentry_checkParams (e);
- checkParamNames (e);
- }
-
- if (uentry_isVar (e)
- && uentry_isCheckedUnknown (e))
- {
- sRef sr = uentry_getSref (e);
-
- if (sRef_isLocalVar (sr))
- {
- if (context_getFlag (FLG_IMPCHECKMODINTERNALS))
- {
- uentry_setCheckMod (e);
- }
- else
- {
- uentry_setUnchecked (e);
- }
- }
- else if (sRef_isFileStatic (sr))
- {
- if (context_getFlag (FLG_IMPCHECKEDSTRICTSTATICS))
- {
- uentry_setCheckedStrict (e);
- }
- else if (context_getFlag (FLG_IMPCHECKEDSTATICS))
- {
- uentry_setChecked (e);
- }
- else if (context_getFlag (FLG_IMPCHECKMODSTATICS))
- {
- uentry_setCheckMod (e);
- }
- else
- {
- ;
- }
- }
- else /* real global */
- {
- llassert (sRef_isRealGlobal (sr));
-
- if (context_getFlag (FLG_IMPCHECKEDSTRICTGLOBALS))
- {
- uentry_setCheckedStrict (e);
- }
- else if (context_getFlag (FLG_IMPCHECKEDGLOBALS))
- {
- uentry_setChecked (e);
- }
- else if (context_getFlag (FLG_IMPCHECKMODGLOBALS))
- {
- uentry_setCheckMod (e);
- }
- else
- {
- ;
- }
- }
- }
- }
+ processVariable (t);
}
- else if (ProcessingTypedef)
+ else if (s_processingTypedef)
{
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);
ctype
declareUnnamedUnion (/*@only@*/ uentryList f)
{
+ DPRINTF (("Unnamed union: %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 [%d]", id, uentryList_unparse (f),
+ uentryList_size (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);
}
else
{
- return (declareEnum (id, enumNameList_new ()));
+ return (ctype_createForwardEnum (id));
}
}
bool processingIterVars (void)
{
- return ProcessingIterVars;
+ return s_processingIterVars;
}
uentry getCurrentIter (void)
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), SA_DECLARED)));
paramno++;
} end_uentryList_elements;
setGenericParamList (params);
- g_expectingTypeName = TRUE;
+ cscannerHelp_setExpectingTypeName ();
return params;
}
setGenericParamList (params);
flipOldStyle = FALSE;
- g_expectingTypeName = TRUE;
+ cscannerHelp_setExpectingTypeName ();
}
return (params);
cstring id = cstring_makeLiteral ("va_alist");
uentry e;
- if (ProcessingParams)
+ if (s_processingParams)
{
int i = uentryList_lookupRealName (saveParamList, id);
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, SA_DECLARED)));
}
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,
- message ("Global variable %s used special clause. (Global variables "
- "are not recognized in special clauses. If there is "
+ (FLG_COMMENTERROR,
+ message ("Global variable %s used state clause. (Global variables "
+ "are not recognized in state clauses. If they are present "
+ "they are ignored. "
+ " If there is "
"sufficient interest in support for this, it may be "
"added to a future release. Send mail to "
- "lclint@cs.virginia.edu.)",
+ "info@splint.org.)",
s),
g_currentloc);
based on checkSpecClausesId
called by grammar
*/
+
sRef checkbufferConstraintClausesId (uentry ue)
{
+ sRef sr;
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 sRef_copy( uentry_getSref (ue) );
+ DPRINTF (("constraint id: %s", uentry_unparseFull (ue)));
+ sr = uentry_getSref (ue);
+
+ if (sRef_isInvalid (sr) )
+ {
+ llfatalerrorLoc (cstring_makeLiteral("Macro defined constants can not be used in function constraints unless they are specifed with the constant annotation. To use a macro defined constant include an annotation of the form /*@constant <type> <name>=<value>@*/ somewhere before the function constraint. This restriction may be removed in future releases if it is determined to be excessively burdensome." ));
+ }
+
+ /*@ savedCopy to used to mitigate danger of accessing freed memory*/
+ return sRef_saveCopy (sr);
}
void checkModifiesId (uentry ue)
}
else
{
- fileloc loc = fileloc_decColumn (g_currentloc, cstring_length (s));
+ fileloc loc = fileloc_decColumn (g_currentloc, size_toInt (cstring_length (s)));
ret = sRef_undefined;
voptgenerror
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.)",
+ "info@splint.org.)",
s),
g_currentloc);
}
else
{
- fileloc loc = fileloc_decColumn (g_currentloc, cstring_length (s));
+
+ /* drl This is the code for structure invariants
+
+ It is no yet stable enough to be included in a Splint release.
+ */
+
+ /*check that we're in a structure */
+#if 0
+ /*@unused@*/ uentryList ueL;
+ /*@unused@*/ uentry ue2;
+ /*@unused@*/ ctype ct;\r
+#endif
+ fileloc loc = fileloc_decColumn (g_currentloc, size_toInt (cstring_length (s)));
ret = sRef_undefined;
+# if 0
+ ct = context_getLastStruct ( ct );
+
+ llassert( ctype_isStruct(ct) );
+
+ ueL = ctype_getFields (ct);
+
+ ue2 = uentryList_lookupField (ueL, s);
+
+ if (!uentry_isUndefined(ue2) )
+ {
+ ret = uentry_getSref(ue2);
+
+ DPRINTF((
+ message("Got field in structure in the annotation constraint: %s (or sref: %s)", s, sRef_unparse(ret) )
+ ));
+
+ return ret;
+ }
+
+#endif
+
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