From 517a2db3da924ba77ae313404da5e12fda798947 Mon Sep 17 00:00:00 2001 From: evans1629 Date: Tue, 22 Apr 2003 01:25:49 +0000 Subject: [PATCH] Fixes after removing -unrecogcomments flag for make splintme. --- src/Headers/constraintList.h | 2 +- src/Headers/cstring.h | 14 ++-- src/Headers/cstringTable.h | 4 +- src/Headers/exprNode.h | 4 - src/Headers/fileTable.h | 2 +- src/Headers/flagSpec.h | 2 +- src/Headers/forwardTypes.h | 4 +- src/Headers/functionClause.h | 2 +- src/Headers/functionClauseList.h | 2 +- src/Headers/genericTable.h | 2 +- src/Headers/llerror.h | 22 +++--- src/Headers/mtDeclarationPiece.h | 2 +- src/Headers/mtDefaultsDeclList.h | 2 +- src/Headers/mtLoseReferenceList.h | 2 +- src/Headers/mtMergeClauseList.h | 2 +- src/Headers/mtTransferClauseList.h | 2 +- src/Headers/osd.h | 4 +- src/Makefile.am | 2 +- src/Makefile.in | 2 +- src/clabstract.c | 60 +++++++-------- src/constraint.c | 120 +++++++++++------------------ src/constraintGeneration.c | 64 ++++++--------- src/constraintList.c | 31 ++++---- src/constraintTerm.c | 10 +-- src/context.c | 4 +- src/cscannerHelp.c | 3 - src/ctbase.i | 2 +- src/exprNode.c | 21 ++--- src/lh.c | 4 +- src/llerror.c | 107 +++++++++++++------------ src/osd.c | 6 +- src/stateClauseList.c | 2 +- src/transferChecks.c | 2 - src/uentry.c | 7 +- src/usymtab.c | 7 +- test/Makefile.am | 1 - test/Makefile.in | 1 - test/help.expect | 2 - 38 files changed, 232 insertions(+), 300 deletions(-) diff --git a/src/Headers/constraintList.h b/src/Headers/constraintList.h index 94b190f..dc8861c 100644 --- a/src/Headers/constraintList.h +++ b/src/Headers/constraintList.h @@ -83,7 +83,7 @@ extern /*@only@*/ constraintList constraintList_makeFixedArrayConstraints ( /*@o extern void constraintList_printErrorPostConditions (constraintList p_s, fileloc p_loc) ; extern void constraintList_printError (constraintList p_s, /*@observer@*/ fileloc p_loc) ; -extern constraintList constraintList_sort (/*@returned@*/ constraintList p_ret) /*@modifes p_ref@*/ ; +extern constraintList constraintList_sort (/*@returned@*/ constraintList p_ret) /*@modifies p_ret@*/ ; void constraintList_dump (/*@observer@*/ constraintList p_c, FILE * p_f); diff --git a/src/Headers/cstring.h b/src/Headers/cstring.h index 3360072..e325010 100644 --- a/src/Headers/cstring.h +++ b/src/Headers/cstring.h @@ -67,8 +67,8 @@ extern void cstring_setChar (cstring p_s, size_t p_n, char p_c) # define cstring_secondChar(s) cstring_getChar (s, 2) extern /*@exposed@*/ /*@notnull@*/ /*@untainted@*/ char * - cstring_toCharsSafe (/*@temp@*/ /*@exposed@*/ /*@returned@*/ cstring p_s) - /*@*/ ; +cstring_toCharsSafe (/*@temp@*/ /*@exposed@*/ /*@returned@*/ cstring p_s) + /*@*/ ; extern size_t cstring_length (cstring p_s) /*@*/ /*@ensures result == maxRead(p_s) @*/; @@ -112,17 +112,17 @@ extern bool cstring_equalFree (/*@only@*/ cstring p_c1, /*@only@*/ cstring p_c2) ** Don't allow tainted cstring's */ -extern /*@untained@*/ cstring - cstring_fromChars (/*@returned@*/ /*@null@*/ - const /*:untainted@*/ /*@exposed@*/ /*@temp@*/ char *p_cp) /*@*/ ; +extern cstring +cstring_fromChars (/*@returned@*/ /*@null@*/ + const /*@exposed@*/ /*@temp@*/ char *p_cp) /*@*/ ; extern cstring - cstring_fromCharsO (/*@null@*/ /*:untainted@*/ /*@only@*/ char *p_cp) /*@*/ ; +cstring_fromCharsO (/*@null@*/ /*@only@*/ char *p_cp) /*@*/ ; /*@-mustfree@*/ # define cstring_fromCharsO(s) cstring_fromChars(s) /*@=mustfree@*/ -extern cstring cstring_fromCharsNew (/*:untainted@*/ /*@null@*/ char *p_s) /*@*/ ; +extern cstring cstring_fromCharsNew (/*@null@*/ char *p_s) /*@*/ ; # define cstring_fromCharsNew(s) cstring_copy(cstring_fromChars(s)) extern /*@exposed@*/ /*@notnull@*/ /*@untainted@*/ diff --git a/src/Headers/cstringTable.h b/src/Headers/cstringTable.h index 1369200..0f798c6 100644 --- a/src/Headers/cstringTable.h +++ b/src/Headers/cstringTable.h @@ -20,13 +20,13 @@ abst_typedef null struct _cstringTable *cstringTable; */ -/*@private@*/ typedef struct +/*:private:*/ typedef struct { /*@only@*/ cstring key; int val; } *hentry; -/*@private@*/ typedef /*@only@*/ hentry o_hentry; +/*:private:*/ typedef /*@only@*/ hentry o_hentry; typedef /*@null@*/ struct { diff --git a/src/Headers/exprNode.h b/src/Headers/exprNode.h index 421550c..12ae15a 100644 --- a/src/Headers/exprNode.h +++ b/src/Headers/exprNode.h @@ -375,10 +375,6 @@ extern void exprNode_freeShallow (/*@only@*/ exprNode p_e); extern void exprNode_destroyMod (void) /*@modifies internalState@*/ ; extern /*@falsewhennull@*/ bool exprNode_isAssign (exprNode p_e) /*@*/ ; -/* added 8-15-00 - by DRL */ -extern /*@observer@*/ fileloc exprNode_getfileloc (exprNode p_e) ; - /*@-exportlocal@*/ extern bool exprNode_isDefaultMarker (exprNode p_e) /*@*/ ; extern bool exprNode_isCaseMarker (exprNode p_e) /*@*/ ; diff --git a/src/Headers/fileTable.h b/src/Headers/fileTable.h index d5ec489..607bec1 100644 --- a/src/Headers/fileTable.h +++ b/src/Headers/fileTable.h @@ -20,7 +20,7 @@ typedef enum { FILE_NORMAL, FILE_LSLTEMP, FILE_NODELETE, FILE_HEADER, FILE_XH, FILE_MACROS, FILE_METASTATE } fileType; -/*@private@*/ typedef struct +/*:private:*/ typedef struct { bool ftemp BOOLBITS; bool fsystem BOOLBITS; diff --git a/src/Headers/flagSpec.h b/src/Headers/flagSpec.h index 79019b8..52f3990 100644 --- a/src/Headers/flagSpec.h +++ b/src/Headers/flagSpec.h @@ -10,7 +10,7 @@ # ifndef flagSpec_H # define flagSpec_H -/*@private@*/ typedef struct +/*:private:*/ typedef struct { cstring name; flagcode code; diff --git a/src/Headers/forwardTypes.h b/src/Headers/forwardTypes.h index b55a8d2..36a417b 100644 --- a/src/Headers/forwardTypes.h +++ b/src/Headers/forwardTypes.h @@ -5,7 +5,9 @@ # ifdef WIN32 /* Microsoft doesn't support ISO C99 yet */ +/*@-namechecks@*/ typedef int bool; +/*@=namechecks@*/ # endif abst_typedef /*@null@*/ struct s_sRef *sRef; @@ -82,7 +84,7 @@ abst_typedef /*@null@*/ ctypeList fileIdList; abst_typedef /*@null@*/ struct s_constraintExpr *constraintExpr; -abst_typedef /*@untainted@*/ /*@null@*/ char *cstring; +abst_typedef /*@null@*/ char *cstring; typedef /*@only@*/ cstring o_cstring; abst_typedef /*@null@*/ struct s_cstringSList *cstringSList; diff --git a/src/Headers/functionClause.h b/src/Headers/functionClause.h index 7d98f64..3b24bc7 100644 --- a/src/Headers/functionClause.h +++ b/src/Headers/functionClause.h @@ -10,7 +10,7 @@ # ifndef FUNCTIONCLAUSE_H # define FUNCTIONCLAUSE_H -/*@private@*/ typedef enum { +/*:private:*/ typedef enum { FCK_GLOBALS, FCK_MODIFIES, FCK_WARN, diff --git a/src/Headers/functionClauseList.h b/src/Headers/functionClauseList.h index a0b0ca2..24ff040 100644 --- a/src/Headers/functionClauseList.h +++ b/src/Headers/functionClauseList.h @@ -7,7 +7,7 @@ # ifndef FUNCTIONCLAUSELIST_H # define FUNCTIONCLAUSELIST_H -/*@private@*/ typedef /*@only@*/ functionClause o_functionClause; +/*:private:*/ typedef /*@only@*/ functionClause o_functionClause; struct s_functionClauseList { diff --git a/src/Headers/genericTable.h b/src/Headers/genericTable.h index bf9a391..52b0722 100644 --- a/src/Headers/genericTable.h +++ b/src/Headers/genericTable.h @@ -17,7 +17,7 @@ abst_typedef null struct _genericTable *genericTable; */ -/*@private@*/ typedef struct +/*:private:*/ typedef struct { /*@only@*/ cstring key; /*@only@*/ void *val; diff --git a/src/Headers/llerror.h b/src/Headers/llerror.h index 99b39e5..5fb4d4d 100644 --- a/src/Headers/llerror.h +++ b/src/Headers/llerror.h @@ -78,7 +78,7 @@ extern void llhint (/*@only@*/ cstring p_s) /*@globals g_currentloc, g_warningstream;@*/ /*@modifies g_warningstream@*/ ; -extern /*@private@*/ /*@noreturn@*/ void +extern /*:private:*/ /*@noreturn@*/ void xllfatalbug (char *p_srcFile, int p_srcLine, /*@only@*/ cstring p_s) /*@globals g_currentloc@*/ /*@modifies g_errorstream@*/ ; @@ -90,7 +90,7 @@ extern /*@noreturn@*/ void llfatalbug (/*@only@*/ cstring p_s) # define llfatalbug(p_s) \ xllfatalbug (__FILE__, __LINE__, p_s) -extern /*@private@*/ bool xllgenerror (char *p_srcFile, int p_srcLine, flagcode p_o, +extern /*:private:*/ bool xllgenerror (char *p_srcFile, int p_srcLine, flagcode p_o, /*@only@*/ cstring p_s, fileloc p_fl) /*@modifies g_warningstream@*/ ; @@ -99,7 +99,7 @@ extern bool llgenerror (flagcode p_o, /*@only@*/ cstring p_s, fileloc p_fl) # define llgenerror(p_o, p_s, p_fl) \ xllgenerror (__FILE__, __LINE__, p_o, p_s, p_fl) -extern /*@private@*/ bool +extern /*:private:*/ bool xllgenhinterror (char *p_srcFile, int p_srcLine, flagcode p_o, /*@only@*/ cstring p_s, /*@only@*/ cstring p_hint, fileloc p_fl) @@ -121,7 +121,7 @@ extern void llerror (flagcode p_o, /*@only@*/ cstring p_s) extern void llgenmsg (/*@only@*/ cstring p_s, fileloc p_fl) /*@modifies g_warningstream@*/ ; -extern /*@noreturn@*/ /*@private@*/ +extern /*@noreturn@*/ /*:private:*/ void xllfatalerror (char *p_srcFile, int p_srcLine, /*@only@*/ cstring p_s) /*@modifies g_errorstream@*/ ; @@ -129,7 +129,7 @@ extern /*@noreturn@*/ void llfatalerror (/*@only@*/ cstring p_s) /*@modifies g_errorstream@*/ ; # define llfatalerror(p_s) xllfatalerror (__FILE__, __LINE__, p_s) -extern /*@noreturn@*/ /*@private@*/ void +extern /*@noreturn@*/ /*:private:*/ void xllfatalerrorLoc (char *p_srcFile, int p_srcLine, /*@only@*/ cstring p_s) /*@globals g_currentloc@*/ /*@modifies g_errorstream@*/ ; @@ -139,7 +139,7 @@ extern /*@noreturn@*/ void llfatalerrorLoc (/*@only@*/ cstring p_s) /*@modifies g_errorstream@*/ ; # define llfatalerrorLoc(p_s) xllfatalerrorLoc (__FILE__, __LINE__, p_s) -extern /*@private@*/ void +extern /*:private:*/ void xllparseerror (char *p_srcFile, int p_srcLine, /*@only@*/ cstring p_s) /*@globals g_currentloc@*/ /*@modifies g_warningstream@*/ ; @@ -234,7 +234,7 @@ optgenerror2n (flagcode p_f1, flagcode p_f2, /*@only@*/ cstring p_s, fileloc p_l # define optgenerror2n(p_f1, p_f2, p_s, p_loc) \ (xoptgenerror2n (__FILE__, __LINE__, p_f1, p_f2, p_s, p_loc)) -extern /*@private@*/ bool xlloptgenerror (char *p_srcFile, int p_srcLine, flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc) +extern /*:private:*/ bool xlloptgenerror (char *p_srcFile, int p_srcLine, flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc) /*@modifies *g_warningstream, internalState@*/ ; extern bool lloptgenerror (flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc) @@ -251,7 +251,7 @@ extern bool llnoptgenerror (flagcode p_o, /*@only@*/ cstring p_s, fileloc p_loc) # define llnoptgenerror(p_o, p_s, p_loc) \ (xllnoptgenerror (__FILE__, __LINE__, p_o, p_s, p_loc)) -extern /*@private@*/ bool +extern /*:private:*/ bool xllgenformattypeerror (char *p_srcFile, int p_srcLine, ctype p_t1, exprNode p_e1, ctype p_t2, exprNode p_e2, @@ -317,7 +317,7 @@ extern void /*@modifies *g_warningstream, internalState@*/ ; #define voptgenerror(o, s, loc) ((void) optgenerror(o,s,loc)) -extern /*@private@*/ bool +extern /*:private:*/ bool xfsgenerror (char *p_srcFile, int p_srcLine, flagSpec p_fs, /*@only@*/ cstring p_s, fileloc p_fl) /*@modifies g_warningstream, internalState@*/ ; @@ -373,7 +373,7 @@ extern void ((void) llgenhinterror(o, s, h, loc)) -extern /*@private@*/ bool /*@alt void@*/ xllforceerror (char *p_srcFile, int p_srcLine, flagcode p_code, /*@only@*/ cstring p_s, fileloc p_fl) +extern /*:private:*/ bool /*@alt void@*/ xllforceerror (char *p_srcFile, int p_srcLine, flagcode p_code, /*@only@*/ cstring p_s, fileloc p_fl) /*@modifies g_warningstream@*/ ; extern bool /*@alt void@*/ llforceerror (flagcode p_code, /*@only@*/ cstring p_s, fileloc p_fl) @@ -381,7 +381,7 @@ extern bool /*@alt void@*/ llforceerror (flagcode p_code, /*@only@*/ cstring p_s # define llforceerror(p_code, p_s, p_fl) \ (xllforceerror (__FILE__, __LINE__, p_code, p_s, p_fl)) -extern /*@private@*/ bool xcppoptgenerror (char *p_srcFile, int p_srcLine, flagcode p_o, +extern /*:private:*/ bool xcppoptgenerror (char *p_srcFile, int p_srcLine, flagcode p_o, /*@only@*/ cstring p_s, cppReader *p_pfile) /*@modifies g_warningstream, p_pfile@*/ ; diff --git a/src/Headers/mtDeclarationPiece.h b/src/Headers/mtDeclarationPiece.h index b326898..e974390 100644 --- a/src/Headers/mtDeclarationPiece.h +++ b/src/Headers/mtDeclarationPiece.h @@ -10,7 +10,7 @@ # ifndef MTDECLARATIONPIECE_H # define MTDECLARATIONPIECE_H -/*@private@*/ typedef enum { +/*:private:*/ typedef enum { MTP_DEAD, MTP_CONTEXT, MTP_VALUES, MTP_DEFAULTS, MTP_DEFAULTVALUE, MTP_ANNOTATIONS, MTP_MERGE, diff --git a/src/Headers/mtDefaultsDeclList.h b/src/Headers/mtDefaultsDeclList.h index a4d7a75..2cdfce7 100644 --- a/src/Headers/mtDefaultsDeclList.h +++ b/src/Headers/mtDefaultsDeclList.h @@ -7,7 +7,7 @@ # ifndef mtDefaultsDeclLIST_H # define mtDefaultsDeclLIST_H -/*@private@*/ typedef /*@only@*/ mtDefaultsDecl o_mtDefaultsDecl; +/*:private:*/ typedef /*@only@*/ mtDefaultsDecl o_mtDefaultsDecl; struct s_mtDefaultsDeclList { diff --git a/src/Headers/mtLoseReferenceList.h b/src/Headers/mtLoseReferenceList.h index d051bf6..ecfe3f3 100644 --- a/src/Headers/mtLoseReferenceList.h +++ b/src/Headers/mtLoseReferenceList.h @@ -7,7 +7,7 @@ # ifndef MTLoseReferenceLIST_H # define MTLoseReferenceLIST_H -/*@private@*/ typedef /*@only@*/ mtLoseReference o_mtLoseReference; +/*:private:*/ typedef /*@only@*/ mtLoseReference o_mtLoseReference; struct s_mtLoseReferenceList { diff --git a/src/Headers/mtMergeClauseList.h b/src/Headers/mtMergeClauseList.h index 65587b1..8af617d 100644 --- a/src/Headers/mtMergeClauseList.h +++ b/src/Headers/mtMergeClauseList.h @@ -7,7 +7,7 @@ # ifndef MTMERGECLAUSELIST_H # define MTMERGECLAUSELIST_H -/*@private@*/ typedef /*@only@*/ mtMergeClause o_mtMergeClause; +/*:private:*/ typedef /*@only@*/ mtMergeClause o_mtMergeClause; struct s_mtMergeClauseList { diff --git a/src/Headers/mtTransferClauseList.h b/src/Headers/mtTransferClauseList.h index 16ef039..60753a9 100644 --- a/src/Headers/mtTransferClauseList.h +++ b/src/Headers/mtTransferClauseList.h @@ -7,7 +7,7 @@ # ifndef MTTRANSFERCLAUSELIST_H # define MTTRANSFERCLAUSELIST_H -/*@private@*/ typedef /*@only@*/ mtTransferClause o_mtTransferClause; +/*:private:*/ typedef /*@only@*/ mtTransferClause o_mtTransferClause; struct s_mtTransferClauseList { diff --git a/src/Headers/osd.h b/src/Headers/osd.h index 0e02f74..ca5c2b9 100644 --- a/src/Headers/osd.h +++ b/src/Headers/osd.h @@ -135,8 +135,8 @@ extern int /*pid_t*/ osd_getPid (void) ; ** full path name. */ -# define CONNECTSTR ":" -# define CONNECTCHAR ':' +# define CONNECTSTR ":" +# define CONNECTCHAR ':' /* Directory separator character for search list. */ /*@constant static char PATH_SEPARATOR; @*/ diff --git a/src/Makefile.am b/src/Makefile.am index bc16e65..635811c 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -397,7 +397,7 @@ etags: lintnew: splintme splintme: - ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw + ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw -mts tainted splintmesupcounts: ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -supcounts -constuse -mts file -mts filerw diff --git a/src/Makefile.in b/src/Makefile.in index af506c8..534fbe5 100644 --- a/src/Makefile.in +++ b/src/Makefile.in @@ -1125,7 +1125,7 @@ etags: lintnew: splintme splintme: - ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw + ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -fcnuse -incondefs -exportlocal -constuse -mts file -mts filerw -mts tainted splintmesupcounts: ./splint $(DEFAULT_INCLUDES) $(DEFS) $(INCLUDES) $(AM_CPPFLAGS) $(CPPFLAGS) +singleinclude $(OVERFLOWCHSRC) $(LINTSRC) $(LCLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -incondefs -exportlocal -supcounts -constuse -mts file -mts filerw diff --git a/src/clabstract.c b/src/clabstract.c index d1affb4..6538a6d 100644 --- a/src/clabstract.c +++ b/src/clabstract.c @@ -505,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 setImplictfcnConstraints (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 (("setImplictfcnConstraints 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 @@ -548,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; } @@ -584,7 +578,7 @@ void setCurrentParams (/*@dependent@*/ uentryList ue) void clearCurrentParams (void) { - currentParamList = uentryList_undefined; + currentParamList = uentryList_undefined; } /* @@ -2221,15 +2215,19 @@ 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.")); } - /*@ savedCopy to used to mitigate danger of accessing freed memory*/ + /* saveCopy to used to mitigate danger of accessing freed memory*/ return sRef_saveCopy (sr); } diff --git a/src/constraint.c b/src/constraint.c index 3706574..e5f7896 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -256,31 +256,22 @@ constraint constraint_setFcnPre (/*@returned@*/ constraint c) fileloc constraint_getFileloc (constraint c) { - llassert (constraint_isDefined (c) ); if (exprNode_isDefined (c->generatingExpr)) - return (fileloc_copy (exprNode_getfileloc (c->generatingExpr))); + return (fileloc_copy (exprNode_loc (c->generatingExpr))); return (constraintExpr_getFileloc (c->lexpr)); - - } static bool checkForMaxSet (constraint c) -{ - - llassert (constraint_isDefined (c) ); - - if (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr)) - return TRUE; - - return FALSE; +{ + llassert (constraint_isDefined (c)); + return (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr)); } bool constraint_hasMaxSet (constraint c) { - llassert (constraint_isDefined (c) ); if (checkForMaxSet (c)) @@ -302,47 +293,44 @@ constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind) po = po; ind = ind; ret->lexpr = constraintExpr_makeMaxReadExpr (po); - ret->ar = GTE; - ret->expr = constraintExpr_makeValueExpr (ind); + ret->ar = GTE; + ret->expr = constraintExpr_makeValueExpr (ind); ret->post = FALSE; return ret; } -constraint constraint_makeWriteSafeInt ( exprNode po, int ind) +constraint constraint_makeWriteSafeInt (exprNode po, int ind) { constraint ret = constraint_makeNew (); - ret->lexpr =constraintExpr_makeMaxSetExpr (po); ret->ar = GTE; ret->expr = constraintExpr_makeIntLiteral (ind); - /*@i1*/return ret; + /*@i1*/ return ret; } constraint constraint_makeSRefSetBufferSize (sRef s, long int size) { - constraint ret = constraint_makeNew (); - ret->lexpr = constraintExpr_makeSRefMaxset (s); - ret->ar = EQ; - ret->expr = constraintExpr_makeIntLiteral ((int)size); - ret->post = TRUE; - return ret; + constraint ret = constraint_makeNew (); + ret->lexpr = constraintExpr_makeSRefMaxset (s); + ret->ar = EQ; + ret->expr = constraintExpr_makeIntLiteral ((int)size); + ret->post = TRUE; + return ret; } constraint constraint_makeSRefWriteSafeInt (sRef s, int ind) { constraint ret = constraint_makeNew (); - - ret->lexpr = constraintExpr_makeSRefMaxset ( s); ret->ar = GTE; - ret->expr = constraintExpr_makeIntLiteral (ind); + ret->expr = constraintExpr_makeIntLiteral (ind); ret->post = TRUE; return ret; } /* drl added 01/12/2000 - - makes the constraint: Ensures index <= MaxRead (buffer) */ +** makes the constraint: Ensures index <= MaxRead (buffer) +*/ constraint constraint_makeEnsureLteMaxRead (exprNode index, exprNode buffer) { @@ -358,7 +346,6 @@ constraint constraint_makeEnsureLteMaxRead (exprNode index, exprNode buffer) constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) { constraint ret = constraint_makeNew (); - ret->lexpr =constraintExpr_makeMaxSetExpr (po); ret->ar = GTE; @@ -367,13 +354,13 @@ constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind) } -constraint constraint_makeReadSafeInt ( exprNode t1, int index) +constraint constraint_makeReadSafeInt (exprNode t1, int index) { constraint ret = constraint_makeNew (); ret->lexpr = constraintExpr_makeMaxReadExpr (t1); - ret->ar = GTE; - ret->expr = constraintExpr_makeIntLiteral (index); + ret->ar = GTE; + ret->expr = constraintExpr_makeIntLiteral (index); ret->post = FALSE; return ret; } @@ -381,8 +368,7 @@ constraint constraint_makeReadSafeInt ( exprNode t1, int index) constraint constraint_makeSRefReadSafeInt (sRef s, int ind) { constraint ret = constraint_makeNew (); - - + ret->lexpr = constraintExpr_makeSRefMaxRead (s); ret->ar = GTE; ret->expr = constraintExpr_makeIntLiteral (ind); @@ -392,10 +378,8 @@ constraint constraint_makeSRefReadSafeInt (sRef s, int ind) constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint) { - constraint ret; - - ret = constraint_makeReadSafeExprNode (t1, t2); - llassert (constraint_isDefined (ret) ); + constraint ret = constraint_makeReadSafeExprNode (t1, t2); + llassert (constraint_isDefined (ret)); ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); ret->post = TRUE; @@ -403,56 +387,46 @@ constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, filelo return ret; } -static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint, arithType ar) +static constraint +constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, + fileloc sequencePoint, arithType ar) { - - constraint ret; - + constraint ret = constraint_makeNew (); llassert (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2)); - - ret = constraint_makeNew (); - ret->lexpr = c1; ret->ar = ar; ret->post = TRUE; - ret->expr = c2; + ret->expr = c2; ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint); return ret; } -static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint, arithType ar) +static constraint +constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, + fileloc sequencePoint, arithType ar) { constraintExpr c1, c2; - constraint ret; - exprNode e; - - if (! (exprNode_isDefined (e1) && exprNode_isDefined (e2))) + + if (!(exprNode_isDefined (e1) && exprNode_isDefined (e2))) { - llcontbug ((message ("null exprNode, Exprnodes are %s and %s", - exprNode_unparse (e1), exprNode_unparse (e2)) - )); + llcontbug (message ("Invalid exprNode, Exprnodes are %s and %s", + exprNode_unparse (e1), exprNode_unparse (e2))); } - - e = e1; - c1 = constraintExpr_makeValueExpr (e); - e = e2; - c2 = constraintExpr_makeValueExpr (e); + c1 = constraintExpr_makeValueExpr (e1); + c2 = constraintExpr_makeValueExpr (e2); - ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar); - - return ret; + return constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar); } - /* make constraint ensures e1 == e2 */ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint) { - return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ)); + return (constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ)); } -/*make constraint ensures e1 < e2 */ +/* make constraint ensures e1 < e2 */ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint) { constraintExpr t1, t2; @@ -461,19 +435,17 @@ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequ t1 = constraintExpr_makeValueExpr (e1); t2 = constraintExpr_makeValueExpr (e2); - /*change this to e1 <= (e2 -1) */ + /* change this to e1 <= (e2 -1) */ t2 = constraintExpr_makeDecConstraintExpr (t2); - - t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE); - - t3 = constraint_simplify(t3); + t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE); + t3 = constraint_simplify (t3); return (t3); } constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint) { - return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE)); + return (constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE)); } constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint) @@ -484,12 +456,10 @@ constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc s t1 = constraintExpr_makeValueExpr (e1); t2 = constraintExpr_makeValueExpr (e2); - /* change this to e1 >= (e2 + 1) */ t2 = constraintExpr_makeIncConstraintExpr (t2); t3 = constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE); - t3 = constraint_simplify(t3); return t3; @@ -817,7 +787,7 @@ static /*@only@*/ cstring constraint_unparseDetailedPostCondition (/*@observer@ cstring temp; temp = message ("\nOriginal Generating expression %q: %s\n", - fileloc_unparse ( exprNode_getfileloc (c->generatingExpr)), + fileloc_unparse (exprNode_loc (c->generatingExpr)), genExpr); st = cstring_concatFree (st, temp); diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index 5e6c84f..7595c14 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -679,26 +679,21 @@ exprNode_doGenerateConstraintSwitch *savedRequires = constraintList_mergeRequiresFreeFirst (*savedRequires, *currentRequires); } - con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle - (stmt->edata), exprNode_getfileloc(stmt)); + con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle (stmt->edata), exprNode_loc (stmt)); - - constraintList_free(*currentEnsures); + constraintList_free (*currentEnsures); *currentEnsures = constraintList_makeNew(); *currentEnsures = constraintList_add(*currentEnsures, con); constraintList_free(*currentRequires); *currentRequires = constraintList_makeNew(); - DPRINTF((message("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:" - "%s savedEnsures:%s", - exprNode_unparse(switchExpr), exprNode_unparse(body), - constraintList_unparse(*savedRequires), constraintList_unparse(*savedEnsures) - ))); - + DPRINTF (("exprNode_doGenerateConstraintSwitch: (switch %s) %s savedRequires:" + "%s savedEnsures:%s", + exprNode_unparse(switchExpr), exprNode_unparse(body), + constraintList_unparse(*savedRequires), constraintList_unparse(*savedEnsures) + )); } - - else if (exprNode_isCaseMarker(stmt)) - /* prior case has no break. */ + else if (exprNode_isCaseMarker(stmt)) /* prior case has no break. */ { /* We don't do anything to the sved constraints because the case hasn't ended @@ -708,38 +703,28 @@ exprNode_doGenerateConstraintSwitch constraintList temp; constraint con; - constraintList ensuresTemp; - DPRINTF ((message("Got case marker with no prior break"))); - - con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle - (stmt->edata), exprNode_getfileloc(stmt)); - - ensuresTemp = constraintList_makeNew(); - + con = constraint_makeEnsureEqual (switchExpr, exprData_getSingle (stmt->edata), exprNode_loc (stmt)); + + ensuresTemp = constraintList_makeNew (); ensuresTemp = constraintList_add (ensuresTemp, con); - if (exprNode_isError(stmtList)) + if (exprNode_isError (stmtList)) { - constraintList_free(*currentEnsures); - - *currentEnsures = constraintList_copy(ensuresTemp); - constraintList_free(ensuresTemp); - + constraintList_free (*currentEnsures); + *currentEnsures = constraintList_copy (ensuresTemp); + constraintList_free (ensuresTemp); } else { - temp = constraintList_logicalOr (*currentEnsures, ensuresTemp); - - constraintList_free(*currentEnsures); - constraintList_free(ensuresTemp); - + constraintList_free (*currentEnsures); + constraintList_free (ensuresTemp); *currentEnsures = temp; } - constraintList_free(*currentRequires); - + + constraintList_free (*currentRequires); *currentRequires = constraintList_makeNew(); } else @@ -751,11 +736,12 @@ exprNode_doGenerateConstraintSwitch BADEXIT; } - DPRINTF((message("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:" - "%s currentEnsures:%s", - exprNode_unparse(switchExpr), exprNode_unparse(body), - constraintList_unparse(*currentRequires), constraintList_unparse(*currentEnsures) - ))); + DPRINTF (("returning from exprNode_doGenerateConstraintSwitch: (switch %s) %s currentRequires:" + "%s currentEnsures:%s", + exprNode_unparse(switchExpr), exprNode_unparse(body), + constraintList_unparse(*currentRequires), constraintList_unparse(*currentEnsures) + )); + /*@-onlytrans@*/ return; /*@=onlytrans@*/ diff --git a/src/constraintList.c b/src/constraintList.c index ba719e9..985e2c1 100644 --- a/src/constraintList.c +++ b/src/constraintList.c @@ -143,32 +143,30 @@ static void constraintList_freeShallow (/*@only@*/ constraintList c) constraintList constraintList_addListFree (/*@returned@*/ constraintList s, /*@only@*/ constraintList newList) { - llassert(constraintList_isDefined(s) ); - llassert(constraintList_isDefined(newList) ); - - if (constraintList_isUndefined(newList) ) + if (constraintList_isUndefined (newList)) return s; + + llassert (constraintList_isDefined (s)); + llassert (constraintList_isDefined (newList)); constraintList_elements_private_only(newList, elem) { - s = constraintList_add (s, elem); - } - end_constraintList_elements_private_only - - constraintList_freeShallow(newList); - return s; + s = constraintList_add (s, elem); + } end_constraintList_elements_private_only; + + constraintList_freeShallow (newList); + return s; } - constraintList constraintList_removeSurpressed (/*@only@*/ constraintList s) { constraintList ret; fileloc loc; - llassert(constraintList_isDefined(s) ); + llassert (constraintList_isDefined (s)); ret = constraintList_makeNew(); - constraintList_elements_private_only(s, elem) + constraintList_elements_private_only (s, elem) { loc = constraint_getFileloc(elem); @@ -176,14 +174,12 @@ constraintList constraintList_removeSurpressed (/*@only@*/ constraintList s) { ret = constraintList_add (ret, elem); } - else if (context_suppressFlagMsg(FLG_BOUNDSWRITE, loc) ) { DPRINTF ((message ("constraintList_removeSurpressed getting rid of surpressed constraint %q", constraint_unparse(elem)))); constraint_free(elem); } - else if (!constraint_hasMaxSet(elem) && context_suppressFlagMsg(FLG_BOUNDSREAD, loc)) { DPRINTF ((message("constraintList_removeSurpressed getting rid of surpressed constraint %q", @@ -195,11 +191,9 @@ constraintList constraintList_removeSurpressed (/*@only@*/ constraintList s) ret = constraintList_add (ret, elem); } fileloc_free(loc); - } - end_constraintList_elements_private_only; + } end_constraintList_elements_private_only; constraintList_freeShallow(s); - return ret; } @@ -646,6 +640,7 @@ constraintList constraintList_sort (/*@returned@*/ constraintList ret) llassert(FALSE); return ret; } + qsort (ret->elements, (size_t) ret->nelements, (sizeof (*ret->elements)), (int (*)(const void *, const void *)) constraint_compare); diff --git a/src/constraintTerm.c b/src/constraintTerm.c index f083460..57172a5 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -206,17 +206,17 @@ constraintTermType constraintTerm_getKind (constraintTerm t) return (t->value.sref); } -/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/ exprNode e) +/*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/ exprNode e) { - constraintTerm ret = new_constraintTermExpr(); - ret->loc = fileloc_copy(exprNode_getfileloc(e)); + constraintTerm ret = new_constraintTermExpr (); + ret->loc = fileloc_copy (exprNode_loc (e)); ret->value.expr = e; ret->kind = CTT_EXPR; - ret = constraintTerm_simplify(ret); + ret = constraintTerm_simplify (ret); return ret; } -/*@only@*/ constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef s) +/*@only@*/ constraintTerm constraintTerm_makesRef (/*@temp@*/ /*@observer@*/ sRef s) { constraintTerm ret = new_constraintTermExpr(); ret->loc = fileloc_undefined; diff --git a/src/context.c b/src/context.c index cc317ba..b7fcc97 100644 --- a/src/context.c +++ b/src/context.c @@ -339,7 +339,7 @@ context_suppressFlagMsg (flagcode flag, fileloc fl) return (!context_getFlag (flag) || context_inSuppressRegion () || context_inSuppressZone (fl) - || (/*@!@@#@ gc.inDerivedFile && */ context_inSuppressFlagZone (fl, flag))); + || (context_inSuppressFlagZone (fl, flag))); /* removed gc.inDerivedFile from this */ } else { @@ -4374,8 +4374,6 @@ context_destroyMod (void) globSet_free (gc.globs_used); metaStateTable_free (gc.stateTable); annotationTable_free (gc.annotTable); - - } /* diff --git a/src/cscannerHelp.c b/src/cscannerHelp.c index e5c6e51..91a03c4 100644 --- a/src/cscannerHelp.c +++ b/src/cscannerHelp.c @@ -747,9 +747,7 @@ bool cscannerHelp_handleSpecial (char *yyt) } llassert (*tmp == '\"'); - tmp++; - fname = tmp; while (*tmp != '\"' && *tmp != '\0') @@ -758,7 +756,6 @@ bool cscannerHelp_handleSpecial (char *yyt) } llassert (*tmp == '\"'); - *tmp = '\0'; # if defined(OS2) || defined(MSDOS) || defined(WIN32) diff --git a/src/ctbase.i b/src/ctbase.i index 49f3e25..a8ee579 100644 --- a/src/ctbase.i +++ b/src/ctbase.i @@ -40,7 +40,7 @@ abst_typedef /*@null@*/ struct s_ctbase *ctbase; ((cid) == CT_ABST || (cid) == CT_USER || (cid) == CT_NUMABST) /*@=macrofcndecl@*/ /*@=macroparams@*/ -/*@private@*/ typedef struct { +/*:private:*/ typedef struct { ctkind kind; ctbase ctbase; ctype base; /* type I point to (or element of array) */ diff --git a/src/exprNode.c b/src/exprNode.c index 578469a..a4846a0 100644 --- a/src/exprNode.c +++ b/src/exprNode.c @@ -2925,7 +2925,7 @@ checkGlobMods (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry_unparse (le))); params = ctype_argsFunction (ct); - return; /*@32 ! remove this? */ + return; /* No checking for non-function */ } /* @@ -11438,31 +11438,22 @@ static void checkUniqueParams (exprNode fcn, } end_exprNodeList_elements; } -long exprNode_getLongValue (exprNode e) { +long exprNode_getLongValue (exprNode e) +{ long value; - - if (exprNode_hasValue (e) - && multiVal_isInt (exprNode_getValue (e))) + + if (exprNode_hasValue (e) && multiVal_isInt (exprNode_getValue (e))) { value = multiVal_forceInt (exprNode_getValue (e)); } else { - /*@!! BADBRANCH;*/ - value = 0; + value = 0; /* Unknown value */ } return value; } -/*@observer@*/ fileloc exprNode_getfileloc (exprNode p_e) -{ - if (exprNode_isDefined (p_e) ) - return ( p_e->loc ); - else - return fileloc_undefined; -} - /*@only@*/ fileloc exprNode_getNextSequencePoint (exprNode e) { /* diff --git a/src/lh.c b/src/lh.c index 30fed49..5019920 100644 --- a/src/lh.c +++ b/src/lh.c @@ -52,9 +52,9 @@ # define TABINCH '\t' -/*@private@*/ typedef struct +/*:private:*/ typedef struct { - /*:open:*/ /*@dependent@*/ /*@null@*/ /*@reldef@*/ FILE *f; + /*@open@*/ /*@dependent@*/ /*@null@*/ /*@reldef@*/ FILE *f; /*@reldef@*/ cstring name; } outFile; diff --git a/src/llerror.c b/src/llerror.c index 4f108c4..4e2fc30 100644 --- a/src/llerror.c +++ b/src/llerror.c @@ -42,10 +42,11 @@ static void printIndentMessage (FILE *p_stream, /*@only@*/ cstring p_sc, int p_indent) /*@modifies *p_stream@*/ ; -static int lclerrors = 0; -static size_t lastfileloclen = 10; -static /*@only@*/ cstring lastmsg = cstring_undefined; -static int mcount = 0; +static bool s_scanOpen = FALSE; +static int s_lclerrors = 0; +static size_t s_lastfileloclen = 10; +static /*@only@*/ cstring s_lastmsg = cstring_undefined; +static int s_mcount = 0; static /*@only@*/ cstring saveOneMessage = cstring_undefined; static /*@only@*/ fileloc lastparseerror = fileloc_undefined; static /*@only@*/ fileloc lastbug = fileloc_undefined; @@ -65,7 +66,7 @@ static void generateCSV (flagcode p_code, cstring p_s, cstring p_addtext, filelo /*@modifies g_csvstream@*/ ; static void printError (FILE *p_stream, /*@only@*/ cstring p_sc) - /*@globals lastfileloclen @*/ + /*@globals s_lastfileloclen @*/ /*@modifies *p_stream@*/ ; static void printMessage (FILE *p_stream, /*@only@*/ cstring p_s) /*@modifies *p_stream@*/ ; @@ -240,7 +241,7 @@ llsuppresshint2 (char c, flagcode f1, flagcode f2) { cstring desc = flagcodeHint (f1); context_setNeednl (); - lastfileloclen = 8; + s_lastfileloclen = 8; if (cstring_isUndefined (desc)) { @@ -301,7 +302,7 @@ llsuppresshint (char c, flagcode f) { cstring desc = flagcodeHint (f); context_setNeednl (); - lastfileloclen = 8; + s_lastfileloclen = 8; if (flagcode_isNamePrefixFlag (f)) { @@ -329,7 +330,7 @@ llnosuppresshint (flagcode f) { cstring desc = flagcodeHint (f); context_setNeednl (); - lastfileloclen = 8; + s_lastfileloclen = 8; if (cstring_isDefined (desc)) { @@ -346,6 +347,17 @@ llnosuppresshint (flagcode f) typedef /*@null@*/ /*@dependent@*/ char *nd_charp; +/* +** mstring_split +** +** Divides a string into lines of up to maxline characters. +** +** Initial string: *sp +** +** Output split: *sp / *tp +** possibly null +*/ + static void mstring_split (/*@returned@*/ char **sp, /*@out@*/ nd_charp *tp, @@ -371,8 +383,6 @@ mstring_split (/*@returned@*/ char **sp, osp = s; } - nl = strchr (s, '\n'); - /* ** splitting: ** @@ -389,6 +399,8 @@ mstring_split (/*@returned@*/ char **sp, ** */ + nl = strchr (s, '\n'); + if ((nl != NULL) && ((nl - s) < maxline)) { *nl = '\0'; @@ -411,7 +423,7 @@ mstring_split (/*@returned@*/ char **sp, } else if (size_toInt (strlen (s)) < maxline) { - llassertprotect (*tp == NULL || (*tp > osp)); + llassertprotect (*tp == NULL); return; } else @@ -467,7 +479,11 @@ mstring_split (/*@returned@*/ char **sp, } } - while (*t != ' ' && *t != '\t' && i < MAXSEARCH) + /* + ** Search for any breaking point (at least 4 letters past s) + */ + + while (*t != ' ' && *t != '\t' && i < MAXSEARCH && t > (s + 4)) { t--; i++; @@ -505,16 +521,7 @@ mstring_split (/*@returned@*/ char **sp, *tp = t; -# if 0 - /* Hack to prevent error case for wierd strings. */ - if (t <= osp) - { - *tp = NULL; - return; - } - llassertprotect (*tp == NULL || (*tp > osp)); -# endif - + llassert (*sp != *tp); return; } } @@ -525,7 +532,7 @@ mstring_split (/*@returned@*/ char **sp, static void limitmessage (/*@only@*/ cstring s, fileloc loc) { - if (mcount > context_getLimit () + 1) + if (s_mcount > context_getLimit () + 1) { cstring_free (s); } @@ -533,7 +540,7 @@ void limitmessage (/*@only@*/ cstring s, fileloc loc) { cstring flstring = fileloc_unparse (loc); - lastfileloclen = cstring_length (flstring); + s_lastfileloclen = cstring_length (flstring); cstring_free (saveOneMessage); saveOneMessage = message ("%q: %q", flstring, s); } @@ -551,7 +558,7 @@ void cleanupMessages () } else { - int unprinted = mcount - context_getLimit (); + int unprinted = s_mcount - context_getLimit (); if (unprinted > 0) { @@ -572,19 +579,19 @@ void cleanupMessages () fprintf (g_warningstream, "%s: (%d more similar errors unprinted)\n", cstring_toCharsSafe (fileloc_filename (g_currentloc)), - mcount - context_getLimit ()); + s_mcount - context_getLimit ()); } } } - mcount = 0; + s_mcount = 0; } void llgenmsg (/*@only@*/ cstring s, fileloc fl) { cstring flstring = fileloc_unparse (fl); - lastfileloclen = cstring_length (flstring); + s_lastfileloclen = cstring_length (flstring); prepareMessage (); (void) printError (g_warningstream, message ("%q: %q", flstring, s)); @@ -1121,16 +1128,16 @@ llgenerrorreal (flagcode code, char *srcFile, int srcLine, *savechar = ':'; } - if (cstring_equal (lastmsg, cstring_fromChars (tmpmsg))) + if (cstring_equal (s_lastmsg, cstring_fromChars (tmpmsg))) { - mcount++; - if (mcount == (context_getLimit () + 1)) + s_mcount++; + if (s_mcount == (context_getLimit () + 1)) { limitmessage (s, fl); return FALSE; } - if (mcount > (context_getLimit ())) + if (s_mcount > (context_getLimit ())) { cstring_free (s); return FALSE; @@ -1139,9 +1146,9 @@ llgenerrorreal (flagcode code, char *srcFile, int srcLine, else { cleanupMessages (); - mcount = 0; - cstring_free (lastmsg); - lastmsg = cstring_fromCharsNew (tmpmsg); + s_mcount = 0; + cstring_free (s_lastmsg); + s_lastmsg = cstring_fromCharsNew (tmpmsg); } } @@ -1230,7 +1237,7 @@ llgenerrorreal (flagcode code, char *srcFile, int srcLine, } flstring = fileloc_unparse (fl); - lastfileloclen = cstring_length (flstring); + s_lastfileloclen = cstring_length (flstring); generateCSV (code, s, addtext, fl); @@ -1296,7 +1303,7 @@ static void printError (FILE *stream, /*@only@*/ cstring sc) { int maxlen = context_getLineLen (); - size_t nspaces = lastfileloclen + 5; + size_t nspaces = s_lastfileloclen + 5; int nextlen = maxlen - size_toInt (nspaces); size_t len = cstring_length (sc); int indent = 0; @@ -1566,7 +1573,7 @@ xllfatalerrorLoc (char *srcFile, int srcLine, /*@only@*/ cstring s) bool lclHadError (void) { - return (lclerrors > 0); + return (s_lclerrors > 0); } bool @@ -1574,9 +1581,9 @@ lclHadNewError (void) { static int lastcall = 0; - if (lclerrors > lastcall) + if (s_lclerrors > lastcall) { - lastcall = lclerrors; + lastcall = s_lclerrors; return TRUE; } else @@ -1588,18 +1595,18 @@ lclHadNewError (void) int lclNumberErrors (void) { - return (lclerrors); + return (s_lclerrors); } void xlclerror (char *srcFile, int srcLine, ltoken t, /*@only@*/ cstring msg) { - lclerrors++; + s_lclerrors++; if (ltoken_getCode (t) != NOTTOKEN) { cstring loc = ltoken_unparseLoc (t); - lastfileloclen = cstring_length (loc); + s_lastfileloclen = cstring_length (loc); printError (g_warningstream, message ("%q: %q", loc, msg)); showSourceLoc (srcFile, srcLine); @@ -1614,7 +1621,7 @@ xlclerror (char *srcFile, int srcLine, ltoken t, /*@only@*/ cstring msg) void lclplainerror (/*@only@*/ cstring msg) { - lclerrors++; + s_lclerrors++; printError (g_warningstream, msg); } @@ -1624,7 +1631,7 @@ lclfatalerror (ltoken t, /*@only@*/ cstring msg) if (ltoken_getCode (t) != NOTTOKEN) { cstring loc = ltoken_unparseLoc (t); - lastfileloclen = cstring_length (loc); + s_lastfileloclen = cstring_length (loc); printError (g_errorstream, message ("%q: %q", loc, msg)); } else @@ -1675,7 +1682,7 @@ void genppllerror (flagcode code, /*@only@*/ cstring s) { if (context_getFlag (code)) { - if (!context_isInCommandLine ()) + if (s_scanOpen) { displayScanClose (); } @@ -1736,7 +1743,11 @@ void pplldiagmsg (cstring s) { if (!context_isInCommandLine ()) { - displayScanClose (); + if (s_scanOpen) + { + displayScanClose (); + } + lldiagmsg (s); displayScanOpen (cstring_makeLiteral ("< more preprocessing .")); } @@ -2046,8 +2057,6 @@ void llflush (void) (void) fflush (g_messagestream); } -static bool s_scanOpen = FALSE; - void displayScan (cstring msg) { if (s_scanOpen) diff --git a/src/osd.c b/src/osd.c index b429d3f..653a0ee 100644 --- a/src/osd.c +++ b/src/osd.c @@ -183,7 +183,7 @@ osd_getPath (cstring path, cstring file, cstring *returnPath) *fullPath == '\0' || (*file == CONNECTCHAR || (file[0] != '\0' && file[1] == ':')) # else - (*file == CONNECTCHAR) + (*file == CONNECTCHAR) # endif ) { @@ -203,8 +203,8 @@ osd_getPath (cstring path, cstring file, cstring *returnPath) /* Path specified. Loop through directories in path looking for the */ /* first occurrence of the file. */ - while (nextdir (&fullPath, &dirPtr, &dirLen) && - rVal == OSD_FILENOTFOUND) + while (nextdir (&fullPath, &dirPtr, &dirLen) + && rVal == OSD_FILENOTFOUND) { if ((dirLen + strlen (file) + 2) <= MAXPATHLEN) { diff --git a/src/stateClauseList.c b/src/stateClauseList.c index d51c24c..fe5bf2e 100644 --- a/src/stateClauseList.c +++ b/src/stateClauseList.c @@ -297,7 +297,7 @@ void stateClauseList_checkAll (uentry ue) stateClause_unparse (cl)), uentry_whereLast (ue))) { - /*@i! annotationInfo_showContextError (ainfo, ue); */ + /* annotationInfo_showContextError (ainfo, ue); */ } } } diff --git a/src/transferChecks.c b/src/transferChecks.c index d77e7c3..fe12682 100644 --- a/src/transferChecks.c +++ b/src/transferChecks.c @@ -4017,7 +4017,6 @@ checkMetaStateConsistent (/*@exposed@*/ sRef fref, sRef tref, } else { - /*@i#!@!!@*/ DPRINTF (("Cannot find meta state for: %s / to: %s / %s", sRef_unparseFull (fref), sRef_unparseFull (tref), fkey)); @@ -4176,7 +4175,6 @@ checkMetaStateTransfer (exprNode fexp, sRef fref, exprNode texp, sRef tref, } else { - /*@i#!@!!@*/ DPRINTF (("Metastate transfer: %s => %s", exprNode_unparse (fexp), exprNode_unparse (texp))); DPRINTF (("Cannot find meta state for: %s / to: %s / %s", sRef_unparseFull (fref), diff --git a/src/uentry.c b/src/uentry.c index 711b32b..ce029e8 100644 --- a/src/uentry.c +++ b/src/uentry.c @@ -2499,7 +2499,7 @@ uentry_reflectOtherQualifier (/*@notnull@*/ uentry ue, qual qel) uentry_unparse (ue)), uentry_whereLast (ue))) { - /*@i! annotationInfo_showContextError (ainfo, ue); */ + /* annotationInfo_showContextError (ainfo, ue); */ } } } @@ -10380,10 +10380,7 @@ uentry_mergeValueStates (/*@notnull@*/ uentry res, /*@notnull@*/ uentry other, ** Copy values from other */ - /*@i$@#@*/ - DPRINTF (("Has value table: %s", sRef_unparseFull (other->sref))); - DPRINTF (("No value table: %s", sRef_unparseFull (res->sref))); - ; + /* ??? */ } else { diff --git a/src/usymtab.c b/src/usymtab.c index bdb71f9..2d2bb3f 100644 --- a/src/usymtab.c +++ b/src/usymtab.c @@ -2047,12 +2047,11 @@ void usymtab_load (FILE *f) { constraintList preconditions; constraintList postconditions; - - cstring name = cstring_fromChars(reader_getWord(&s) ); + cstring name = cstring_fromChars (reader_getWord (&s)); cstring temp; - ue = usymtab_lookup ( name ); - cstring_free(name); + ue = usymtab_lookup (name); + cstring_free (name); preconditions = constraintList_undefined; postconditions = constraintList_undefined; diff --git a/test/Makefile.am b/test/Makefile.am index 6331482..4fd04a8 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -83,7 +83,6 @@ version: help: -@$(SPLINT) - -@LARCH_PATH=/dev/null; $(SPLINT) -nof empty.lcl -@$(SPLINT) -help -@$(SPLINTP) -asdf -@$(SPLINTP) +boolint +boolint diff --git a/test/Makefile.in b/test/Makefile.in index 55d5b67..79e5c88 100644 --- a/test/Makefile.in +++ b/test/Makefile.in @@ -927,7 +927,6 @@ version: help: -@$(SPLINT) - -@LARCH_PATH=/dev/null; $(SPLINT) -nof empty.lcl -@$(SPLINT) -help -@$(SPLINTP) -asdf -@$(SPLINTP) +boolint +boolint diff --git a/test/help.expect b/test/help.expect index 456dda1..4fbb2dc 100644 --- a/test/help.expect +++ b/test/help.expect @@ -22,8 +22,6 @@ Topics: version (information on compilation, maintainer) -Finished checking --- no code processed - Source files are .c, .h and .lcl files. If there is no suffix, Splint will look for .c and .lcl. -- 2.45.0