X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/4287634ef9d99c9ab7476b2937c35fabc299aca8..061ece7d6fedbde47030222fea74b575c12707dc:/src/clabstract.c diff --git a/src/clabstract.c b/src/clabstract.c index 3798ba6..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,13 +29,15 @@ */ # include "splintMacros.nf" -# include "llbasic.h" +# include "basic.h" # include "cgrammar.h" # include "usymtab_interface.h" # include "structNames.h" # include "nameChecks.h" +# include "cscannerHelp.h" + # ifdef SANITIZER # include "sgrammar_tokens.h" # else @@ -503,42 +505,43 @@ The current semantics are generated constraints of the form MaxSet(p) >= 0 and M unless the @out@ annotation has been applied to a parameter, then we only want to generate maxSet(p) > = 0 */ -void setImplictfcnConstraints (void) +void setImplicitfcnConstraints (void) { uentryList params; sRef s; constraint c; params = currentParamList; - if (constraintList_isDefined(implicitFcnConstraints) ) - constraintList_free(implicitFcnConstraints); + if (constraintList_isDefined (implicitFcnConstraints)) + { + constraintList_free (implicitFcnConstraints); + } - implicitFcnConstraints = constraintList_makeNew(); + implicitFcnConstraints = constraintList_makeNew(); uentryList_elements (params, el) { - DPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) )); + DPRINTF (("setImplicitfcnConstraints doing: %s", uentry_unparse(el))); - if ( uentry_isVariable (el) ) + if (uentry_isVariable (el)) { s = uentry_getSref(el); - if (sRef_isReference (s) ) + + 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); + implicitFcnConstraints = constraintList_add (implicitFcnConstraints , c); /*drl 10/23/2002 added support for out*/ - - if (!uentry_isOut(el) ) + + if (!uentry_isOut(el)) { c = constraint_makeSRefReadSafeInt (s, 0); - - implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c); + implicitFcnConstraints = constraintList_add (implicitFcnConstraints , c); } } else @@ -546,31 +549,24 @@ void setImplictfcnConstraints (void) DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) )); } } /*end uentry_isVariable*/ - else if (uentry_isElipsisMarker (el) ) { - /*just ignore these*/ + /* just ignore these*/ ; } else { - /*just ignore this - I'm not sure if this is possible though + /* just ignore this + I'm not sure if this is possible though */ - /*@warning take this out befor@*/ - llassert(FALSE); + ; } - } - - end_uentryList_elements; - DPRINTF((message("implicitFcnConstraints has been set to %s\n", - constraintList_print(implicitFcnConstraints) ) )); - + } end_uentryList_elements; } -/*@observer@*/ constraintList getImplicitFcnConstraints (void) +/*@observer@*/ constraintList getImplicitFcnConstraints (void) { return implicitFcnConstraints; } @@ -582,7 +578,7 @@ void setCurrentParams (/*@dependent@*/ uentryList ue) void clearCurrentParams (void) { - currentParamList = uentryList_undefined; + currentParamList = uentryList_undefined; } /* @@ -945,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."), @@ -959,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 ())); @@ -2161,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.)", @@ -2217,14 +2215,20 @@ sRef checkbufferConstraintClausesId (uentry ue) } } - DPRINTF (("constraint id: %s", uentry_unparseFull (ue))); sr = uentry_getSref (ue); - if (sRef_isInvalid (sr) ) + 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." )); + 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.")); } - return sRef_saveCopy (sr); /*@i523 why the saveCopy? */ + + /* saveCopy to used to mitigate danger of accessing freed memory*/ + return sRef_saveCopy (sr); } void checkModifiesId (uentry ue) @@ -2358,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) ); @@ -2390,8 +2396,8 @@ sRef fixStateClausesId (cstring s) return ret; } - */ -# endif + +#endif voptgenerror (FLG_UNRECOG,