X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/2cecdaff4e89d020d2500eab63b6fe6caa537788..061ece7d6fedbde47030222fea74b575c12707dc:/src/clabstract.c diff --git a/src/clabstract.c b/src/clabstract.c index db7300c..3bf4168 100644 --- a/src/clabstract.c +++ b/src/clabstract.c @@ -1,6 +1,6 @@ /* ** Splint - annotation-assisted static program checker -** Copyright (C) 1994-2002 University of Virginia, +** Copyright (C) 1994-2003 University of Virginia, ** Massachusetts Institute of Technology ** ** This program is free software; you can redistribute it and/or modify it @@ -29,16 +29,15 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.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 @@ -498,46 +497,76 @@ static /*@dependent@*/ uentryList currentParamList; /*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 */ -void setImplictfcnConstraints (void) +/* 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 setImplicitfcnConstraints (void) { uentryList params; sRef s; constraint c; params = currentParamList; - if (constraintList_isDefined(implicitFcnConstraints) ) - constraintList_free(implicitFcnConstraints); - - implicitFcnConstraints = constraintList_makeNew(); + if (constraintList_isDefined (implicitFcnConstraints)) + { + constraintList_free (implicitFcnConstraints); + } + + implicitFcnConstraints = constraintList_makeNew(); uentryList_elements (params, el) { - DPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) )); + DPRINTF (("setImplicitfcnConstraints doing: %s", uentry_unparse(el))); - s = uentry_getSref(el); - if (sRef_isReference (s) ) + if (uentry_isVariable (el)) + { + 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) ) { - DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) )); + /* 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 + */ + ; } - /*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; + } end_uentryList_elements; } -/*@observer@*/ constraintList getImplicitFcnConstraints (void) +/*@observer@*/ constraintList getImplicitFcnConstraints (void) { return implicitFcnConstraints; } @@ -549,7 +578,7 @@ void setCurrentParams (/*@dependent@*/ uentryList ue) void clearCurrentParams (void) { - currentParamList = uentryList_undefined; + currentParamList = uentryList_undefined; } /* @@ -912,8 +941,8 @@ checkTypeDecl (uentry e, ctype rep) vgenhinterror (FLG_SYNTAX, message ("Member of boolean enumerated type definition " - "does not match name set to represent TRUE " - "or FALSE: %s", + "does not match name set to represent true " + "or false: %s", ye), message ("Use -boolfalse and -booltrue to set the " "name of false and true boolean values."), @@ -926,7 +955,7 @@ checkTypeDecl (uentry e, ctype rep) if (usymtab_exists (n)) { usymId llm = usymtab_getId (n); - uentry le = usymtab_getTypeEntry (llm); + uentry le = usymtab_getTypeEntry (typeId_fromUsymId (llm)); uentry_setDeclared (e, g_currentloc); uentry_setSref (e, sRef_makeGlobal (llm, uentry_getType (le), stateInfo_currentLoc ())); @@ -1810,7 +1839,7 @@ handleEnum (cstring id) } else { - return (declareEnum (id, enumNameList_new ())); + return (ctype_createForwardEnum (id)); } } @@ -1850,12 +1879,14 @@ void setNewStyle () { flipNewStyle = TRUE; } uentryList_elements (params, current) { uentry_setParam (current); - uentry_setSref (current, sRef_makeParam (paramno, ctype_unknown, stateInfo_makeLoc (uentry_whereLast (current)))); + 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; } @@ -1872,7 +1903,7 @@ void setNewStyle () { flipNewStyle = TRUE; } setGenericParamList (params); flipOldStyle = FALSE; - g_expectingTypeName = TRUE; + cscannerHelp_setExpectingTypeName (); } return (params); @@ -1892,7 +1923,9 @@ doVaDcl () if (i >= 0) { fileloc loc = context_getSaveLocation (); - e = uentry_makeVariableSrefParam (id, c, loc, sRef_makeParam (i, c, stateInfo_makeLoc (loc))); + e = uentry_makeVariableSrefParam + (id, c, loc, + sRef_makeParam (i, c, stateInfo_makeLoc (loc, SA_DECLARED))); } else { @@ -2124,7 +2157,9 @@ sRef checkStateClausesId (uentry ue) voptgenerror (FLG_COMMENTERROR, message ("Global variable %s used state clause. (Global variables " - "are not recognized in state clauses. If there is " + "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 " "info@splint.org.)", @@ -2165,6 +2200,7 @@ sRef checkStateClausesId (uentry ue) sRef checkbufferConstraintClausesId (uentry ue) { + sRef sr; cstring s = uentry_rawName (ue); if (cstring_equalLit (s, "result")) @@ -2179,8 +2215,20 @@ sRef checkbufferConstraintClausesId (uentry ue) } } - DPRINTF (("constrant id: %s", uentry_unparseFull (ue))); - return sRef_saveCopy (uentry_getSref (ue)); /*@i523 why the saveCopy? */ + 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.")); + } + + /* saveCopy to used to mitigate danger of accessing freed memory*/ + return sRef_saveCopy (sr); } void checkModifiesId (uentry ue) @@ -2314,20 +2362,22 @@ sRef fixStateClausesId (cstring s) } else { - /*@i222@*/ - /*drl handle structure invariant */ - /*@i222@*/ + /* 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 +#if 0 /*@unused@*/ uentryList ueL; /*@unused@*/ uentry ue2; /*@unused@*/ ctype ct; -# endif +#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) ); @@ -2346,8 +2396,8 @@ sRef fixStateClausesId (cstring s) return ret; } - */ -# endif + +#endif voptgenerror (FLG_UNRECOG,