Fixes after removing -unrecogcomments flag for make splintme.

diff --git a/src/Headers/constraintList.h b/src/Headers/constraintList.h
index 94b190fc551a1926ea6676feaf02db5249c86c1d..dc8861c90fe6766f75b49edb02536b15c83d71b3 100644 (file)
--- 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 336007297d237afe2f6364b3e0155e2430759f1a..e3250100734eaec307d6e6bb908ac96dfa165979 100644 (file)
--- 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 13692009958d66e06a96884a79f8e8578482f11d..0f798c69f4f5c12d9649d34747c41c98800651a2 100644 (file)
--- 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 421550c41cd87bc72cdc372ca05d12e1ff19610b..12ae15aec19d1def0428de286241ac1640bc47ab 100644 (file)
--- 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 d5ec489fb44ddad3a69716c0c942802fd7303c82..607bec1004248f52196f140b00622f59137a095e 100644 (file)
--- 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 79019b883f44d875c3febf94c43e2444162239ac..52f399020a54fed4db94461ff784c50e8c368c9b 100644 (file)
--- 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 b55a8d25eb6496c90ae941683fb3420866ea9b64..36a417bed7e83dde95a7c4a84478902c12e928b3 100644 (file)
--- 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 7d98f6455277e5bfb233c37418e0257ecbbf5314..3b24bc72a83c48f6a52d6811cc48469f68a00c34 100644 (file)
--- 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 a0b0ca25593261eb25c52c04cf13554563bc8cc3..24ff040c02d76694abc08a9ae164515cfbe71fda 100644 (file)
--- 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 bf9a391a70d095b89d972648366710c3c14aafbb..52b0722fa8819de40cd4f3088ef8e11ebe887614 100644 (file)
--- 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 99b39e5ff41fb58ced95bd2712934f1316202264..5fb4d4db0b8f6f3cf0ade02d32faf44064c5cfbd 100644 (file)
--- 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 b3268989cbbe520f450f5c65ac6193dfdbae5d8d..e9743906b8112fcebbca45ed119f4408b55c4bb7 100644 (file)
--- 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 a4d7a7563c272398862349ebdb6a0ad51e9c5f12..2cdfce7ddff7296321f9f75f743ae7f65182e3f5 100644 (file)
--- 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 d051bf65b441277921946d6f6f48fe3534b6687f..ecfe3f3d83b6453659e8dfa32da3255a8a12db17 100644 (file)
--- 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 65587b1e1ef8cffcb8cb1401b2fd95ab06cc7a7b..8af617dbb4b6b9cde339f3df8c5b29a1ae4bcaff 100644 (file)
--- 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 16ef039d2486a56891db4f545b7ea80210674ba5..60753a93ad84f2bd945dfb3fac51751cbc998ade 100644 (file)
--- 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 0e02f748183b19016263b26aa1ef38129f3f2c2a..ca5c2b9aeded4d2ba295595a84d2e68df9f8753e 100644 (file)
--- 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 bc16e650cd0b51e6da263b3cf0288908ce591c89..635811c29dd55dd92623cbdd25d3e34414f798b0 100644 (file)
--- 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 af506c82a9b2eed7731c8ee1ed3db3fabb902602..534fbe5bab5fd46bb879621c27fd3a31f2499dcb 100644 (file)
--- 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 d1affb49b70f199a7fb30be7386ca58d7ea53626..6538a6dc7ab83efa62a22d32a5299a8caf84a129 100644 (file)
--- 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 <type> <name>=<value>@*/ 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 <type> <name>=<value>@*/ "
+                                           "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 3706574599ec1cf2e2881a2934b392d19973cd73..e5f7896247c245aabfde08bb4d6333d988f408f6 100644 (file)
--- 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 5e6c84f2355316b715a9c25ea83b51304c4c11b5..7595c148bf101026231119a55e0c96ebcecfa43f 100644 (file)
--- 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 ba719e9e992cba8fc59c97fa5b050792ee720945..985e2c13ebe56870d3d6b1aed6fd7321c14744cd 100644 (file)
--- 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 f08346078a8ae5ffe91a728d17ab140e86a6d746..57172a52d34342d26faca41fed11ad7012fdc1ad 100644 (file)
--- 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 cc317ba1b6087197761cda7499dbc8a802382390..b7fcc97fbb98cf8a1a5c6c5c7a76b9e6dd74ddff 100644 (file)
--- 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 e5c6e51c0e77fe4d21716f40544c5248ff7073fd..91a03c4813527ac4f41c308bc7c1d726a2236194 100644 (file)
--- 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 49f3e257644cdb715de398c679f36ef6d0421ed6..a8ee579148be33bd7e0ba187bf308598ac191d7c 100644 (file)
--- 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 578469ad4a7a357753ba32fcb06a6608f82c3b57..a4846a0dd7aa2525df09937a2a696c0f77ba728e 100644 (file)
--- 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 30fed4956d5c1d62f939772362ac8ae4bed92f32..5019920d05f99a4838007fb0b9361e0c296e7b11 100644 (file)
--- 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 4f108c481e19ab70751f63ee7b43895eb93f4391..4e2fc300d3817b2c1a5949f02108925e88c1ebdc 100644 (file)
--- 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 b429d3f30b37c0785df7c81c5dec6a9c0730ef46..653a0ee8526867f7e74ae4181892fbdb78cc7263 100644 (file)
--- 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 d51c24c0fe539f48791aca22be8ba9345ed9d8c7..fe5bf2ef40894f073a7b65780c54b0462eba0a14 100644 (file)
--- 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 d77e7c3869874355cf37fd1eb322c24c07af113a..fe12682be7a5c64cbce70f74842edde0cffc77e1 100644 (file)
--- 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 711b32b68c4a4f7ea176dd818aea2fe6cbe85823..ce029e85868558df61d9274cafc9b4e044d6541d 100644 (file)
--- 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 bdb71f9e080f5933548ba434b3c82afc3491b17d..2d2bb3f724416ab2671f29a0caa1eacff9603362 100644 (file)
--- 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 63314821c2d787e68f4190b341bd7923e9f830a4..4fd04a8773498d7c5b7d7f0c172da70fa6ee6fe8 100644 (file)
--- 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 55d5b671b6dc5c9f5b95b146168706dc32165616..79e5c88a1a51cd4b347f50e112b1593570790484 100644 (file)
--- 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 456dda1fc8d99760d681a9b1680ee5c3a4dfdf8a..4fbb2dc709009d177c8e139fa4124c5480190e09 100644 (file)
--- 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 <file>.c and <file>.lcl.