X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/c3e695ffb52ea08e5464cccde162a94e4568d208..312c981596ce6202de7686f2d4c46aec1bae3939:/src/clabstract.c diff --git a/src/clabstract.c b/src/clabstract.c index 718c775..a47ca84 100644 --- a/src/clabstract.c +++ b/src/clabstract.c @@ -1,6 +1,6 @@ /* -** LCLint - annotation-assisted static program checker -** Copyright (C) 1994-2000 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 @@ -17,9 +17,9 @@ ** 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 @@ -28,13 +28,10 @@ ** */ -# 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" @@ -52,29 +49,19 @@ */ /*drl*/ -/*@only@*/ static constraintList fcnConstraints = NULL; - -/*@only@*/ static constraintList fcnEnsuresConstraints = NULL; -/*end drl*/ - -/*drl */ -/*@only@*/ constraintList implicitFcnConstraints = NULL; +static /*@only@*/ constraintList implicitFcnConstraints = NULL; - -//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 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; @@ -84,12 +71,18 @@ static /*@dependent@*/ fileloc saveStoreLoc = fileloc_undefined; 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) @@ -125,7 +118,7 @@ static void reflectArgsUsed (uentry ue) extern void setSpecialFunction (qual qu) { - if (specialFunctionCode != QU_UNKNOWN) + if (!qual_isUnknown (specialFunctionCode)) { voptgenerror (FLG_SYNTAX, message ("Multiple special function codes: %s, %s " @@ -140,22 +133,19 @@ extern void setSpecialFunction (qual qu) 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) @@ -165,52 +155,6 @@ 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) @@ -235,99 +179,14 @@ void storeLoc () 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 */ @@ -346,6 +205,7 @@ static void reflectGlobalQualifiers (sRef sr, qualList quals) } sRef_setDefState (sr, defstate, fileloc_undefined); + DPRINTF (("State: %s", sRef_unparseFull (sr))); } else if (qual_isAllocQual (qel)) /* out, partial, reldef, etc. */ { @@ -401,15 +261,24 @@ static void reflectGlobalQualifiers (sRef sr, qualList quals) } 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) @@ -421,21 +290,18 @@ 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; } @@ -626,11 +492,17 @@ declareEnumList (enumNameList el, ctype c, fileloc loc) 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; @@ -638,6 +510,9 @@ void setImplictfcnConstraints (void) constraint c; params = currentParamList; + if (constraintList_isDefined(implicitFcnConstraints) ) + constraintList_free(implicitFcnConstraints); + implicitFcnConstraints = constraintList_makeNew(); uentryList_elements (params, el) @@ -654,13 +529,30 @@ void setImplictfcnConstraints (void) DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) )); } /*drl 4/26/01 - chagned this is MaxSet(s) == 0 to MaxSet(s) >= 0 */ - + chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0 */ c = constraint_makeSRefWriteSafeInt (s, 0); - // constraint_makeSRefSetBufferSize (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); + } + + } 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) @@ -706,17 +598,17 @@ extern void exitParamsTemp (void) 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 { @@ -732,28 +624,28 @@ static /*@exposed@*/ uentry globalDeclareFunction (idDecl tid) 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); } /* @@ -779,15 +671,11 @@ static /*@only@*/ uentry globalDeclareOldStyleFunction (idDecl tid) 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); } @@ -798,6 +686,13 @@ static void oldStyleDeclareFunction (/*@only@*/ uentry 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_enterFunction (e); @@ -806,54 +701,95 @@ static void oldStyleDeclareFunction (/*@only@*/ uentry 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); } @@ -863,7 +799,7 @@ void declareStaticFunction (idDecl tid) /*@globals undef saveFunction; @*/ DPRINTF (("Declare static funciton: %s", idDecl_unparse (tid))); - if (ProcessingParams) + if (s_processingParams) { ue = globalDeclareOldStyleFunction (tid); saveFunction = ue; @@ -902,7 +838,7 @@ void declareStaticFunction (idDecl tid) /*@globals undef saveFunction; @*/ if (ctype_isFunction (deftype)) { - rettype = ctype_returnValue (deftype); + rettype = ctype_getReturnType (deftype); } else { @@ -921,6 +857,7 @@ void declareStaticFunction (idDecl tid) /*@globals undef saveFunction; @*/ } else { + DPRINTF (("Here we are!")); llparseerror (message ("Inconsistent function declaration: %q", idDecl_unparse (tid))); @@ -933,7 +870,6 @@ void declareStaticFunction (idDecl tid) /*@globals undef saveFunction; @*/ uentry_setStatic (ue); uentry_checkParams (ue); - reflectModGlobs (ue); DPRINTF (("Sub global entry: %s", uentry_unparse (ue))); ue = usymtab_supGlobalEntryReturn (ue); @@ -956,7 +892,7 @@ checkTypeDecl (uentry e, ctype rep) { 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)) { @@ -1006,7 +942,7 @@ checkTypeDecl (uentry e, ctype rep) 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 ())); @@ -1015,6 +951,8 @@ checkTypeDecl (uentry e, ctype rep) { 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. @@ -1032,12 +970,23 @@ checkTypeDecl (uentry e, ctype rep) 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; } @@ -1169,7 +1118,7 @@ fixUentryList (idDeclList tl, qtype q) ** 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. */ @@ -1180,13 +1129,19 @@ fixUnnamedDecl (qtype q) 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; @@ -1200,7 +1155,7 @@ void setStorageClass (storageClassCode sc) void setProcessingIterVars (uentry iter) { - ProcessingIterVars = TRUE; + s_processingIterVars = TRUE; currentIter = iter; saveIterParamNo = 0; } @@ -1208,20 +1163,7 @@ setProcessingIterVars (uentry iter) 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; } @@ -1247,23 +1189,20 @@ isProcessingGlobMods () 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; } @@ -1271,14 +1210,14 @@ setProcessingVars (/*@only@*/ qtype 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; @@ -1288,34 +1227,28 @@ void 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 (); } @@ -1340,9 +1273,11 @@ checkDoneParams () ** 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 */ @@ -1351,29 +1286,71 @@ checkDoneParams () 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); } @@ -1406,31 +1383,199 @@ void checkValueConstant (qtype t, idDecl id, exprNode 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, @@ -1451,177 +1596,19 @@ void processNamedDecl (idDecl t) 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); @@ -1652,18 +1639,6 @@ void processNamedDecl (idDecl 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 { @@ -1701,6 +1676,8 @@ static idDecl fixStructDecl (/*@returned@*/ idDecl d) ctype declareUnnamedStruct (/*@only@*/ uentryList f) { + DPRINTF (("Unnamed struct: %s", uentryList_unparse (f))); + if (context_maybeSet (FLG_NUMSTRUCTFIELDS)) { int num = uentryList_size (f); @@ -1723,6 +1700,8 @@ declareUnnamedStruct (/*@only@*/ uentryList f) ctype declareUnnamedUnion (/*@only@*/ uentryList f) { + DPRINTF (("Unnamed union: %s", uentryList_unparse (f))); + if (context_maybeSet (FLG_NUMSTRUCTFIELDS)) { int num = uentryList_size (f); @@ -1748,10 +1727,17 @@ ctype declareStruct (cstring id, /*@only@*/ uentryList 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); @@ -1837,13 +1823,13 @@ handleEnum (cstring id) } else { - return (declareEnum (id, enumNameList_new ())); + return (ctype_createForwardEnum (id)); } } bool processingIterVars (void) { - return ProcessingIterVars; + return s_processingIterVars; } uentry getCurrentIter (void) @@ -1872,10 +1858,12 @@ void setNewStyle () { flipNewStyle = TRUE; } 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; @@ -1910,13 +1898,14 @@ doVaDcl () 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))); } else { @@ -1935,7 +1924,7 @@ doVaDcl () usymtab_supEntrySref (e); } -/*@exposed@*/ sRef modListPointer (sRef s) +/*@exposed@*/ sRef modListPointer (/*@exposed@*/ sRef s) { ctype ct = sRef_getType (s); ctype rt = ctype_realType (ct); @@ -2026,7 +2015,7 @@ doVaDcl () } } -sRef globListUnrecognized (cstring s) +/*@dependent@*/ sRef clabstract_unrecognizedGlobal (cstring s) { if (cstring_equalLit (s, "nothing")) { @@ -2096,15 +2085,15 @@ sRef globListUnrecognized (cstring s) } 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); } @@ -2139,19 +2128,19 @@ sRef globListUnrecognized (cstring s) 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 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); @@ -2186,14 +2175,17 @@ sRef checkSpecClausesId (uentry ue) 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)) { @@ -2201,7 +2193,14 @@ sRef checkbufferConstraintClausesId (uentry ue) } } - 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 =@*/ somewhere before the function constraint. This restriction may be removed in future releases if it is determined to be excessively burdensome." )); + } + return sRef_saveCopy (sr); /*@i523 why the saveCopy? */ } void checkModifiesId (uentry ue) @@ -2269,7 +2268,7 @@ 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 @@ -2284,7 +2283,7 @@ void checkModifiesId (uentry ue) return ret; } -sRef fixSpecClausesId (cstring s) +sRef fixStateClausesId (cstring s) { sRef ret; cstring pname = makeParam (s); @@ -2294,7 +2293,7 @@ sRef fixSpecClausesId (cstring s) if (cstring_equalLit (s, "result")) { - ret = sRef_makeResult (); + ret = sRef_makeResult (ctype_unknown); } else { @@ -2307,8 +2306,8 @@ sRef fixSpecClausesId (cstring s) { 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); } } @@ -2318,15 +2317,15 @@ sRef fixSpecClausesId (cstring s) { 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); @@ -2335,12 +2334,44 @@ sRef fixSpecClausesId (cstring s) } else { - fileloc loc = fileloc_decColumn (g_currentloc, cstring_length (s)); + /*@i222@*/ + /*drl handle structure invariant */ + + /*@i222@*/ + /*check that we're in a structure */ +# if 0 + /*@unused@*/ uentryList ueL; + /*@unused@*/ uentry ue2; + /*@unused@*/ ctype ct; +# endif + fileloc loc = fileloc_decColumn (g_currentloc, size_toInt (cstring_length (s))); ret = sRef_undefined; - +# if 0 + /*drl commenting this out for now + 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); @@ -2350,7 +2381,7 @@ sRef fixSpecClausesId (cstring s) 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); @@ -2384,10 +2415,20 @@ sRef modListArrayFetch (sRef s, /*@unused@*/ sRef mexp) } } +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); +}