*** empty log message ***

diff --git a/src/Headers/constraintList.h b/src/Headers/constraintList.h
index fa80b091e430435489493b9acb2c6f12b12c5615..c17bf6c21b9a22b368e9a3cd74f6810cca2615c7 100644 (file)
--- a/src/Headers/constraintList.h
+++ b/src/Headers/constraintList.h
@@ -82,11 +82,11 @@ 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@*/ ;
+
 void constraintList_dump (/*@observer@*/ constraintList p_c,  FILE * p_f);
 
 /*@only@*/ constraintList constraintList_undump (FILE * p_f);
-constraintList constraintList_sort (/*@returned@*/ constraintList p_ret);
-
 
 # else
 # error "Multiple include"

diff --git a/src/Headers/context.h b/src/Headers/context.h
index 29e4cf7ac34d5793ccce21152da1713499a167b5..1f64901092dc4d149ceda15ad6633e13b8e74c0a 100644 (file)
--- a/src/Headers/context.h
+++ b/src/Headers/context.h
@@ -325,10 +325,10 @@ extern void context_addAnnotation (/*@only@*/ annotationInfo)
 extern void context_addMetaState (/*@only@*/ cstring, /*@only@*/ metaStateInfo)
      /*@modifies internalState@*/ ;
 
-extern valueTable context_createValueTable (sRef p_s)
+extern valueTable context_createValueTable (sRef p_s, /*@only@*/ stateInfo p_sinfo)
      /*@globals internalState@*/ ;
 
-extern valueTable context_createGlobalMarkerValueTable (void)
+extern valueTable context_createGlobalMarkerValueTable (/*@only@*/ stateInfo p_sinfo)
      /*@globals internalState@*/ ;
 
 extern int context_getBugsLimit (void) /*@*/ ;

diff --git a/src/Headers/exprNode.h b/src/Headers/exprNode.h
index e9b8cda69562b45e1571477c467304e42cdab5a8..226cabb5bb024fe66a1edc1156c5161178eb1b1b 100644 (file)
--- a/src/Headers/exprNode.h
+++ b/src/Headers/exprNode.h
@@ -217,7 +217,11 @@ extern /*@exposed@*/ sRef exprNode_getSref (exprNode p_e) /*@*/ ;
 extern /*@observer@*/ uentry exprNode_getUentry (exprNode p_e) 
    /*@globals internalState@*/ ;
 extern void exprNode_produceGuards (exprNode p_pred) /*@modifies p_pred@*/ ;
+
 extern /*@observer@*/ fileloc exprNode_loc (exprNode p_e) /*@*/ ;
+extern /*@observer@*/ fileloc exprNode_getLoc (exprNode p_e) /*@*/ ;
+# define exprNode_getLoc exprNode_loc
+
 extern exprNode
   exprNode_charLiteral (char p_c, cstring p_text, /*@only@*/ fileloc p_loc) /*@*/ ;
 extern /*@observer@*/ exprNode exprNode_makeMustExit (void) /*@*/ ;

diff --git a/src/Headers/herald.h b/src/Headers/herald.h
index f929ab5997a7a00c2b986091160005195758d2ea..ab93b80b0c179c0d2df399afd54d52e7e29f3224 100644 (file)
--- a/src/Headers/herald.h
+++ b/src/Headers/herald.h
@@ -4,4 +4,4 @@
 /*@constant observer char *LCL_PARSE_VERSION;@*/
 # define LCL_PARSE_VERSION "LCLint 3.0.0.9"
 /*@constant observer char *LCL_COMPILE;@*/
-# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on Linux fowler 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by drl7x"
+# define LCL_COMPILE "Compiled using gcc -Wall -g on Linux matthews.cs.Virginia.EDU 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by evans"

diff --git a/src/Headers/herald.last b/src/Headers/herald.last
index f929ab5997a7a00c2b986091160005195758d2ea..ab93b80b0c179c0d2df399afd54d52e7e29f3224 100644 (file)
--- a/src/Headers/herald.last
+++ b/src/Headers/herald.last
@@ -4,4 +4,4 @@
 /*@constant observer char *LCL_PARSE_VERSION;@*/
 # define LCL_PARSE_VERSION "LCLint 3.0.0.9"
 /*@constant observer char *LCL_COMPILE;@*/
-# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on Linux fowler 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by drl7x"
+# define LCL_COMPILE "Compiled using gcc -Wall -g on Linux matthews.cs.Virginia.EDU 2.4.3-12 #1 Fri Jun 8 13:35:30 EDT 2001 i686 unknown by evans"

diff --git a/src/Headers/local_constants.h b/src/Headers/local_constants.h
index 73e13fc02ff2ff0ec28919e4f5adc9cc5c4dac80..c4c3a887ac645344e32355e5979556d4d408aa9a 100644 (file)
--- a/src/Headers/local_constants.h
+++ b/src/Headers/local_constants.h
@@ -2,6 +2,6 @@
 /*@constant observer char *SYSTEM_LIBDIR;@*/
 # define SYSTEM_LIBDIR "/usr/include"
 /*@constant observer char *DEFAULT_LARCHPATH;@*/
-# define DEFAULT_LARCHPATH ".:/af9/drl7x/re3/LCLintDev/lib"
+# define DEFAULT_LARCHPATH "/usr/local/lclint-2.5m/lib"
 /*@constant observer char *DEFAULT_LCLIMPORTDIR;@*/
-# define DEFAULT_LCLIMPORTDIR "/af9/drl7x/re3/LCLintDev/imports"
+# define DEFAULT_LCLIMPORTDIR "/usr/local/lclint-2.5m/imports"

diff --git a/src/Headers/local_constants.last b/src/Headers/local_constants.last
index 73e13fc02ff2ff0ec28919e4f5adc9cc5c4dac80..c4c3a887ac645344e32355e5979556d4d408aa9a 100644 (file)
--- a/src/Headers/local_constants.last
+++ b/src/Headers/local_constants.last
@@ -2,6 +2,6 @@
 /*@constant observer char *SYSTEM_LIBDIR;@*/
 # define SYSTEM_LIBDIR "/usr/include"
 /*@constant observer char *DEFAULT_LARCHPATH;@*/
-# define DEFAULT_LARCHPATH ".:/af9/drl7x/re3/LCLintDev/lib"
+# define DEFAULT_LARCHPATH "/usr/local/lclint-2.5m/lib"
 /*@constant observer char *DEFAULT_LCLIMPORTDIR;@*/
-# define DEFAULT_LCLIMPORTDIR "/af9/drl7x/re3/LCLintDev/imports"
+# define DEFAULT_LCLIMPORTDIR "/usr/local/lclint-2.5m/imports"

diff --git a/src/Headers/metaStateSpecifier.h b/src/Headers/metaStateSpecifier.h
index 8815ee29466716ee306782b878cac624a958a0f2..855179bbe05502745f810f8c2068b8523b43313b 100644 (file)
--- a/src/Headers/metaStateSpecifier.h
+++ b/src/Headers/metaStateSpecifier.h
@@ -10,6 +10,7 @@
 # define METASTATESPECIFIER_H
 
 struct s_metaStateSpecifier {
+  bool elipsis;
   sRef sr;
   /*@observer@*/ metaStateInfo msinfo;
 } ;
@@ -17,6 +18,10 @@ struct s_metaStateSpecifier {
 extern metaStateSpecifier
 metaStateSpecifier_create (/*@only@*/ sRef, /*@observer@*/ metaStateInfo) ;
 
+extern metaStateSpecifier
+metaStateSpecifier_createElipsis (/*@observer@*/ metaStateInfo) ;
+
+extern bool metaStateSpecifier_isElipsis (metaStateSpecifier) /*@*/ ;
 extern /*@exposed@*/ sRef metaStateSpecifier_getSref (metaStateSpecifier) /*@*/ ;
 extern /*@observer@*/ metaStateInfo metaStateSpecifier_getMetaStateInfo (metaStateSpecifier) /*@*/ ;
 

diff --git a/src/Headers/sRef.h b/src/Headers/sRef.h
index 87d5bfb14a4081413deee651d59617539244c54b..dc1c31644ca26bacec590016ad8c2300f506928f 100644 (file)
--- a/src/Headers/sRef.h
+++ b/src/Headers/sRef.h
@@ -329,20 +329,20 @@ extern /*@notnull@*/ /*@exposed@*/ sRef
 extern /*@notnull@*/ /*@dependent@*/ sRef
   sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef p_a, /*@exposed@*/ sRef p_b);
 extern /*@notnull@*/ /*@dependent@*/ sRef
-  sRef_makeCvar (int p_level, usymId p_index, ctype p_ct);
+  sRef_makeCvar (int p_level, usymId p_index, ctype p_ct, /*@only@*/ stateInfo p_stinfo);
 extern /*@notnull@*/ /*@dependent@*/ sRef
   sRef_makeConst (ctype p_ct);
 extern /*@exposed@*/ sRef
   sRef_makeField (sRef p_rec, /*@dependent@*/ cstring p_f);
 extern /*@notnull@*/ /*@dependent@*/ sRef 
-  sRef_makeGlobal (usymId p_l, ctype p_ct);
+  sRef_makeGlobal (usymId p_l, ctype p_ct, /*@only@*/ stateInfo);
 extern /*@exposed@*/ sRef
   sRef_makeNCField (/*@exposed@*/ sRef p_rec, /*@dependent@*/ cstring p_f) /*@*/ ;
 extern void sRef_maybeKill (sRef p_s, fileloc p_loc) /*@modifies p_s@*/ ;
 extern /*@unused@*/ /*@notnull@*/ /*@dependent@*/ sRef 
   sRef_makeObject (ctype p_o) /*@*/ ;
 extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeType (ctype p_ct) /*@*/ ;
-extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct) /*@*/ ;
+extern /*@notnull@*/ /*@dependent@*/ sRef sRef_makeParam (int p_l, ctype p_ct, /*@only@*/ stateInfo p_stinfo) /*@*/ ;
 extern /*@exposed@*/ sRef sRef_makePointer (/*@exposed@*/ sRef p_s) /*@modifies p_s@*/ ;
 extern void sRef_makeSafe (sRef p_s) /*@modifies p_s@*/ ;
 extern void sRef_makeUnsafe (sRef p_s) /*@modifies p_s@*/ ;

diff --git a/src/Headers/stateInfo.h b/src/Headers/stateInfo.h
index a446b4b6ccbdb88336e6c225533cd4a4ac7bc3c3..a5d0fcbd880807091e19ffc8c80f798a6b60f38d 100644 (file)
--- a/src/Headers/stateInfo.h
+++ b/src/Headers/stateInfo.h
@@ -33,6 +33,7 @@ extern /*@only@*/ stateInfo
 
 extern /*@only@*/ stateInfo stateInfo_copy (stateInfo p_a); 
 
+extern /*@only@*/ /*@notnull@*/ stateInfo stateInfo_currentLoc (void) ;
 extern /*@only@*/ /*@notnull@*/ stateInfo stateInfo_makeLoc (fileloc p_loc) ;
 extern /*@only@*/ stateInfo stateInfo_makeRefLoc (/*@exposed@*/ sRef p_ref, fileloc p_loc) ;
 

diff --git a/src/Headers/uentry.h b/src/Headers/uentry.h
index bf3a534626cece4419d77a9a822c46d174b78d54..db199e3609663e1126aec4a2c1751c8f177830a2 100644 (file)
--- a/src/Headers/uentry.h
+++ b/src/Headers/uentry.h
@@ -457,12 +457,12 @@ extern /*@notnull@*/ /*@only@*/ uentry
 
 # ifndef NOLCL
 extern /*@notnull@*/ /*@only@*/ 
-  uentry uentry_makeVariableParam (cstring p_n, ctype p_t);
+  uentry uentry_makeVariableParam (cstring p_n, ctype p_t, fileloc p_loc);
 # endif
 
 extern /*@notnull@*/ /*@only@*/ 
-  uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, 
-                                      /*@exposed@*/ sRef p_s);
+uentry uentry_makeVariableSrefParam (cstring p_n, ctype p_t, /*@only@*/ fileloc p_loc,
+                                    /*@exposed@*/ sRef p_s);
 extern /*@notnull@*/ /*@only@*/ 
   uentry uentry_makeIdFunction (idDecl p_id);
 extern /*@notnull@*/ /*@only@*/ 

diff --git a/src/Headers/warnClause.h b/src/Headers/warnClause.h
index 375f9ddcb602ded63511b33604381e23d7f9f032..4f41bb00aac83c9b4ba418d5b82974c605552846 100644 (file)
--- a/src/Headers/warnClause.h
+++ b/src/Headers/warnClause.h
@@ -14,7 +14,7 @@ struct s_warnClause
 {
   /*@only@*/ fileloc loc;
   /*@only@*/ flagSpec flag;
-  /*@only@*/ exprNode msg;
+  /*@only@*/ cstring msg;
 } ;
 
 /*@constant null warnClause warnClause_undefined; @*/
@@ -28,7 +28,7 @@ extern /*@truenull@*/ bool warnClause_isUndefined (/*@null@*/ warnClause p_f) /*
 
 extern warnClause warnClause_create (/*@only@*/ lltok,
                                     /*@only@*/ flagSpec p_flag,
-                                    /*@only@*/ exprNode p_msg) /*@*/ ;
+                                    /*@only@*/ cstring p_msg) /*@*/ ;
 
 extern /*@only@*/ warnClause warnClause_copy (warnClause) /*@*/ ;
 
@@ -37,7 +37,7 @@ extern /*@observer@*/ flagSpec warnClause_getFlag (warnClause p_w) /*@*/ ;
 extern /*@only@*/ cstring warnClause_dump (warnClause p_wc) /*@*/ ;
 extern /*@only@*/ warnClause warnClause_undump (char **p_s) /*@modifies p_s@*/ ;
 
-extern bool warnClause_hasMessage (warnClause p_w) /*@*/ ;
+extern /*@falsenull@*/ bool warnClause_hasMessage (warnClause p_w) /*@*/ ;
 
 extern /*@observer@*/ cstring warnClause_getMessage (warnClause p_w) /*@*/ ;
 extern /*@only@*/ cstring warnClause_unparse (warnClause p_w) /*@*/ ;

diff --git a/src/Makefile b/src/Makefile
index c39ab81e2bca3381d8e15f1b1d5947e81c28d157..cb7a79bf11aebae5bf5afb5fcc27104efa0bc986 100644 (file)
--- a/src/Makefile
+++ b/src/Makefile
@@ -411,7 +411,7 @@ lint28:
        ${HOME}/lclint-2.8a/bin/lclint -f lclint.lclintrc $(CPPFLAGS) +singleinclude $(ALLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -constuse -exportlocal -supcounts
 
 lint29: 
-       ${HOME}/lclint-2.9a/bin/lclint -f lclint.lclintrc $(CPPFLAGS) -larchpath .:${HOME}/lclint-2.9a/lib/ +singleinclude $(ALLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -constuse -exportlocal -supcounts
+       ${HOME}/lclint-2.9a/bin/lclint -f lclint.lclintrc $(CPPFLAGS) -larchpath .:${HOME}/lclint-2.9a/lib/ +singleinclue $(ALLSRC) -dump lclint +forcehints -misplacedsharequal +showsourceloc -unrecogcomments -fcnuse -constuse -exportlocal -supcounts
 
 lintm: 
        lclint-2.5m -f lclint.lclintrc $(CPPFLAGS) +singleinclude $(ALLSRC) -dump lclint

diff --git a/src/cgrammar.y b/src/cgrammar.y
index 4faaf30cb940bf5a0e00c52c3b0f384d78ad2364..9817a79649d504d94d5922f95f57145f48f3940b 100644 (file)
--- a/src/cgrammar.y
+++ b/src/cgrammar.y
@@ -451,8 +451,11 @@ metaStateConstraint
 
 metaStateSpecifier
   : BufConstraintSrefExpr { cscanner_expectingMetaStateName (); } TCOLON metaStateName
-   { cscanner_clearExpectingMetaStateName ();
-     $$ = metaStateSpecifier_create ($1, $4); }
+    { cscanner_clearExpectingMetaStateName ();
+      $$ = metaStateSpecifier_create ($1, $4); }
+  | CTOK_ELIPSIS { cscanner_expectingMetaStateName (); } TCOLON metaStateName
+    { cscanner_clearExpectingMetaStateName ();
+      $$ = metaStateSpecifier_createElipsis ($4); }
 
 metaStateExpression
 : metaStateSpecifier { $$ = metaStateExpression_create ($1); }
@@ -617,9 +620,13 @@ warnClause
 
 warnClausePlain
  : QWARN flagSpec cconstantExpr
-   { $$ = warnClause_create ($1, $2, $3); }
+   {      
+     llassert (exprNode_knownStringValue ($3));
+     $$ = warnClause_create ($1, $2, cstring_copy (multiVal_forceString (exprNode_getValue ($3)))); 
+     exprNode_free ($3);
+   }
  | QWARN flagSpec
-   { $$ = warnClause_create ($1, $2, exprNode_undefined); }
+   { $$ = warnClause_create ($1, $2, cstring_undefined); }
 
 globIdList
  : globIdListExpr                     { $$ = globSet_single ($1); }

diff --git a/src/clabstract.c b/src/clabstract.c
index dd02ed201c374a5127d63bc944b29e7f74ed6a27..f1bb637d386b525700c9fefe93b0fd92235384c5 100644 (file)
--- a/src/clabstract.c
+++ b/src/clabstract.c
@@ -888,7 +888,7 @@ checkTypeDecl (uentry e, ctype rep)
       uentry le  = usymtab_getTypeEntry (llm);
 
       uentry_setDeclared (e, g_currentloc); 
-      uentry_setSref (e, sRef_makeGlobal (llm, uentry_getType (le)));
+      uentry_setSref (e, sRef_makeGlobal (llm, uentry_getType (le), stateInfo_currentLoc ()));
 
       DPRINTF (("Here we are: %s / %s",
                n, context_getBoolName ()));
@@ -1731,7 +1731,7 @@ void setNewStyle ()              { flipNewStyle = TRUE; }
   uentryList_elements (params, current)
     {
       uentry_setParam (current);
-      uentry_setSref (current, sRef_makeParam (paramno, ctype_unknown));
+      uentry_setSref (current, sRef_makeParam (paramno, ctype_unknown, stateInfo_makeLoc (uentry_whereLast (current))));
       paramno++;
     } end_uentryList_elements;
 
@@ -1772,7 +1772,8 @@ doVaDcl ()
       
       if (i >= 0)
        {
-         e = uentry_makeVariableSrefParam (id, c, sRef_makeParam (i, c));
+         fileloc loc = context_getSaveLocation ();
+         e = uentry_makeVariableSrefParam (id, c, loc, sRef_makeParam (i, c, stateInfo_makeLoc (loc)));
        }
       else
        {

diff --git a/src/constraintTerm.c b/src/constraintTerm.c
index 709d77c3d0f2f9440583d2757e34d939909088e0..bbba3b7f9f518eb7ea127f31c53a3cb89b2ebdd8 100644 (file)
--- a/src/constraintTerm.c
+++ b/src/constraintTerm.c
@@ -594,12 +594,12 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t,  FILE *f)
   
   uentry ue;
   
-  char * str;
-  char * os;
+  char *str;
+  char *os;
 
   str = mstring_create (MAX_DUMP_LINE_LENGTH);
   os = str;
-  str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+  str = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 
   kind = (constraintTermType) reader_getInt(&str);
   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
@@ -630,7 +630,7 @@ void constraintTerm_dump ( /*@observer@*/ constraintTerm t,  FILE *f)
 
            ostr2 = str2;
            t = ctype_undump(&str2) ;
-           s = sRef_makeParam (param, t );
+           s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc));
            free (ostr2);
          }
        else  //This must be an identified that we can search for

diff --git a/src/context.c b/src/context.c
index ac81cc73a8c052b9035ec739182f844e62df5581..a4963c21c2885d3cfeb659d0dd8f60ea0502d5ce 100644 (file)
--- a/src/context.c
+++ b/src/context.c
@@ -3344,18 +3344,15 @@ void
 context_saveLocation (void)
 {
   /* was llassert (fileloc_isUndefined (gc.saveloc)) */
-      fileloc_free (gc.saveloc);
-    
-
+  fileloc_free (gc.saveloc);
   gc.saveloc = fileloc_copy (g_currentloc);
-  }
+}
 
 fileloc
 context_getSaveLocation (void)
 {
   fileloc fl = gc.saveloc;
-
-    gc.saveloc = fileloc_undefined;
+  gc.saveloc = fileloc_undefined;
   return fl;
 }
 
@@ -4390,7 +4387,7 @@ void context_addMetaState (cstring mname, metaStateInfo msinfo)
     }
 }
 
-valueTable context_createValueTable (sRef s)
+valueTable context_createValueTable (sRef s, stateInfo sinfo)
 {
   if (metaStateTable_size (gc.stateTable) > 0)
     {
@@ -4410,8 +4407,8 @@ valueTable context_createValueTable (sRef s)
              valueTable_insert 
                (res,
                 cstring_copy (metaStateInfo_getName (msi)),
-                stateValue_createImplicit (metaStateInfo_getDefaultValue (msi, s),
-                                           stateInfo_undefined));
+                stateValue_createImplicit (metaStateInfo_getDefaultValue (msi, s), 
+                                           stateInfo_copy (sinfo)));
            }
          else
            {
@@ -4420,16 +4417,18 @@ valueTable context_createValueTable (sRef s)
        } 
       end_metaStateTable_elements ;
       
+      stateInfo_free (sinfo);
       DPRINTF (("Value table: %s", valueTable_unparse (res)));
       return res;
     }
   else
     {
+      stateInfo_free (sinfo);
       return valueTable_undefined;
     }
 }
 
-valueTable context_createGlobalMarkerValueTable ()
+valueTable context_createGlobalMarkerValueTable (stateInfo sinfo)
 {
   if (metaStateTable_size (gc.stateTable) > 0)
     {
@@ -4445,15 +4444,17 @@ valueTable context_createGlobalMarkerValueTable ()
          valueTable_insert (res,
                             cstring_copy (metaStateInfo_getName (msi)),
                             stateValue_create (metaStateInfo_getDefaultGlobalValue (msi),
-                                               stateInfo_undefined));
+                                               stateInfo_copy (sinfo)));
        } 
       end_metaStateTable_elements ;
       
+      stateInfo_free (sinfo);
       DPRINTF (("Value table: %s", valueTable_unparse (res)));
       return res;
     }
   else
     {
+      stateInfo_free (sinfo);
       return valueTable_undefined;
     }
 }

diff --git a/src/cscanner.l b/src/cscanner.l
index db64bb0843741568e5c189fee1efe31698f28a45..3cc9e38543cab6b7c45d762aa0add942f5d727a5 100644 (file)
--- a/src/cscanner.l
+++ b/src/cscanner.l
@@ -1523,6 +1523,7 @@ static bool processMacro (void)
              && !uentry_isElipsisMarker (uentryList_getN 
                                          (specparams, paramno)))
            {
+             fileloc sloc = context_getSaveLocation ();
              uentry decl = uentryList_getN (specparams, paramno);
              sRef sr;
              
@@ -1530,7 +1531,7 @@ static bool processMacro (void)
 
                              
              uentry_setParam (param);
-             sr = sRef_makeParam (paramno, uentry_getType (param));
+             sr = sRef_makeParam (paramno, uentry_getType (param), stateInfo_makeLoc (sloc));
 
              if (sRef_getNullState (sr) == NS_ABSNULL)
                {
@@ -1547,12 +1548,12 @@ static bool processMacro (void)
                    }
                  else
                    {
-                     sRef_setNullState (sr, NS_UNKNOWN, g_currentloc);
+                     sRef_setNullState (sr, NS_UNKNOWN, sloc);
                    }
                }
 
              uentry_setSref (param, sr);
-             uentry_setDeclaredForceOnly (param, context_getSaveLocation ());
+             uentry_setDeclaredForceOnly (param, sloc);
 
              skipparam = isiter && uentry_isOut (uentryList_getN (specparams, paramno));
            }
@@ -1561,11 +1562,11 @@ static bool processMacro (void)
              fileloc sloc = context_getSaveLocation ();
 
              param = uentry_makeVariableSrefParam 
-               (paramname, ctype_unknown, sRef_makeParam (paramno, ctype_unknown));
+               (paramname, ctype_unknown, fileloc_copy (sloc), 
+                sRef_makeParam (paramno, ctype_unknown, stateInfo_makeLoc (sloc)));
              cstring_free (paramname);
 
              sRef_setPosNull  (uentry_getSref (param), sloc);
-
              uentry_setDeclaredForce (param, sloc);
 
              skipparam = FALSE;

diff --git a/src/exprNode.c b/src/exprNode.c
index 4b48356ee7ca48b35df75439296a95ab7e988b8c..4091c410e6bebf0ebe3e4ced43b23e7fb3ae7641 100644 (file)
--- a/src/exprNode.c
+++ b/src/exprNode.c
@@ -3208,6 +3208,8 @@ reflectEnsuresClause (exprNode ret, uentry le, exprNode f, exprNodeList args)
 
       if (uentry_hasMetaStateEnsures (le))
        {
+         fileloc loc = exprNode_loc (f);
+
          metaStateConstraintList mscl = uentry_getMetaStateEnsures (le);
 
          metaStateConstraintList_elements (mscl, msc)
@@ -3215,7 +3217,7 @@ reflectEnsuresClause (exprNode ret, uentry le, exprNode f, exprNodeList args)
              metaStateSpecifier msspec = metaStateConstraint_getSpecifier (msc);
              metaStateInfo msinfo = metaStateSpecifier_getMetaStateInfo (msspec);
              metaStateExpression msexpr = metaStateConstraint_getExpression (msc);
-             cstring key = metaStateInfo_getName (msinfo);
+             cstring key = metaStateInfo_getName (msinfo);           
              sRef mlsr = metaStateSpecifier_getSref (msspec);
              sRef s;
              sRef lastref = sRef_undefined;
@@ -3239,10 +3241,9 @@ reflectEnsuresClause (exprNode ret, uentry le, exprNode f, exprNodeList args)
              while (metaStateExpression_isDefined (msexpr)) 
                {
                  metaStateSpecifier ms = metaStateExpression_getSpecifier (msexpr);
-                 sRef msr = metaStateSpecifier_getSref (ms);
                  metaStateInfo msi = metaStateSpecifier_getMetaStateInfo (ms);
-                 sRef fs;
-                 
+                 sRef msr, fs;
+
                  DPRINTF (("Check expression: %s", metaStateExpression_unparse (msexpr)));
                  
                  if (metaStateExpression_isMerge (msexpr))
@@ -3260,72 +3261,167 @@ reflectEnsuresClause (exprNode ret, uentry le, exprNode f, exprNodeList args)
                      llassert (metaStateInfo_equal (msinfo, msi));
                    }
                  
-                 llassert (sRef_isParam (sRef_getRootBase (msr)));
-                 fs = sRef_fixBaseParam (msr, args);
-                 
-                 if (stateValue_isDefined (sval))
+                 if (metaStateSpecifier_isElipsis (ms))
                    {
-                     /* Use combination table to merge old state value with new one: */
-                     stateValue tval = sRef_getMetaStateValue (fs, key);
+                     /*
+                     ** For elipsis, we need to merge all the relevant elipsis parameters
+                     ** 
+                     */
                      
-                     if (stateValue_isDefined (tval))
+                     uentryList params = uentry_getParams (le);
+                     int paramno = uentryList_size (params) - 1;
+
+                     if (!uentry_isElipsisMarker (uentryList_getN (params, paramno)))
                        {
-                         stateCombinationTable sctable = metaStateInfo_getMergeTable (msinfo);
-                         cstring msg = cstring_undefined;
-                         int nval = stateCombinationTable_lookup (sctable, 
-                                                                  stateValue_getValue (sval), 
-                                                                  stateValue_getValue (tval), 
-                                                                  &msg);
-                         DPRINTF (("Combining: %s + %s -> %d",
-                                   stateValue_unparseValue (sval, msinfo),
-                                   stateValue_unparseValue (tval, msinfo),
-                                   nval));
-                         
-                         if (nval == stateValue_error)
+                         voptgenerror 
+                           (FLG_TYPE,
+                            message ("Ensures clauses uses ... for function without ... in parameter list: %q",
+                                     uentry_getName (le)),
+                            uentry_whereLast (le));
+                         /*@innerbreak@*/ break;
+                       }
+
+                     while (paramno < exprNodeList_size (args))
+                       {
+                         exprNode arg = exprNodeList_getN (args, paramno);
+                         fs = exprNode_getSref (arg);
+                         DPRINTF (("Merge arg: %s", exprNode_unparse (arg)));
+
+                         /* cut and pasted... gack*/
+                         if (stateValue_isDefined (sval))
                            {
-                             llassert (cstring_isDefined (msg));
+                             /* Use combination table to merge old state value with new one: */
+                             stateValue tval = sRef_getMetaStateValue (fs, key);
                              
-                             if (optgenerror 
-                                 (FLG_STATEMERGE,
-                                  message
-                                  ("Attributes merged in ensures clause in states that "
-                                   "cannot be combined (%q is %q, %q is %q): %s",
-                                   sRef_unparse (lastref),
-                                   stateValue_unparseValue (sval, msinfo),
-                                   sRef_unparse (fs),
-                                   stateValue_unparseValue (tval, msinfo),
-                                   msg),
-                                  exprNode_loc (f)))
+                             if (stateValue_isDefined (tval))
+                               {
+                                 stateCombinationTable sctable = metaStateInfo_getMergeTable (msinfo);
+                                 cstring msg = cstring_undefined;
+                                 int nval = stateCombinationTable_lookup (sctable, 
+                                                                          stateValue_getValue (sval), 
+                                                                          stateValue_getValue (tval), 
+                                                                          &msg);
+                                 DPRINTF (("Combining: %s + %s -> %d",
+                                           stateValue_unparseValue (sval, msinfo),
+                                           stateValue_unparseValue (tval, msinfo),
+                                           nval));
+                                 
+                                 if (nval == stateValue_error)
+                                   {
+                                     llassert (cstring_isDefined (msg));
+                                     
+                                     if (optgenerror 
+                                         (FLG_STATEMERGE,
+                                          message
+                                          ("Attributes merged in ensures clause in states that "
+                                           "cannot be combined (%q is %q, %q is %q): %s",
+                                           sRef_unparse (lastref),
+                                           stateValue_unparseValue (sval, msinfo),
+                                           sRef_unparse (fs),
+                                           stateValue_unparseValue (tval, msinfo),
+                                           msg),
+                                          exprNode_loc (f)))
+                                       {
+                                         sRef_showMetaStateInfo (fs, key);
+                                       }                   
+                                   }
+                                 
+                                 stateValue_updateValueLoc (sval, nval, fileloc_undefined);
+                                 loc = exprNode_loc (arg);
+                               }
+                             else
                                {
-                                 sRef_showMetaStateInfo (fs, key);
-                               }                   
+                                 DPRINTF (("No value for: %s:%s", sRef_unparse (fs), key));
+                               }
+                           }
+                         else
+                           {
+                             sval = sRef_getMetaStateValue (fs, key);
                            }
                          
-                         stateValue_updateValueLoc (sval, nval, fileloc_undefined);
-                       }
-                     else
-                       {
-                         DPRINTF (("No value for: %s:%s", sRef_unparse (fs), key));
+                         lastref = fs;
+                         
+                         if (stateValue_isError (sval))
+                           {
+                             /*@innerbreak@*/ break; /* Don't merge any more values if here was an error */
+                           }
+                       
+                         
+                         paramno++;
                        }
                    }
                  else
                    {
-                     sval = sRef_getMetaStateValue (fs, key);
-                   }
+                     msr = metaStateSpecifier_getSref (ms);
                  
-                 lastref = fs;
-                 
-                 if (stateValue_isError (sval))
-                   {
-                     /*@innerbreak@*/ break; /* Don't merge any more values if here was an error */
+                     
+                     llassert (sRef_isParam (sRef_getRootBase (msr)));
+                     fs = sRef_fixBaseParam (msr, args);
+                     
+                     if (stateValue_isDefined (sval))
+                       {
+                         /* Use combination table to merge old state value with new one: */
+                         stateValue tval = sRef_getMetaStateValue (fs, key);
+                         
+                         if (stateValue_isDefined (tval))
+                           {
+                             stateCombinationTable sctable = metaStateInfo_getMergeTable (msinfo);
+                             cstring msg = cstring_undefined;
+                             int nval = stateCombinationTable_lookup (sctable, 
+                                                                      stateValue_getValue (sval), 
+                                                                      stateValue_getValue (tval), 
+                                                                      &msg);
+                             DPRINTF (("Combining: %s + %s -> %d",
+                                       stateValue_unparseValue (sval, msinfo),
+                                       stateValue_unparseValue (tval, msinfo),
+                                       nval));
+                             
+                             if (nval == stateValue_error)
+                               {
+                                 llassert (cstring_isDefined (msg));
+                                 
+                                 if (optgenerror 
+                                     (FLG_STATEMERGE,
+                                      message
+                                      ("Attributes merged in ensures clause in states that "
+                                       "cannot be combined (%q is %q, %q is %q): %s",
+                                       sRef_unparse (lastref),
+                                       stateValue_unparseValue (sval, msinfo),
+                                       sRef_unparse (fs),
+                                       stateValue_unparseValue (tval, msinfo),
+                                       msg),
+                                      exprNode_loc (f)))
+                                   {
+                                     sRef_showMetaStateInfo (fs, key);
+                                   }               
+                               }
+                             
+                             stateValue_updateValueLoc (sval, nval, fileloc_undefined);
+                           }
+                         else
+                           {
+                             DPRINTF (("No value for: %s:%s", sRef_unparse (fs), key));
+                           }
+                       }
+                     else
+                       {
+                         sval = sRef_getMetaStateValue (fs, key);
+                       }
+                     
+                     lastref = fs;
+                     
+                     if (stateValue_isError (sval))
+                       {
+                         /*@innerbreak@*/ break; /* Don't merge any more values if here was an error */
+                       }
                    }
                }
-             
+
              DPRINTF (("Setting: %s:%s <- %s", sRef_unparse (s), key, stateValue_unparse (sval)));
              
              if (stateValue_isDefined (sval))
                {
-                 sRef_setMetaStateValueComplete (s, key, stateValue_getValue (sval), exprNode_loc (f));
+                 sRef_setMetaStateValueComplete (s, key, stateValue_getValue (sval), loc);
                }
              else
                {

diff --git a/src/metaStateSpecifier.c b/src/metaStateSpecifier.c
index 28525d87e318397b30e4da3283a65eba2bb861b5..51e68a7e1a49ea69e3f473f8f7832173a748740a 100644 (file)
--- a/src/metaStateSpecifier.c
+++ b/src/metaStateSpecifier.c
@@ -34,12 +34,30 @@ metaStateSpecifier_create (/*@only@*/ sRef sr, /*@observer@*/ metaStateInfo msin
   metaStateSpecifier res = (metaStateSpecifier) dmalloc (sizeof (*res));
   res->sr = sr;
   res->msinfo = msinfo;
+  res->elipsis = FALSE;
   return res;
 }
 
+metaStateSpecifier 
+metaStateSpecifier_createElipsis (/*@observer@*/ metaStateInfo msinfo)
+{
+  metaStateSpecifier res = (metaStateSpecifier) dmalloc (sizeof (*res));
+  res->sr = sRef_undefined;
+  res->msinfo = msinfo;
+  res->elipsis = TRUE;
+  return res;
+}
+
+bool
+metaStateSpecifier_isElipsis (metaStateSpecifier m)
+{
+  return m->elipsis;
+}
+
 sRef
 metaStateSpecifier_getSref (metaStateSpecifier m)
 {
+  llassert (!metaStateSpecifier_isElipsis (m));
   return m->sr;
 }
 
@@ -52,14 +70,29 @@ metaStateSpecifier_getMetaStateInfo (metaStateSpecifier m)
 metaStateSpecifier 
 metaStateSpecifier_copy (metaStateSpecifier m)
 {
-  return metaStateSpecifier_create (sRef_saveCopy (m->sr), m->msinfo);
+  if (metaStateSpecifier_isElipsis (m))
+    {
+      return metaStateSpecifier_createElipsis (m->msinfo);
+    }
+  else
+    {
+      return metaStateSpecifier_create (sRef_saveCopy (m->sr), m->msinfo);
+    }
 }
 
 cstring metaStateSpecifier_unparse (metaStateSpecifier m) 
 {
-  return message ("%q:%s", 
-                 sRef_unparse (m->sr),
-                 metaStateInfo_getName (m->msinfo));
+  if (m->elipsis)
+    {
+      return message ("...:%s", 
+                     metaStateInfo_getName (m->msinfo));
+    }
+  else
+    {
+      return message ("%q:%s", 
+                     sRef_unparse (m->sr),
+                     metaStateInfo_getName (m->msinfo));
+    }
 }
 
 void metaStateSpecifier_free (/*@only@*/ metaStateSpecifier m) 

diff --git a/src/mtContextNode.c b/src/mtContextNode.c
index 9f89c870eecb1820a0f47a3abc0ceb3958834ec7..22a29267aec9fa7def0805a7075fd1d0f7c05f5c 100644 (file)
--- a/src/mtContextNode.c
+++ b/src/mtContextNode.c
@@ -114,8 +114,9 @@ bool mtContextNode_matchesEntry (mtContextNode context, uentry ue)
        }
       break;
     case MTC_PARAM: 
-      if (!uentry_isParam (ue))
+      if (!uentry_isAnyParam (ue))
        {
+         DPRINTF (("not param: %s", uentry_unparseFull (ue)));
          return FALSE;
        }
       break;

diff --git a/src/sRef.c b/src/sRef.c
index e637ba5117ccf8ead9946b2800a9718d6440a0c2..fcdf105b612b0bd211716d4876683cc540dded31 100644 (file)
--- a/src/sRef.c
+++ b/src/sRef.c
@@ -2325,7 +2325,7 @@ sRef_undumpGlobal (char **c)
        reader_checkChar (c, '@');
        nullstate = nstate_fromInt (reader_getInt (c));
 
-       ret = sRef_makeGlobal (uid, ctype_unknown);
+       ret = sRef_makeGlobal (uid, ctype_unknown, stateInfo_currentLoc ());
        sRef_setNullStateN (ret, nullstate);
        ret->defstate = defstate;
        return ret;
@@ -2367,9 +2367,9 @@ static /*@exposed@*/ sRef sRef_undumpBody (char **c)
   switch (p)
     {
     case 'g':
-      return (sRef_makeGlobal (usymId_fromInt (reader_getInt (c)), ctype_unknown));
+      return (sRef_makeGlobal (usymId_fromInt (reader_getInt (c)), ctype_unknown, stateInfo_currentLoc ()));
     case 'p':
-      return (sRef_makeParam (reader_getInt (c), ctype_unknown));
+      return (sRef_makeParam (reader_getInt (c), ctype_unknown, stateInfo_makeLoc (g_currentloc)));
     case 'r':
       return (sRef_makeResult (ctype_undump (c)));
     case 'a':
@@ -3106,7 +3106,7 @@ bool sRef_isUnconstrained (sRef s)
 }
 
 static /*@dependent@*/ /*@notnull@*/ sRef 
-  sRef_makeCvarAux (int level, usymId index, ctype ct)
+  sRef_makeCvarAux (int level, usymId index, ctype ct, /*@only@*/ stateInfo stinfo)
 {
   sRef s = sRef_newRef ();
   
@@ -3147,13 +3147,13 @@ static /*@dependent@*/ /*@notnull@*/ sRef
 
   DPRINTF (("Made cvar: [%p] %s", s, sRef_unparseDebug (s)));
   llassert (valueTable_isUndefined (s->state));
-  s->state = context_createValueTable (s);
+  s->state = context_createValueTable (s, stinfo); 
   return s;
 }
 
-/*@dependent@*/ sRef sRef_makeCvar (int level, usymId index, ctype ct)
+/*@dependent@*/ sRef sRef_makeCvar (int level, usymId index, ctype ct, /*@only@*/ stateInfo stinfo)
 {
-  return (sRef_makeCvarAux (level, index, ct));
+  return (sRef_makeCvarAux (level, index, ct, stinfo));
 }
 
 int sRef_lexLevel (sRef s)
@@ -3175,9 +3175,9 @@ int sRef_lexLevel (sRef s)
 }
 
 sRef
-sRef_makeGlobal (usymId l, ctype ct)
+sRef_makeGlobal (usymId l, ctype ct, /*@only@*/ stateInfo stinfo)
 {
-  return (sRef_makeCvar (globScope, l, ct));
+  return (sRef_makeCvar (globScope, l, ct, stinfo));
 }
 
 void
@@ -3189,7 +3189,7 @@ sRef_setParamNo (sRef s, int l)
 }
 
 /*@dependent@*/ sRef
-sRef_makeParam (int l, ctype ct)
+sRef_makeParam (int l, ctype ct, stateInfo stinfo)
 {
   sRef s = sRef_new ();
 
@@ -3203,7 +3203,7 @@ sRef_makeParam (int l, ctype ct)
   /* (probably defined, unless its an out parameter) */
 
   llassert (valueTable_isUndefined (s->state));
-  s->state = context_createValueTable (s);
+  s->state = context_createValueTable (s, stinfo);
   return s;
 }
 
@@ -3291,7 +3291,7 @@ static bool sRef_isZerothArrayFetch (/*@notnull@*/ sRef s)
        }
 
       llassert (valueTable_isUndefined (s->state));
-      s->state = context_createValueTable (s);
+      s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
       return s;
     }
 }
@@ -3464,7 +3464,7 @@ sRef_makeObject (ctype o)
   s->info = (sinfo) dmalloc (sizeof (*s->info));
   s->info->object = o;
   llassert (valueTable_isUndefined (s->state));
-  s->state = context_createValueTable (s);
+  s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
   return s;
 }
 
@@ -3483,7 +3483,7 @@ sRef sRef_makeExternal (sRef t)
   s->type = t->type;
   s->info->ref = t; /* sRef_copy (t); */ /*@i32 was exposed@*/
   llassert (valueTable_isUndefined (s->state));
-  s->state = context_createValueTable (s);
+  s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
   return s;
 }
 
@@ -3499,7 +3499,7 @@ sRef sRef_makeExternal (sRef t)
       
       s->type = t->type;
       llassert (valueTable_isUndefined (s->state));
-      s->state = context_createValueTable (s);
+      s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
       return s;
     }
   else
@@ -4310,7 +4310,7 @@ sRef sRef_makeConj (/*@exposed@*/ /*@returned@*/ sRef a, /*@exposed@*/ sRef b)
       s->aliaskind = alkind_resolve (a->aliaskind, b->aliaskind);
 
       llassert (valueTable_isUndefined (s->state));
-      s->state = context_createValueTable (s);
+      s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
       return s;
     }
   else
@@ -4395,7 +4395,7 @@ sRef_makeGlobalMarker (void)
 {
   sRef s = sRef_makeSpecial (SR_GLOBALMARKER);
   llassert (valueTable_isUndefined (s->state));
-  s->state = context_createGlobalMarkerValueTable ();
+  s->state = context_createGlobalMarkerValueTable (stateInfo_undefined);
   return s;
 }
 
@@ -4410,7 +4410,7 @@ sRef_makeResult (ctype c)
   s->aliaskind = AK_UNKNOWN;
   sRef_setNullStateN (s, NS_UNKNOWN);
   llassert (valueTable_isUndefined (s->state));
-  s->state = context_createValueTable (s);
+  s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
 
   DPRINTF (("Result: [%p] %s", s, sRef_unparseFull (s)));
   return s;
@@ -6498,7 +6498,7 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
       
       if (valueTable_isUndefined (s->state))
        {
-         s->state = context_createValueTable (s);
+         s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
        }
 
       return (s);
@@ -6556,7 +6556,7 @@ void sRef_setArrayFetchState (/*@notnull@*/ /*@exposed@*/ sRef s,
       sRef_addDeriv (arr, s);
 
       llassert (valueTable_isUndefined (s->state));
-      s->state = context_createValueTable (s);
+      s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
 
       return (s);
     }
@@ -6792,7 +6792,7 @@ sRef_constructPointerAux (/*@notnull@*/ /*@exposed@*/ sRef t)
 
   if (valueTable_isUndefined (s->state))
     {
-      s->state = context_createValueTable (s);
+      s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
     }
 
   return s;
@@ -7143,7 +7143,7 @@ sRef_makeType (ctype ct)
   s->oaliaskind = s->aliaskind;
   s->oexpkind = s->expkind;
   llassert (valueTable_isUndefined (s->state));
-  s->state = context_createValueTable (s);
+  s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
 
   DPRINTF (("Create: %s", sRef_unparseFull (s)));
   return s;
@@ -7180,7 +7180,7 @@ sRef_makeConst (ctype ct)
   s->oexpkind = s->expkind;
 
   llassert (valueTable_isUndefined (s->state));
-  s->state = context_createValueTable (s);
+  s->state = context_createValueTable (s, stateInfo_makeLoc (g_currentloc));
 
   return s;
 }

diff --git a/src/stateClauseList.c b/src/stateClauseList.c
index a7038370f9ff086d26b040cfb51af12533b829c5..0afa765d99cd395eeadb3b14e4e3cf39d804f599 100644 (file)
--- a/src/stateClauseList.c
+++ b/src/stateClauseList.c
@@ -273,7 +273,7 @@ void stateClauseList_checkAll (uentry ue)
                    {
                      if (optgenerror
                          (FLG_ANNOTATIONERROR,
-                          message ("Meta state anntation %s used on inappropriate reference %q in %q clause of %q: %q",
+                          message ("Meta state annotation %s used on inappropriate reference %q in %q clause of %q: %q",
                                    qual_unparse (q),
                                    sRef_unparse (el),
                                    stateClause_unparseKind (cl),

diff --git a/src/stateInfo.c b/src/stateInfo.c
index d0b9a2fda7d47566d7c2f633cb9d738fc387cba7..06542e59847e7a815b189273da2a9ed55ec998b4 100644 (file)
--- a/src/stateInfo.c
+++ b/src/stateInfo.c
@@ -111,6 +111,12 @@ void stateInfo_free (/*@only@*/ stateInfo a)
     }
 }
 
+/*@only@*/ /*@notnull@*/ stateInfo
+stateInfo_currentLoc (void)
+{
+  return stateInfo_makeLoc (g_currentloc);
+}
+
 /*@only@*/ /*@notnull@*/ stateInfo
 stateInfo_makeLoc (fileloc loc)
 {

diff --git a/src/uentry.c b/src/uentry.c
index e4646e863822d6cda6db4f9e13495677ba0e9a71..0c79b938068cd08c98250c21865d84eac76bb0f0 100644 (file)
--- a/src/uentry.c
+++ b/src/uentry.c
@@ -1272,13 +1272,14 @@ static void uentry_implicitParamAnnots (/*@notnull@*/ uentry e)
 }
 
 static /*@only@*/ /*@notnull@*/ uentry 
-uentry_makeVariableParamAux (cstring n, ctype t, /*@dependent@*/ sRef s, sstate defstate) /*@i32 exposed*/
+uentry_makeVariableParamAux (cstring n, ctype t, /*@dependent@*/ sRef s, 
+                            /*@only@*/ fileloc loc, sstate defstate) /*@i32 exposed*/
 {
   cstring pname = makeParam (n);
   uentry e;
 
   DPRINTF (("Sref: %s", sRef_unparseFull (s)));
-  e = uentry_makeVariableAux (pname, t, setLocation (), s, FALSE, VKPARAM);
+  e = uentry_makeVariableAux (pname, t, loc, s, FALSE, VKPARAM);
 
   cstring_free (pname);
   DPRINTF (("Param: %s", uentry_unparseFull (e)));
@@ -1410,9 +1411,9 @@ void checkGlobalsModifies (/*@notnull@*/ uentry ue, sRefSet sr)
 }
 
 uentry
-uentry_makeVariableSrefParam (cstring n, ctype t, /*@exposed@*/ sRef s)
+uentry_makeVariableSrefParam (cstring n, ctype t, /*@only@*/ fileloc loc, /*@exposed@*/ sRef s)
 {
-  return (uentry_makeVariableParamAux (n, t, s, SS_UNKNOWN));
+  return (uentry_makeVariableParamAux (n, t, s, loc, SS_UNKNOWN));
 }
 
 void
@@ -2438,7 +2439,7 @@ uentry_reflectOtherQualifier (/*@notnull@*/ uentry ue, qual qel)
        {
          if (optgenerror
              (FLG_ANNOTATIONERROR,
-              message ("Meta state anntation %s used in inconsistent context: %q",
+              message ("Meta state annotation %s used in inconsistent context: %q",
                        qual_unparse (qel),
                        uentry_unparse (ue)),
               uentry_whereLast (ue)))
@@ -3012,9 +3013,11 @@ uentry_isSpecialFunction (uentry ue)
 {
   ctype ct = idDecl_getCtype (t);
   ctype base = ct;
-  sRef pref = sRef_makeParam (i, ct);
-  uentry ue = uentry_makeVariableSrefParam (idDecl_observeId (t), ct, pref);
+  fileloc loc = setLocation ();
+  sRef pref = sRef_makeParam (i, ct, stateInfo_makeLoc (loc));
+  uentry ue = uentry_makeVariableSrefParam (idDecl_observeId (t), ct, loc, pref);
 
+  DPRINTF (("Make param: %s", uentry_unparseFull (ue)));
   uentry_reflectQualifiers (ue, idDecl_getQuals (t));
   uentry_implicitParamAnnots (ue);
 
@@ -3073,9 +3076,9 @@ uentry_isSpecialFunction (uentry ue)
 }
 
 # ifndef NOLCL
-/*@notnull@*/ uentry uentry_makeVariableParam (cstring n, ctype t)
+/*@notnull@*/ uentry uentry_makeVariableParam (cstring n, ctype t, fileloc loc)
 {
-  return (uentry_makeVariableParamAux (n, t, sRef_makeType (t), SS_DEFINED));
+  return (uentry_makeVariableParamAux (n, t, sRef_makeType (t), fileloc_copy (loc), SS_DEFINED));
 }
 # endif
 
@@ -3277,11 +3280,11 @@ static /*@only@*/ /*@notnull@*/
   e->info->var->defstate = sRef_getDefState (e->sref);  
   e->info->var->nullstate = sRef_getNullState (e->sref);
 
-/* start modifications */
-/* This function sets the uentry for a pointer or array variable declaration,
-   it allocates memory and sets the fields. We check if the type of the variable
-   is a pointer or array and allocate a `bbufinfo' struct accordingly */
-
+  /* start modifications */
+  /* This function sets the uentry for a pointer or array variable declaration,
+     it allocates memory and sets the fields. We check if the type of the variable
+     is a pointer or array and allocate a `bbufinfo' struct accordingly */
+  
   if( ctype_isArray (t) || ctype_isPointer(t)) {
     /*@i222@*/e->info->var->bufinfo = dmalloc( sizeof(*e->info->var->bufinfo) );
      e->info->var->bufinfo->bufstate = BB_NOTNULLTERMINATED;
@@ -7247,6 +7250,10 @@ paramTypeError (uentry old, uentry oldCurrent, ctype oldType,
   
   if (hasError)
     {
+      DPRINTF (("Here: %s / %s",
+               uentry_unparseFull (oldCurrent),
+               uentry_unparseFull (newCurrent)));
+
       if (!uentry_isUndefined (oldCurrent))
        {
          if (!uentry_isUndefined (newCurrent) 

diff --git a/src/usymtab.c b/src/usymtab.c
index 73c45f2250090b3c2c45f4c6f1f924621e06a27d..bb2c40c31f4a07c1f7e34b77fdec4c1617e4b72b 100644 (file)
--- a/src/usymtab.c
+++ b/src/usymtab.c
@@ -503,7 +503,8 @@ usymtab_addEntryBase (/*@notnull@*/ usymtab s, /*@only@*/ uentry e)
       if (uentry_isVar (e))
        {
          uentry_setSref (e, sRef_makeCvar (globScope, thisentry, 
-                                           uentry_getType (e)));
+                                           uentry_getType (e),
+                                           stateInfo_makeLoc (uentry_whereLast (e))));
        }
       
       usymtab_addEntryQuiet (s, e);
@@ -542,7 +543,8 @@ usymtab_addEntryAlways (/*@notnull@*/ usymtab s, /*@only@*/ uentry e)
   if (uentry_isVar (e) && !uentry_isGlobalMarker (e))
     {
       uentry_setSref (e, sRef_makeCvar (globScope, thisentry, 
-                                       uentry_getType (e)));
+                                       uentry_getType (e),
+                                       stateInfo_makeLoc (uentry_whereLast (e))));
     }
   
   usymtab_addEntryQuiet (s, e);
@@ -583,7 +585,7 @@ usymtab_addEntryAux (/*@notnull@*/ usymtab st, /*@keep@*/ uentry e, bool isSref)
 
       if (uentry_isStatic (e))
        {
-         sRef sr = sRef_makeCvar (st->lexlevel, thisentry, ct);
+         sRef sr = sRef_makeCvar (st->lexlevel, thisentry, ct, stateInfo_makeLoc (uentry_whereLast (e)));
 
          if (sRef_isStack (sr) || sRef_isLocalState (sr))
            {
@@ -595,10 +597,9 @@ usymtab_addEntryAux (/*@notnull@*/ usymtab st, /*@keep@*/ uentry e, bool isSref)
        }
       else
        {
-         uentry_setSref (e, sRef_makeCvar (st->lexlevel, thisentry, ct));
+         uentry_setSref (e, sRef_makeCvar (st->lexlevel, thisentry, ct, stateInfo_makeLoc (uentry_whereLast (e))));
        }
-
-          }
+    }
 
   if (uentry_isDatatype (e))
     {
@@ -906,8 +907,8 @@ usymtab_supEntryAux (/*@notnull@*/ usymtab st,
              ct = ctype_getReturnType (ct);
            }
          
-         uentry_setSref (ce, sRef_makeCvar (st->lexlevel, eindex, ct));
-               }
+         uentry_setSref (ce, sRef_makeCvar (st->lexlevel, eindex, ct, stateInfo_makeLoc (uentry_whereLast (ce))));
+       }
     }
   else /* no previous entry */
     {

diff --git a/src/usymtab_interface.c b/src/usymtab_interface.c
index 87e414d0696156c6a7bd37ba1ceb0487ffadfe7c..7bc8addb08c503f7a2287987b68e0fa0a5df2b39 100644 (file)
--- a/src/usymtab_interface.c
+++ b/src/usymtab_interface.c
@@ -1577,14 +1577,13 @@ static /*@exposed@*/ sRef fixTermNode (termNode n, fcnNode f, uentryList cl)
                          }
                      }
                    else
-                     return (sRef_makeGlobal (usym, ctype_unknown));
+                     return (sRef_makeGlobal (usym, ctype_unknown, stateInfo_currentLoc ()));
                  }
                
                else
                  {
-                   sRef p = sRef_makeParam (i, ctype_unknown);
-
-                                   return (p);
+                   sRef p = sRef_makeParam (i, ctype_unknown, stateInfo_currentLoc ());
+                   return (p);
                  }
              }
          }
@@ -1700,7 +1699,7 @@ paramNode_toUentry (paramNode p)
          ctype cr = convertTypeExpr (qtype_getType (ct), p->paramdecl);
          cstring pname = (p->paramdecl == (typeExpr)0) ? cstring_undefined 
                                                        : paramNode_name (p);
-         uentry ue = uentry_makeVariableParam (pname, cr);
+         uentry ue = uentry_makeVariableParam (pname, cr, g_currentloc);
 
          uentry_reflectQualifiers (ue, qtype_getQuals (ct));
          qtype_free (ct);

diff --git a/src/warnClause.c b/src/warnClause.c
index e9fbc863cea19fc404554ddbb2142f6c72e17f94..059ec9af578d421c423b05005919033ddd84dd4b 100644 (file)
--- a/src/warnClause.c
+++ b/src/warnClause.c
@@ -30,7 +30,7 @@
 
 static warnClause warnClause_createAux (/*@only@*/ fileloc loc, 
                                        /*@only@*/ flagSpec flag, 
-                                       /*@only@*/ exprNode msg)
+                                       /*@only@*/ cstring msg)
 {
   warnClause res = (warnClause) dmalloc (sizeof (*res));
   
@@ -41,14 +41,10 @@ static warnClause warnClause_createAux (/*@only@*/ fileloc loc,
   return res;
 }
 
-extern warnClause warnClause_create (lltok tok, flagSpec flag, exprNode msg) 
+extern warnClause warnClause_create (lltok tok, flagSpec flag, cstring msg) 
 {
   warnClause res;
-  DPRINTF (("Create warn message: %s/ %s ", 
-           flagSpec_unparse (flag), exprNode_unparse(msg)));
-  
-  res = warnClause_createAux (lltok_stealLoc (tok),
-                             flag, msg);
+  res = warnClause_createAux (lltok_stealLoc (tok), flag, msg);
   lltok_release (tok);
   return res;
 }
@@ -59,7 +55,7 @@ warnClause warnClause_copy (warnClause w)
     {
       return warnClause_createAux (fileloc_copy (w->loc),
                                   flagSpec_copy (w->flag),
-                                  w->msg); /*@i32 should exprNode_copy (w->msg)); */
+                                  cstring_copy (w->msg)); 
     }
   else
     {
@@ -69,6 +65,7 @@ warnClause warnClause_copy (warnClause w)
 
 extern flagSpec warnClause_getFlag (warnClause w)
 {
+  llassert (warnClause_isDefined (w));
   return w->flag;
 }
 
@@ -76,8 +73,7 @@ extern cstring warnClause_unparse (warnClause w)
 {
   if (warnClause_isDefined (w))
     {
-      return message ("<%q> %s",
-                     flagSpec_unparse (w->flag), exprNode_unparse (w->msg));
+      return message ("<%q> %s", flagSpec_unparse (w->flag), w->msg);
     }
   else
     {
@@ -87,15 +83,13 @@ extern cstring warnClause_unparse (warnClause w)
 
 extern bool warnClause_hasMessage (warnClause w)
 {
-  return warnClause_isDefined (w) && exprNode_isDefined (w->msg)
-    && cstring_isDefined (multiVal_forceString (exprNode_getValue (w->msg)));
+  return warnClause_isDefined (w) && cstring_isDefined (w->msg);
 }
 
 extern /*@observer@*/ cstring warnClause_getMessage (warnClause w)
 {
-  if (warnClause_isDefined (w) && exprNode_isDefined (w->msg)) {
-    llassert (exprNode_knownStringValue (w->msg));
-    return multiVal_forceString (exprNode_getValue (w->msg));
+  if (warnClause_isDefined (w)) {
+    return w->msg;
   } else {
     return cstring_undefined;
   }
@@ -107,8 +101,8 @@ extern void warnClause_free (warnClause w)
   if (warnClause_isDefined (w))
     {
       flagSpec_free (w->flag);
-      /*@i43 should be copied! exprNode_free (w->msg); */
       fileloc_free (w->loc);
+      cstring_free (w->msg);
       sfree (w);
     }
 }
@@ -117,7 +111,7 @@ extern void warnClause_free (warnClause w)
 warnClause_dump (warnClause wc)
 {
   cstring st = cstring_undefined;
-
+  llassert (warnClause_isDefined (wc));
   llassert (!cstring_containsChar (warnClause_getMessage (wc), '#'));
 
   if (warnClause_hasMessage (wc))
@@ -138,7 +132,6 @@ warnClause_undump (char **s)
 {
   flagSpec flag;
   cstring msg;
-  exprNode emsg;
 
   DPRINTF (("Undump: %s", *s));
   flag = flagSpec_undump (s);
@@ -158,7 +151,5 @@ warnClause_undump (char **s)
   DPRINTF (("Here: %s", *s));
   reader_checkChar (s, '#');
 
-  emsg = exprNode_rawStringLiteral (msg, fileloc_copy (g_currentloc));
-  
-  return warnClause_createAux (fileloc_copy (g_currentloc), flag, emsg);
+  return warnClause_createAux (fileloc_copy (g_currentloc), flag, msg);
 }

diff --git a/test/metastate.expect b/test/metastate.expect
index 16b1ad7ebc119af1bfaf367cf8f17f9eda0797dd..a7fa45de7233abaaff24143e22669b17157b2c02 100644 (file)
--- a/test/metastate.expect
+++ b/test/metastate.expect
@@ -2,6 +2,7 @@
 file1.c: (in function main)
 file1.c:10:14: Invalid transfer from implicitly unopen fle to open (unopen file
                   passed as open): fle
+   file1.c:6:14: Meta state fle becomes implicitly unopen
 file1.c:19:16: Invalid transfer from implicitly open fle to unopen (open file
                   passed as unopen): fle
    file1.c:12:3: Meta state fle becomes implicitly open
@@ -36,6 +37,7 @@ Finished LCLint checking --- 2 code errors found, as expected
 file4.c: (in function main)
 file4.c:15:14: Invalid transfer from implicitly unopen fle to open (unopen file
                   passed as open): fle
+   file4.c:11:14: Meta state fle becomes implicitly unopen
 
 Finished LCLint checking --- 1 code error found, as expected
 
@@ -50,6 +52,7 @@ file5.c:16:10: Result state fle does not satisfy ensures clause:
 file5.c: (in function main)
 file5.c:25:14: Invalid transfer from implicitly unopen fle to open (unopen file
                   passed as open): fle
+   file5.c:21:14: Meta state fle becomes implicitly unopen
 file5.c:35:18: Invalid transfer from unopen fle to open (unopen file passed as
                   open): fle
    file5.c:34:3: Meta state fle becomes unopen
@@ -67,11 +70,11 @@ file6.c:30:12: Return loses reference fle in invalid state implicitly open
 
 Finished LCLint checking --- 2 code errors found, as expected
 
-filebad.c:1:23: Meta state anntation open used in inconsistent context:
+filebad.c:1:23: Meta state annotation open used in inconsistent context:
                    int badOpen(FILE *)
-filebad.c:3:52: Meta state anntation closed used in inconsistent context:
+filebad.c:3:52: Meta state annotation closed used in inconsistent context:
                    int p_x
-filebad.c:3:12: Meta state anntation open used on inappropriate reference p_x
+filebad.c:3:12: Meta state annotation open used on inappropriate reference p_x
                    in ensures open clause of badEnsures: ensures open p_x
 
 Finished LCLint checking --- 3 code errors found, as expected

diff --git a/test/mystrncat.out b/test/mystrncat.out
index 490d7e30a81bab20f748e682d853fa8dd04bbe97..11818893db58db4608e16ea569fda4e43226bcf5 100644 (file)
--- a/test/mystrncat.out
+++ b/test/mystrncat.out
@@ -4,14 +4,6 @@ mystrncat.c:12:13: Passed storage buffer not completely defined (*buffer is
                       undefined): mystrncat (buffer, ...)
 mystrncat.c:13:13: Passed storage b not completely defined (*b is undefined):
                       mystrncat (b, ...)
-mystrncat.c:13:3: Possible out-of-bounds store.  Unable to resolve constraint:
-    requires: : maxRead ((malloc(256) @ mystrncat.c:10:7 ) )  <=  ( 0 ) 
-     needed to satisfy precondition:
-    requires: : maxSet ((b @ mystrncat.c:13:13 ) )  >=  (maxRead ((b @
-    mystrncat.c:13:13 ) )) + (( 255 ) )
-     derived from mystrncat precondition: requires: :
-    maxSet ((<parameter 1> ) )  >=  (maxRead ((<parameter 1> ) )) +
-    ((<parameter 3> ) )
 mystrncat.c:12:3: Possible out-of-bounds store.  Unable to resolve constraint:
     requires: : maxRead ((buffer @ mystrncat.c:12:13 ) )  <=  ( 0 ) 
      needed to satisfy precondition:
@@ -20,5 +12,13 @@ mystrncat.c:12:3: Possible out-of-bounds store.  Unable to resolve constraint:
      derived from mystrncat precondition: requires: :
     maxSet ((<parameter 1> ) )  >=  (maxRead ((<parameter 1> ) )) +
     ((<parameter 3> ) )
+mystrncat.c:13:3: Possible out-of-bounds store.  Unable to resolve constraint:
+    requires: : maxRead ((malloc(256) @ mystrncat.c:10:7 ) )  <=  ( 0 ) 
+     needed to satisfy precondition:
+    requires: : maxSet ((b @ mystrncat.c:13:13 ) )  >=  (maxRead ((b @
+    mystrncat.c:13:13 ) )) + (( 255 ) )
+     derived from mystrncat precondition: requires: :
+    maxSet ((<parameter 1> ) )  >=  (maxRead ((<parameter 1> ) )) +
+    ((<parameter 3> ) )
 
 Finished LCLint checking --- 4 code errors found, as expected

diff --git a/test/tainted.expect b/test/tainted.expect
index 3e4cd0e6365861df8161375eab15fa2bf77a614c..f823c5dd17a5a203889d7d85a7addcd00d000f5c 100644 (file)
--- a/test/tainted.expect
+++ b/test/tainted.expect
@@ -83,3 +83,13 @@ taintedimplicit.c:17:18: Invalid transfer from tainted [result of taintme] to
    taintedimplicit.c:17:18: Meta state becomes tainted
 
 Finished LCLint checking --- 1 code error found, as expected
+
+sprintf.c: (in function sp)
+sprintf.c:11:18: Invalid transfer from tainted s to untainted (Possibly tainted
+                    storage used as untainted.): s
+   sprintf.c:10:37: Meta state s becomes tainted
+sprintf.c:14:18: Invalid transfer from tainted s to untainted (Possibly tainted
+                    storage used as untainted.): s
+   sprintf.c:13:61: Meta state s becomes tainted
+
+Finished LCLint checking --- 2 code errors found, as expected