From 6970c11be2c0e175abf98c906a87115836e4f55f Mon Sep 17 00:00:00 2001 From: evans Date: Fri, 27 Jul 2001 01:02:13 +0000 Subject: [PATCH] *** empty log message *** --- src/Headers/constraintList.h | 4 +- src/Headers/context.h | 4 +- src/Headers/exprNode.h | 4 + src/Headers/herald.h | 2 +- src/Headers/herald.last | 2 +- src/Headers/local_constants.h | 4 +- src/Headers/local_constants.last | 4 +- src/Headers/metaStateSpecifier.h | 5 + src/Headers/sRef.h | 6 +- src/Headers/stateInfo.h | 1 + src/Headers/uentry.h | 6 +- src/Headers/warnClause.h | 6 +- src/Makefile | 2 +- src/cgrammar.y | 15 ++- src/clabstract.c | 7 +- src/constraintTerm.c | 8 +- src/context.c | 23 ++-- src/cscanner.l | 11 +- src/exprNode.c | 198 +++++++++++++++++++++++-------- src/metaStateSpecifier.c | 41 ++++++- src/mtContextNode.c | 3 +- src/sRef.c | 46 +++---- src/stateClauseList.c | 2 +- src/stateInfo.c | 6 + src/uentry.c | 35 +++--- src/usymtab.c | 17 +-- src/usymtab_interface.c | 9 +- src/warnClause.c | 33 ++---- test/metastate.expect | 9 +- test/mystrncat.out | 16 +-- test/tainted.expect | 10 ++ 31 files changed, 353 insertions(+), 186 deletions(-) diff --git a/src/Headers/constraintList.h b/src/Headers/constraintList.h index fa80b09..c17bf6c 100644 --- 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 29e4cf7..1f64901 100644 --- 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 e9b8cda..226cabb 100644 --- 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 f929ab5..ab93b80 100644 --- 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 f929ab5..ab93b80 100644 --- 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 73e13fc..c4c3a88 100644 --- 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 73e13fc..c4c3a88 100644 --- 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 8815ee2..855179b 100644 --- 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 87d5bfb..dc1c316 100644 --- 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 a446b4b..a5d0fcb 100644 --- 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 bf3a534..db199e3 100644 --- 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 375f9dd..4f41bb0 100644 --- 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 c39ab81..cb7a79b 100644 --- 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 4faaf30..9817a79 100644 --- 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 dd02ed2..f1bb637 100644 --- 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 709d77c..bbba3b7 100644 --- 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 ac81cc7..a4963c2 100644 --- 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 db64bb0..3cc9e38 100644 --- 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 4b48356..4091c41 100644 --- 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 28525d8..51e68a7 100644 --- 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 9f89c87..22a2926 100644 --- 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 e637ba5..fcdf105 100644 --- 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 a703837..0afa765 100644 --- 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 d0b9a2f..06542e5 100644 --- 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 e4646e8..0c79b93 100644 --- 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 73c45f2..bb2c40c 100644 --- 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 87e414d..7bc8add 100644 --- 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 e9fbc86..059ec9a 100644 --- 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 16b1ad7..a7fa45d 100644 --- 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 490d7e3..1181889 100644 --- 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 (( ) ) >= (maxRead (( ) )) + - (( ) ) 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 (( ) ) >= (maxRead (( ) )) + (( ) ) +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 (( ) ) >= (maxRead (( ) )) + + (( ) ) Finished LCLint checking --- 4 code errors found, as expected diff --git a/test/tainted.expect b/test/tainted.expect index 3e4cd0e..f823c5d 100644 --- 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 -- 2.45.2