From 90bc41f719ecb2f59b070c94357de65cbcd52d16 Mon Sep 17 00:00:00 2001 From: drl7x Date: Fri, 4 May 2001 06:35:16 +0000 Subject: [PATCH] Added support for or constraints. --- src/Headers/constraint.h | 1 + src/Headers/constraintExpr.h | 5 +- src/Headers/constraintOutput.h | 4 + src/Headers/constraintResolve.h | 1 + src/Headers/flag_codes.gen | 404 ------------------------------ src/Headers/herald.h | 2 +- src/Headers/herald.last | 2 +- src/constraint.c | 58 +++++ src/constraintGeneration.c | 13 +- src/constraintList.c | 7 +- src/constraintResolve.c | 358 +++++++++++++++++++++----- src/constraintTerm.c | 16 +- src/context.c | 4 +- src/exprChecks.c | 13 +- src/exprDataQuite.i | 2 +- src/flags.def | 9 + src/llerror.c | 2 + test/db1.out | 4 +- test/help.out | 2 + test/maxset/maxsetannotations.c | 2 +- test/maxset/maxsetnoannotations.c | 2 +- 21 files changed, 418 insertions(+), 493 deletions(-) create mode 100644 src/Headers/constraintOutput.h delete mode 100644 src/Headers/flag_codes.gen diff --git a/src/Headers/constraint.h b/src/Headers/constraint.h index 58b8de6..396b30e 100644 --- a/src/Headers/constraint.h +++ b/src/Headers/constraint.h @@ -13,6 +13,7 @@ arithType; struct _constraint { constraint orig; + constraint or; constraintExpr lexpr; arithType ar; constraintExpr expr; diff --git a/src/Headers/constraintExpr.h b/src/Headers/constraintExpr.h index 6e84f9b..631d042 100644 --- a/src/Headers/constraintExpr.h +++ b/src/Headers/constraintExpr.h @@ -11,6 +11,7 @@ typedef union constraintTermValue_ typedef enum { + ERRORBADCONSTRAINTTERMTYPE, EXPRNODE, SREF, INTLITERAL } constraintTermType; @@ -42,7 +43,7 @@ typedef enum { binaryexpr, unaryExpr, - term, + term } constraintExprKind; @@ -174,4 +175,6 @@ constraintExpr constraintExpr_propagateConstants (constraintExpr expr, /*@out@*/ bool * propagate, /*@out@*/ int *literal); +constraintExpr constraintExpr_makeSRefMaxRead(sRef s); + #endif diff --git a/src/Headers/constraintOutput.h b/src/Headers/constraintOutput.h new file mode 100644 index 0000000..96ccfcf --- /dev/null +++ b/src/Headers/constraintOutput.h @@ -0,0 +1,4 @@ +void ConPrint (char * string, fileloc loc) /*@*/; + +void BPRINTF (char * string) /*@*/; + diff --git a/src/Headers/constraintResolve.h b/src/Headers/constraintResolve.h index 6dce56d..4add8da 100644 --- a/src/Headers/constraintResolve.h +++ b/src/Headers/constraintResolve.h @@ -17,3 +17,4 @@ extern constraintList constraintList_mergeEnsures (constraintList list1, constra bool constraint_isAlwaysTrue (constraint c); constraintList constraintList_mergeRequires (constraintList list1, constraintList list2); +constraintList reflectChangesOr (constraintList pre2, constraintList post1); diff --git a/src/Headers/flag_codes.gen b/src/Headers/flag_codes.gen deleted file mode 100644 index f9db498..0000000 --- a/src/Headers/flag_codes.gen +++ /dev/null @@ -1,404 +0,0 @@ - FLG_LIKELYBOOL, - FLG_IMPABSTRACT, - FLG_ACCESSALL, - FLG_ACCESSMODULE, - FLG_ACCESSFILE, - FLG_ACCESSCZECH, - FLG_ACCESSSLOVAK, - FLG_ACCESSCZECHOSLOVAK, - FLG_ABSTRACT, - FLG_MUTREP, - FLG_GLOBALIAS, - FLG_CHECKSTRICTGLOBALIAS, - FLG_CHECKEDGLOBALIAS, - FLG_CHECKMODGLOBALIAS, - FLG_UNCHECKEDGLOBALIAS, - FLG_ALIASUNIQUE, - FLG_MAYALIASUNIQUE, - FLG_MUSTNOTALIAS, - FLG_RETALIAS, - FLG_NOPARAMS, - FLG_OLDSTYLE, - FLG_GNUEXTENSIONS, - FLG_USEVARARGS, - FLG_WARNPOSIX, - FLG_EXITARG, - FLG_EVALORDER, - FLG_EVALORDERUNCON, - FLG_BOOLFALSE, - FLG_BOOLTYPE, - FLG_BOOLTRUE, - FLG_NOACCESS, - FLG_NOCOMMENTS, - FLG_UNRECOGCOMMENTS, - FLG_CONTINUECOMMENT, - FLG_NESTCOMMENT, - FLG_TMPCOMMENTS, - FLG_LINTCOMMENTS, - FLG_WARNLINTCOMMENTS, - FLG_DECLUNDEF, - FLG_SPECUNDEF, - FLG_SPECUNDECL, - FLG_LOOPEXEC, - FLG_CONTROL, - FLG_INFLOOPS, - FLG_INFLOOPSUNCON, - FLG_DEEPBREAK, - FLG_LOOPLOOPBREAK, - FLG_SWITCHLOOPBREAK, - FLG_LOOPSWITCHBREAK, - FLG_SWITCHSWITCHBREAK, - FLG_LOOPLOOPCONTINUE, - FLG_UNREACHABLE, - FLG_WHILEEMPTY, - FLG_WHILEBLOCK, - FLG_FOREMPTY, - FLG_FORBLOCK, - FLG_IFEMPTY, - FLG_IFBLOCK, - FLG_ALLEMPTY, - FLG_ALLBLOCK, - FLG_ELSEIFCOMPLETE, - FLG_NORETURN, - FLG_CASEBREAK, - FLG_MISSCASE, - FLG_FIRSTCASE, - FLG_GRAMMAR, - FLG_NOPP, - FLG_SHADOW, - FLG_INCONDEFSLIB, - FLG_WARNOVERLOAD, - FLG_NESTEDEXTERN, - FLG_REDECL, - FLG_REDEF, - FLG_INCONDEFS, - FLG_IMPTYPE, - FLG_MATCHFIELDS, - FLG_USEDEF, - FLG_IMPOUTS, - FLG_TMPDIR, - FLG_LARCHPATH, - FLG_LCLIMPORTDIR, - FLG_SYSTEMDIRS, - FLG_SKIPANSIHEADERS, - FLG_SKIPPOSIXHEADERS, - FLG_SYSTEMDIRERRORS, - FLG_SYSTEMDIREXPAND, - FLG_INCLUDEPATH, - FLG_SPECPATH, - FLG_QUIET, - FLG_USESTDERR, - FLG_SHOWSUMMARY, - FLG_SHOWSCAN, - FLG_STATS, - FLG_TIMEDIST, - FLG_SHOWUSES, - FLG_NOEFFECT, - FLG_NOEFFECTUNCON, - FLG_EXPORTANY, - FLG_EXPORTFCN, - FLG_EXPORTMACRO, - FLG_EXPORTTYPE, - FLG_EXPORTVAR, - FLG_EXPORTCONST, - FLG_EXPORTITER, - FLG_REPEXPOSE, - FLG_RETEXPOSE, - FLG_ASSIGNEXPOSE, - FLG_CASTEXPOSE, - FLG_LINELEN, - FLG_SHOWCOL, - FLG_PARENFILEFORMAT, - FLG_SHOWFUNC, - FLG_SHOWALLCONJS, - FLG_IMPCONJ, - FLG_EXPECT, - FLG_LCLEXPECT, - FLG_PARTIAL, - FLG_GLOBALS, - FLG_USEALLGLOBS, - FLG_INTERNALGLOBS, - FLG_INTERNALGLOBSNOGLOBS, - FLG_WARNMISSINGGLOBALS, - FLG_WARNMISSINGGLOBALSNOGLOBS, - FLG_GLOBUNSPEC, - FLG_ALLGLOBALS, - FLG_CHECKSTRICTGLOBALS, - FLG_IMPCHECKEDSPECGLOBALS, - FLG_IMPCHECKMODSPECGLOBALS, - FLG_IMPCHECKEDSTRICTSPECGLOBALS, - FLG_IMPCHECKEDGLOBALS, - FLG_IMPCHECKMODGLOBALS, - FLG_IMPCHECKEDSTRICTGLOBALS, - FLG_IMPCHECKEDSTATICS, - FLG_IMPCHECKMODSTATICS, - FLG_IMPCHECKMODINTERNALS, - FLG_IMPCHECKEDSTRICTSTATICS, - FLG_MODGLOBS, - FLG_MODGLOBSUNSPEC, - FLG_MODSTRICTGLOBSUNSPEC, - FLG_MODGLOBSUNCHECKED, - FLG_KEEP, - FLG_DOLH, - FLG_DOLCS, - FLG_SINGLEINCLUDE, - FLG_NEVERINCLUDE, - FLG_SKIPSYSHEADERS, - FLG_WARNFLAGS, - FLG_WARNUNIXLIB, - FLG_BADFLAG, - FLG_FORCEHINTS, - FLG_HELP, - FLG_HINTS, - FLG_RETVAL, - FLG_RETVALOTHER, - FLG_RETVALBOOL, - FLG_RETVALINT, - FLG_OPTF, - FLG_INIT, - FLG_NOF, - FLG_NEEDSPEC, - FLG_NEWDECL, - FLG_ITER, - FLG_HASYIELD, - FLG_DUMP, - FLG_MERGE, - FLG_NOLIB, - FLG_ANSILIB, - FLG_STRICTLIB, - FLG_UNIXLIB, - FLG_UNIXSTRICTLIB, - FLG_POSIXLIB, - FLG_POSIXSTRICTLIB, - FLG_WHICHLIB, - FLG_COMMENTCHAR, - FLG_ALLMACROS, - FLG_LIBMACROS, - FLG_SPECMACROS, - FLG_FCNMACROS, - FLG_CONSTMACROS, - FLG_MACROMATCHNAME, - FLG_MACRONEXTLINE, - FLG_MACROSTMT, - FLG_MACROEMPTY, - FLG_MACROPARAMS, - FLG_MACROASSIGN, - FLG_SEFPARAMS, - FLG_SEFUNSPEC, - FLG_MACROPARENS, - FLG_MACRODECL, - FLG_MACROFCNDECL, - FLG_MACROCONSTDECL, - FLG_MACROREDEF, - FLG_MACROUNDEF, - FLG_RETSTACK, - FLG_USERELEASED, - FLG_STRICTUSERELEASED, - FLG_COMPDEF, - FLG_COMPMEMPASS, - FLG_MUSTDEFINE, - FLG_UNIONDEF, - FLG_MEMIMPLICIT, - FLG_PARAMIMPTEMP, - FLG_ALLIMPONLY, - FLG_CODEIMPONLY, - FLG_SPECALLIMPONLY, - FLG_GLOBIMPONLY, - FLG_RETIMPONLY, - FLG_STRUCTIMPONLY, - FLG_SPECGLOBIMPONLY, - FLG_SPECRETIMPONLY, - FLG_SPECSTRUCTIMPONLY, - FLG_DEPARRAYS, - FLG_COMPDESTROY, - FLG_STRICTDESTROY, - FLG_MUSTFREE, - FLG_BRANCHSTATE, - FLG_STRICTBRANCHSTATE, - FLG_MEMCHECKS, - FLG_MEMTRANS, - FLG_EXPOSETRANS, - FLG_OBSERVERTRANS, - FLG_DEPENDENTTRANS, - FLG_NEWREFTRANS, - FLG_ONLYTRANS, - FLG_ONLYUNQGLOBALTRANS, - FLG_OWNEDTRANS, - FLG_FRESHTRANS, - FLG_SHAREDTRANS, - FLG_TEMPTRANS, - FLG_KEPTTRANS, - FLG_KEEPTRANS, - FLG_IMMEDIATETRANS, - FLG_REFCOUNTTRANS, - FLG_STATICTRANS, - FLG_UNKNOWNTRANS, - FLG_STATICINITTRANS, - FLG_UNKNOWNINITTRANS, - FLG_READONLYSTRINGS, - FLG_READONLYTRANS, - FLG_PASSUNKNOWN, - FLG_MODIFIES, - FLG_MUSTMOD, - FLG_MODOBSERVER, - FLG_MODOBSERVERUNCON, - FLG_MODINTERNALSTRICT, - FLG_MODFILESYSTEM, - FLG_MODUNSPEC, - FLG_MODNOMODS, - FLG_MODUNCON, - FLG_MODUNCONNOMODS, - FLG_GLOBALSIMPMODIFIESNOTHING, - FLG_MODIFIESIMPNOGLOBALS, - FLG_NAMECHECKS, - FLG_CZECH, - FLG_CZECHFUNCTIONS, - FLG_CZECHVARS, - FLG_CZECHMACROS, - FLG_CZECHCONSTANTS, - FLG_CZECHTYPES, - FLG_SLOVAK, - FLG_SLOVAKFUNCTIONS, - FLG_SLOVAKMACROS, - FLG_SLOVAKVARS, - FLG_SLOVAKCONSTANTS, - FLG_SLOVAKTYPES, - FLG_CZECHOSLOVAK, - FLG_CZECHOSLOVAKFUNCTIONS, - FLG_CZECHOSLOVAKMACROS, - FLG_CZECHOSLOVAKVARS, - FLG_CZECHOSLOVAKCONSTANTS, - FLG_CZECHOSLOVAKTYPES, - FLG_ANSIRESERVED, - FLG_CPPNAMES, - FLG_ANSIRESERVEDLOCAL, - FLG_DISTINCTEXTERNALNAMES, - FLG_EXTERNALNAMELEN, - FLG_EXTERNALNAMECASEINSENSITIVE, - FLG_DISTINCTINTERNALNAMES, - FLG_INTERNALNAMELEN, - FLG_INTERNALNAMECASEINSENSITIVE, - FLG_INTERNALNAMELOOKALIKE, - FLG_MACROVARPREFIX, - FLG_MACROVARPREFIXEXCLUDE, - FLG_TAGPREFIX, - FLG_TAGPREFIXEXCLUDE, - FLG_ENUMPREFIX, - FLG_ENUMPREFIXEXCLUDE, - FLG_FILESTATICPREFIX, - FLG_FILESTATICPREFIXEXCLUDE, - FLG_GLOBPREFIX, - FLG_GLOBPREFIXEXCLUDE, - FLG_TYPEPREFIX, - FLG_TYPEPREFIXEXCLUDE, - FLG_EXTERNALPREFIX, - FLG_EXTERNALPREFIXEXCLUDE, - FLG_LOCALPREFIX, - FLG_LOCALPREFIXEXCLUDE, - FLG_UNCHECKEDMACROPREFIX, - FLG_UNCHECKEDMACROPREFIXEXCLUDE, - FLG_CONSTPREFIX, - FLG_CONSTPREFIXEXCLUDE, - FLG_ITERPREFIX, - FLG_ITERPREFIXEXCLUDE, - FLG_DECLPARAMPREFIX, - FLG_DECLPARAMNAME, - FLG_DECLPARAMMATCH, - FLG_DECLPARAMPREFIXEXCLUDE, - FLG_CONTROLNESTDEPTH, - FLG_STRINGLITERALLEN, - FLG_NUMSTRUCTFIELDS, - FLG_NUMENUMMEMBERS, - FLG_INCLUDENEST, - FLG_ANSILIMITS, - FLG_NAME, - FLG_SPECIAL, - FLG_NULL, - FLG_NULLTERMINATED, - FLG_BUFFEROVERFLOW, - FLG_ARRAYREAD, - FLG_ARRAYWRITE, - FLG_FUNCTIONPOST, - FLG_FUNCTIONCONSTRAINT, - FLG_CONSTRAINTLOCATION, - FLG_IMPLICTCONSTRAINT, - FLG_NULLTERMINATEDWARNING, - FLG_NULLDEREF, - FLG_FCNDEREF, - FLG_NULLPASS, - FLG_NULLRET, - FLG_NULLSTATE, - FLG_NULLASSIGN, - FLG_BOOLCOMPARE, - FLG_REALCOMPARE, - FLG_POINTERARITH, - FLG_NULLPOINTERARITH, - FLG_PTRNUMCOMPARE, - FLG_STRICTOPS, - FLG_BITWISEOPS, - FLG_SHIFTSIGNED, - FLG_BOOLOPS, - FLG_PTRNEGATE, - FLG_SIZEOFTYPE, - FLG_SIZEOFFORMALARRAY, - FLG_FIXEDFORMALARRAY, - FLG_INCOMPLETETYPE, - FLG_FORMALARRAY, - FLG_PREDASSIGN, - FLG_PREDBOOL, - FLG_PREDBOOLINT, - FLG_PREDBOOLOTHERS, - FLG_PREDBOOLPTR, - FLG_DEFINE, - FLG_UNDEFINE, - FLG_GLOBSTATE, - FLG_SUPCOUNTS, - FLG_LIMIT, - FLG_SYNTAX, - FLG_TRYTORECOVER, - FLG_PREPROC, - FLG_TYPE, - FLG_FULLINITBLOCK, - FLG_ENUMMEMBERS, - FLG_MAINTYPE, - FLG_FORMATTYPE, - FLG_FORMATCODE, - FLG_FORWARDDECL, - FLG_ABSTVOIDP, - FLG_CASTFCNPTR, - FLG_CHARINDEX, - FLG_ENUMINDEX, - FLG_BOOLINT, - FLG_CHARINT, - FLG_ENUMINT, - FLG_FLOATDOUBLE, - FLG_IGNOREQUALS, - FLG_DUPLICATEQUALS, - FLG_IGNORESIGNS, - FLG_NUMLITERAL, - FLG_CHARINTLITERAL, - FLG_RELAXQUALS, - FLG_RELAXTYPES, - FLG_CHARUNSIGNEDCHAR, - FLG_MATCHANYINTEGRAL, - FLG_LONGUNSIGNEDINTEGRAL, - FLG_LONGINTEGRAL, - FLG_LONGUNSIGNEDUNSIGNEDINTEGRAL, - FLG_LONGSIGNEDINTEGRAL, - FLG_ZEROPTR, - FLG_ZEROBOOL, - FLG_REPEATUNRECOG, - FLG_SYSTEMUNRECOG, - FLG_UNRECOG, - FLG_TOPUNUSED, - FLG_EXPORTLOCAL, - FLG_EXPORTHEADER, - FLG_EXPORTHEADERVAR, - FLG_FIELDUNUSED, - FLG_ENUMMEMUNUSED, - FLG_CONSTUNUSED, - FLG_FUNCUNUSED, - FLG_PARAMUNUSED, - FLG_TYPEUNUSED, - FLG_VARUNUSED, - FLG_UNUSEDSPECIAL, diff --git a/src/Headers/herald.h b/src/Headers/herald.h index 1326d5c..e65ef86 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 2.5q" /*@constant observer char *LCL_COMPILE;@*/ -# define LCL_COMPILE "Compiled using gcc28 -DSTDC_HEADERS=1 -g -Wall on FreeBSD shankly.cs.virginia.edu 3.2-RELEASE FreeBSD 3.2-RELEASE #0: Tue May 18 04:05:08 GMT 1999 jkh@cathair:/usr/src/sys/compile/GENERIC i386 by drl7x" +# define LCL_COMPILE "Compiled using gcc28 -DSTDC_HEADERS=1 -Wall -g -pedantic on FreeBSD shankly.cs.virginia.edu 3.2-RELEASE FreeBSD 3.2-RELEASE #0: Tue May 18 04:05:08 GMT 1999 jkh@cathair:/usr/src/sys/compile/GENERIC i386 by drl7x" diff --git a/src/Headers/herald.last b/src/Headers/herald.last index 117a593..e65ef86 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 2.5q" /*@constant observer char *LCL_COMPILE;@*/ -# define LCL_COMPILE "Compiled using gcc -DSTDC_HEADERS=1 -g -Wall on FreeBSD shankly.cs.virginia.edu 3.2-RELEASE FreeBSD 3.2-RELEASE #0: Tue May 18 04:05:08 GMT 1999 jkh@cathair:/usr/src/sys/compile/GENERIC i386 by drl7x" +# define LCL_COMPILE "Compiled using gcc28 -DSTDC_HEADERS=1 -Wall -g -pedantic on FreeBSD shankly.cs.virginia.edu 3.2-RELEASE FreeBSD 3.2-RELEASE #0: Tue May 18 04:05:08 GMT 1999 jkh@cathair:/usr/src/sys/compile/GENERIC i386 by drl7x" diff --git a/src/constraint.c b/src/constraint.c index 2226654..f313f7f 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -94,6 +94,20 @@ constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconsta return ret; } +constraint constraint_same (constraint c1, constraint c2) +{ + + if (c1->ar != c2->ar) + return FALSE; + + if (!constraintExpr_similar (c1->lexpr, c2->lexpr) ) + return FALSE; + + if (!constraintExpr_similar (c1->expr, c2->expr) ) + return FALSE; + + return TRUE; +} constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r) { @@ -119,6 +133,11 @@ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r ret->expr = constraintExpr_copy (r); ret->post = TRUE; + + ret->orig = constraint_copy(ret); + + ret = constraint_simplify (ret); + // ret->orig = ret; DPRINTF(("GENERATED CONSTRAINT:")); DPRINTF( (message ("%s", constraint_print(ret) ) ) ); @@ -128,6 +147,9 @@ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r constraint constraint_copy (constraint c) { constraint ret; + + llassert (c); + ret = constraint_makeNew(); ret->lexpr = constraintExpr_copy (c->lexpr); ret->ar = c->ar; @@ -140,6 +162,12 @@ constraint constraint_copy (constraint c) ret->orig = constraint_copy (c->orig); else ret->orig = NULL; + + if (c->or != NULL) + ret->or = constraint_copy (c->or); + else + ret->or = NULL; + return ret; } @@ -156,6 +184,12 @@ void constraint_overWrite (constraint c1, constraint c2) c1->orig = constraint_copy (c2->orig); else c1->orig = NULL; + + if (c2->or != NULL) + c1->or = constraint_copy (c2->or); + else + c1->or = NULL; + c1->generatingExpr = exprNode_fakeCopy (c2->generatingExpr ); } @@ -175,6 +209,7 @@ bool constraint_resolve (/*@unused@*/ constraint c) ret->ar = LT; ret->post = FALSE; ret->orig = NULL; + ret->or = NULL; ret->generatingExpr = NULL; return ret; } @@ -610,6 +645,29 @@ cstring constraint_print (constraint c) /*@*/ return st; } +cstring constraint_printOr (constraint c) /*@*/ +{ + cstring ret; + constraint temp; + + ret = cstring_undefined; + temp = c; + + ret = cstring_concat (ret, constraint_print(temp) ); + + temp = temp->or; + + while (temp) + { + ret = cstring_concat (ret, cstring_makeLiteral (" OR ") ); + ret = cstring_concat (ret, constraint_print(temp) ); + temp = temp->or; + } + + return ret; + +} + /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition, exprNodeList arglist) { diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c index 2e460e4..83348e8 100644 --- a/src/constraintGeneration.c +++ b/src/constraintGeneration.c @@ -328,11 +328,14 @@ exprNode doIf (exprNode e, exprNode test, exprNode body) #warning bad e->ensuresConstraints = constraintList_copy (test->ensuresConstraints); - /* - if (!exprNode_mayEscape (body) ) - e->ensuresConstraints = constraintList_mergeEnsures (e->ensuresConstraints, + + if (exprNode_mayEscape (body) ) + { + DPRINTF (( message("doIf: the if statement body %s returns or exits", exprNode_unparse(body) ) )); + e->ensuresConstraints = constraintList_mergeEnsures (e->ensuresConstraints, test->falseEnsuresConstraints); - */ + } + DPRINTF ((message ("doIf: if requiers %s ", constraintList_print(e->requiresConstraints) ) ) ); return e; @@ -493,7 +496,7 @@ exprNode doSwitch (/*@returned@*/ exprNode e) data = e->edata; llassert(FALSE); - //TPRINTF (( message ("doSwitch for: switch (%s) %s", + //DPRINTF (( message ("doSwitch for: switch (%s) %s", // exprNode_unparse (exprData_getPairA (data)), // exprNode_unparse (exprData_getPairB (data))) )); diff --git a/src/constraintList.c b/src/constraintList.c index 26dbaa3..49b07bf 100644 --- a/src/constraintList.c +++ b/src/constraintList.c @@ -69,6 +69,7 @@ constraintList_grow (constraintList s) constraintList constraintList_add (constraintList s, constraint el) { + el = constraint_simplify (el); if (resolve (el, s) ) return s; @@ -114,7 +115,11 @@ constraintList_print (constraintList s) /*@*/ if (current != NULL) { - cstring temp1 = constraint_print(current); + cstring temp1; + if ( context_getFlag (FLG_ORCONSTRAINT) ) + temp1 = constraint_printOr(current); + else + temp1 = constraint_print(current); type = message ("%q %q\n", type, temp1 ); } diff --git a/src/constraintResolve.c b/src/constraintResolve.c index ee1e63a..4b7ba08 100644 --- a/src/constraintResolve.c +++ b/src/constraintResolve.c @@ -21,6 +21,9 @@ +constraintList reflectChangesOr (constraintList pre2, constraintList post1); + +constraint inequalitySubstituteUnsound (constraint c, constraintList p); constraintList reflectChanges (constraintList pre2, constraintList post1); constraint substitute (constraint c, constraintList p); @@ -47,14 +50,27 @@ constraintList constraintList_mergeEnsures (constraintList list1, constraintList constraintList temp; //ret = constraintList_new(); + + llassert(list1); + llassert(list2); + + DPRINTF(( message ("constraintList_mergeEnsures: list1 %s list2 %s", + constraintList_print(list1), constraintList_print(list2) + ))); - ret = reflectChangesEnsures (list1, list2); - ret = constraintList_fixConflicts (ret, list2); + ret = constraintList_fixConflicts (list1, list2); + ret = reflectChangesEnsures (ret, list2); ret = constraintList_subsumeEnsures (ret, list2); list2 = constraintList_subsumeEnsures (list2, ret); temp = constraintList_copy(list2); temp = constraintList_addList (temp, ret); + + DPRINTF(( message ("constraintList_mergeEnsures: returning %s ", + constraintList_print(temp) ) + )); + + return temp; //ret = constraintList_addList (ret, list2); //return ret; @@ -82,25 +98,6 @@ constraintList constraintList_mergeRequires (constraintList list1, constraintLis return ret; } - -/* constraintList constraintList_resolveRequires (constraintList requires, constraintList ensures) */ -/* { */ - -/* constraintList ret; */ -/* constraintList temp; */ -/* ret = constraintList_new(); */ - -/* ret = reflectChangesEnsures (list1, list2); */ -/* ret = constraintList_fixConflicts (ret, list2); */ -/* ret = constraintList_subsumeEnsures (ret, list2); */ -/* list2 = constraintList_subsumeEnsures (list2, ret); */ -/* temp = constraintList_copy(list2); */ - -/* temp = constraintList_addList (temp, ret); */ -/* return temp; */ -/* //ret = constraintList_addList (ret, list2); */ -/* //return ret; */ -/* } */ void checkArgumentList (exprNode temp, exprNodeList arglist, fileloc sequencePoint) { @@ -216,9 +213,12 @@ void mergeResolve (exprNode parent, exprNode child1, exprNode child2) parent->ensuresConstraints = constraintList_new(); parent->requiresConstraints = constraintList_copy (child1->requiresConstraints); - - temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints); + if ( context_getFlag (FLG_ORCONSTRAINT) ) + temp = reflectChangesOr (child2->requiresConstraints, child1->ensuresConstraints); + else + temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints); + parent->requiresConstraints = constraintList_mergeRequires (parent->requiresConstraints, temp); parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints, @@ -255,7 +255,8 @@ constraintList constraintList_subsumeEnsures (constraintList list1, constraintLi return ret; } -/* tries to resolve constraints in list pr2 using post1 */ + +/* tries to resolve constraints in list pre2 using post1 */ constraintList reflectChanges (constraintList pre2, constraintList post1) { @@ -277,9 +278,14 @@ constraintList reflectChanges (constraintList pre2, constraintList post1) // the inequality substitution may cause us to lose information //so we don't want to store the result but we do it anyway temp2 = constraint_copy (temp); - temp2 = inequalitySubstitute (temp, post1); - if (!resolve (temp2, post1) ) - ret = constraintList_add (ret, temp2); + // if (context_getFlag (FLG_ORCONSTRAINT) ) + temp2 = inequalitySubstitute (temp, post1); + if (!resolve (temp2, post1) ) + { + temp2 = inequalitySubstituteUnsound (temp2, post1); + if (!resolve (temp2, post1) ) + ret = constraintList_add (ret, temp2); + } } } } end_constraintList_elements; @@ -289,6 +295,136 @@ constraintList reflectChanges (constraintList pre2, constraintList post1) } +constraint constraint_addOr (constraint orig, constraint or) +{ + constraint c; + c = orig; + + DPRINTF((message("constraint_addor: oring %s onto %s", constraint_printOr(or), constraint_printOr(orig) ) )); + + while (c->or != NULL) + { + c = c->or; + } + c->or = constraint_copy(or); + + DPRINTF((message("constraint_addor: returning %s",constraint_printOr(orig) ) )); + + return orig; +} + + +bool resolveOr (constraint c, constraintList list) +{ + constraint temp; + + DPRINTF(( message("resolveOr: constraint %s and list %s", constraint_printOr(c), constraintList_print(list) ) )); + temp = c; + + do + { + if (resolve (temp, list) ) + return TRUE; + temp = temp->or; + } + while (temp); + + return FALSE; +} + + +constraint doResolve (constraint c, constraintList post1, bool * resolved) +{ + constraint temp; + + if (!resolveOr (c, post1) ) + { + temp = substitute (c, post1); + if (!resolveOr (temp, post1) ) + { + // try inequality substitution + constraint temp2; + + // the inequality substitution may cause us to lose information + //so we don't want to store the result but we do it anyway + temp2 = constraint_copy (c); + // if (context_getFlag (FLG_ORCONSTRAINT) ) + temp2 = inequalitySubstitute (temp2, post1); + if (!resolveOr (temp2, post1) ) + { + temp2 = inequalitySubstituteUnsound (temp2, post1); + if (!resolveOr (temp2, post1) ) + { + if (!constraint_same (temp, temp2) ) + temp = constraint_addOr (temp, temp2); + *resolved = FALSE; + return temp; + } + } + } + } + + *resolved = TRUE; + return NULL; + + + +} + +constraint doResolveOr (constraint c, constraintList post1, bool * resolved) +{ + constraint ret; + constraint next; + constraint curr; + + *resolved = FALSE; + ret = constraint_copy(c); + next = ret->or; + ret->or = NULL; + + ret = doResolve (ret, post1, resolved); + while (next) + { + curr = next; + next = curr->or; + curr->or = NULL; + + curr = doResolve (curr, post1, resolved); + if (*resolved) + return NULL; + + ret = constraint_addOr (ret, curr); + } + + return ret; +} + + + + + +/* tries to resolve constraints in list pr2 using post1 */ +constraintList reflectChangesOr (constraintList pre2, constraintList post1) +{ + bool resolved; + constraintList ret; + constraint temp; + ret = constraintList_new(); + DPRINTF((message ("reflectChangesOr: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) ))); + + constraintList_elements (pre2, el) + { + temp = doResolveOr (el, post1, &resolved); + + if (!resolved) + { + ret = constraintList_add(ret, temp); + } + } end_constraintList_elements; + + DPRINTF((message ("reflectChangesOr: returning %s", constraintList_print(ret) ) ) ); + return ret; +} constraintList reflectChangesEnsures (constraintList pre2, constraintList post1) { @@ -349,8 +485,8 @@ void constraint_fixConflict (constraint good, constraint conflicting) bool conflict (constraint c, constraintList list) { - - constraintList_elements (list, el) + + constraintList_elements (list, el) { if ( constraint_conflict(el, c) ) { @@ -360,16 +496,16 @@ bool conflict (constraint c, constraintList list) } end_constraintList_elements; return FALSE; - } //check if constraint in list1 and conflict with constraints in List2. If so we -//remove form list1 and (optionally) change list2. -constraintList constraintList_fixConflicts (constraintList list1, constraintList list2) +//remove form list1 and change list2. +constraintList constraintList_fixConflicts (/*@returned@*/constraintList list1, constraintList list2) { constraintList ret; ret = constraintList_new(); + llassert(list1); constraintList_elements (list1, el) { if (! conflict (el, list2) ) @@ -400,7 +536,7 @@ bool resolve (constraint c, constraintList p) } -/*returns true if cosntraint post satifies cosntriant pre */ +/*returns true if constraint post satifies cosntriant pre */ bool satifies (constraint pre, constraint post) { if (constraint_isAlwaysTrue (pre) ) @@ -447,6 +583,8 @@ bool arithType_canResolve (arithType ar1, arithType ar2) return FALSE; } +/* We look for constraint which are tautologies */ + bool constraint_isAlwaysTrue (constraint c) { constraintExpr l, r; @@ -455,6 +593,8 @@ bool constraint_isAlwaysTrue (constraint c) l = c->lexpr; r = c->expr; + + DPRINTF(( message("constraint_IsAlwaysTrue:examining %s", constraint_print(c) ) )); if (constraintExpr_canGetValue(l) && constraintExpr_canGetValue(r) ) { @@ -497,43 +637,40 @@ bool constraint_isAlwaysTrue (constraint c) } } + return FALSE; l = constraintExpr_copy (c->lexpr); r = constraintExpr_copy (c->expr); // l = constraintExpr_propagateConstants (l, &lHasConstant, &lConstant); r = constraintExpr_propagateConstants (r, &rHasConstant, &rConstant); - if (constraintExpr_similar (l,r) ) + if (constraintExpr_similar (l,r) && (rHasConstant ) ) { DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants %s and %s are similar", constraintExpr_unparse(l), constraintExpr_unparse(r) ) )); - if (rHasConstant) + DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is %d", rConstant ) )); + switch (c->ar) { - DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is %d", rConstant ) )); - switch (c->ar) - { - case EQ: - return (rConstant == 0); - case LT: - return (rConstant > 0); - case LTE: - return (rConstant >= 0); - case GTE: - return (rConstant <= 0); - case GT: - return (rConstant < 0); - - default: - BADEXIT; - break; - } + case EQ: + return (rConstant == 0); + case LT: + return (rConstant > 0); + case LTE: + return (rConstant >= 0); + case GTE: + return (rConstant <= 0); + case GT: + return (rConstant < 0); + + default: + BADEXIT; + break; } - } - else - { - DPRINTF(( message("Constraint %s is not always true", constraint_print(c) ) )); - return FALSE; - } + else + { + DPRINTF(( message("Constraint %s is not always true", constraint_print(c) ) )); + return FALSE; + } BADEXIT; } @@ -555,6 +692,19 @@ bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintE if (! (constraintExpr_canGetValue (expr1) && constraintExpr_canGetValue (expr2) ) ) { + constraintExpr e1, e2; + bool p1, p2; + int const1, const2; + + e1 = constraintExpr_propagateConstants (expr1, &p1, &const1); + + e2 = constraintExpr_propagateConstants (expr2, &p2, &const2); + + if (p1 && p2) + if (const1 <= const2) + if (constraintExpr_similar (e1, e2) ) + return TRUE; + DPRINTF( ("Can't Get value")); return FALSE; } @@ -575,6 +725,19 @@ bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintE if (! (constraintExpr_canGetValue (expr1) && constraintExpr_canGetValue (expr2) ) ) { + constraintExpr e1, e2; + bool p1, p2; + int const1, const2; + + e1 = constraintExpr_propagateConstants (expr1, &p1, &const1); + + e2 = constraintExpr_propagateConstants (expr2, &p2, &const2); + + if (p1 && p2) + if (const1 >= const2) + if (constraintExpr_similar (e1, e2) ) + return TRUE; + DPRINTF( ("Can't Get value")); return FALSE; } @@ -644,6 +807,12 @@ constraint constraint_adjust (constraint substitute, constraint old) } +/* If function preforms substitutes based on inequality + + It uses the rule x >= y && b < y ===> x >= b + 1 + + Warning this is sound but throws out information + */ constraint inequalitySubstitute (constraint c, constraintList p) { if (c->ar != GTE) @@ -655,18 +824,21 @@ constraint inequalitySubstitute (constraint c, constraintList p) // if (!constraint_conflict (c, el) ) { constraint temp; + constraintExpr temp2; + temp = constraint_copy(el); // temp = constraint_adjust(temp, c); - if (constraintExpr_same (el->lexpr, c->expr) ) + if (constraintExpr_same (el->expr, c->expr) ) { - DPRINTF((message ("Replacing %s in %s with %s", + DPRINTF((message ("inequalitySubstitute Replacing %s in %s with %s", constraintExpr_print (c->expr), constraint_print (c), constraintExpr_print (el->expr) ) )); - c->expr = constraintExpr_copy (el->expr); + temp2 = constraintExpr_copy (el->lexpr); + c->expr = constraintExpr_makeIncConstraintExpr (temp2); } } @@ -677,32 +849,80 @@ constraint inequalitySubstitute (constraint c, constraintList p) return c; } +/* This function performs substitutions based on the rule: + for a constraint of the form expr1 >= expr2; a < b => + a = b -1 for all a in expr1. This will work in most cases. + + Like inequalitySubstitute we're throwing away some information +*/ + +constraint inequalitySubstituteUnsound (constraint c, constraintList p) +{ + DPRINTF (( message ("Doing inequalitySubstituteUnsound " ) )); + + if (c->ar != GTE) + return c; + + constraintList_elements (p, el) + { + DPRINTF (( message ("inequalitySubstituteUnsound examining substituting %s on %s", constraint_print(el), constraint_print(c) ) )); + if ( ( el->ar == LTE) || (el->ar == LT) ) + // if (!constraint_conflict (c, el) ) + { + constraint temp; + constraintExpr temp2; + + temp = constraint_copy(el); + + // temp = constraint_adjust(temp, c); + temp2 = constraintExpr_copy (el->expr); + + if (el->ar == LT) + temp2 = constraintExpr_makeDecConstraintExpr (temp2); + + DPRINTF((message ("Replacing %s in %s with %s", + constraintExpr_print (el->lexpr), + constraintExpr_print (c->lexpr), + constraintExpr_print (temp2) ) )); + + c->lexpr = constraintExpr_searchandreplace (c->lexpr, el->lexpr, temp2); + } + } + end_constraintList_elements; + + c = constraint_simplify(c); + return c; +} + constraint substitute (constraint c, constraintList p) { + constraint ret; + + ret = constraint_copy(c); constraintList_elements (p, el) { if ( el->ar == EQ) - if (!constraint_conflict (c, el) ) + if (!constraint_conflict (ret, el) ) { constraint temp; temp = constraint_copy(el); - temp = constraint_adjust(temp, c); + temp = constraint_adjust(temp, ret); DPRINTF((message ("Substituting %s in the constraint %s", - constraint_print (temp), constraint_print (c) + constraint_print (temp), constraint_print (ret) ) ) ); - c = constraint_searchandreplace (c, temp->lexpr, temp->expr); - DPRINTF(( message ("The new constraint is %s", constraint_print (c) ) )); + ret = constraint_searchandreplace (ret, temp->lexpr, temp->expr); + DPRINTF(( message ("The new constraint is %s", constraint_print (ret) ) )); } } end_constraintList_elements; - c = constraint_simplify(c); - return c; + ret = constraint_simplify(ret); + return ret; } diff --git a/src/constraintTerm.c b/src/constraintTerm.c index abadf41..adac901 100644 --- a/src/constraintTerm.c +++ b/src/constraintTerm.c @@ -377,7 +377,21 @@ bool constraintTerm_similar (constraintTerm term1, constraintTerm term2) sRef s1, s2; llassert (term1 !=NULL && term2 !=NULL); - + + if ( (term1->kind == INTLITERAL) && (term2->kind == INTLITERAL) ) + { + int t1, t2; + llassert (constraintTerm_canGetValue(term1) ); + t1 = constraintTerm_getValue (term1); + + llassert (constraintTerm_canGetValue(term2) ); + t2 = constraintTerm_getValue (term2); + if (t1 == t2) + return TRUE; + + return FALSE; + } + s1 = constraintTerm_getsRef (term1); s2 = constraintTerm_getsRef (term2); diff --git a/src/context.c b/src/context.c index 02fe35b..a3e4159 100644 --- a/src/context.c +++ b/src/context.c @@ -161,7 +161,7 @@ static void context_exitClauseSimp (void) /*@modifies gc@*/ ; static void context_exitClausePlain (void) /*@modifies gc@*/ ; static void context_setJustPopped (void) /*@modifies gc.justpopped@*/ ; static void context_setValue (flagcode p_flag, int p_val) /*@modifies gc.flags@*/ ; -static void context_setFlag (flagcode p_f, bool p_b) +/*drl fix static */ void context_setFlag (flagcode p_f, bool p_b) /*@modifies gc.flags@*/ ; static void @@ -3366,7 +3366,7 @@ context_restoreFlag (flagcode f) } -static void +/*drl7x fix this static */ void context_setFlag (flagcode f, bool b) { context_setFlagAux (f, b, FALSE, FALSE); diff --git a/src/exprChecks.c b/src/exprChecks.c index 4b90d09..6f9fbf0 100644 --- a/src/exprChecks.c +++ b/src/exprChecks.c @@ -903,7 +903,8 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) constraintList c2, fix; // return; - + + // context_setFlag(FLG_ORCONSTRAINT, TRUE); exprNode_generateConstraints (body); c = uentry_getFcnPreconditions (ue); @@ -923,8 +924,14 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body) c2 = constraintList_copy (c); fix = constraintList_makeFixedArrayConstraints (body->uses); c2 = reflectChanges (c2, constraintList_copy(fix) ); - - t = reflectChanges (body->requiresConstraints, constraintList_copy (c2) ); + if ( context_getFlag (FLG_ORCONSTRAINT) ) + { + t = reflectChangesOr (body->requiresConstraints, constraintList_copy (c2) ); + } + else + { + t = reflectChanges (body->requiresConstraints, constraintList_copy (c2) ); + } body->requiresConstraints = constraintList_copy (t); DPRINTF ( (message ("The body has the required constraints: %s", constraintList_printDetailed (t) ) ) ); diff --git a/src/exprDataQuite.i b/src/exprDataQuite.i index affecfd..262cdd1 100644 --- a/src/exprDataQuite.i +++ b/src/exprDataQuite.i @@ -10,7 +10,7 @@ restricts access to exprData static void fakeQuite1 (int x) { -void *f; +void** f; x = 1; diff --git a/src/flags.def b/src/flags.def index dc211c4..bc448d5 100644 --- a/src/flags.def +++ b/src/flags.def @@ -2823,6 +2823,15 @@ NULL, NULL, ", ", 0, 0 }, + /*drl7x added 4/29/01 */ +{ + FK_NT, FK_MEMORY, modeFlag, + "orconstraint", + FLG_ORCONSTRAINT, + "Use limited OR expressions to resolve constraints", + ", ", + 0, 0 +}, { FK_NT, FK_MEMORY, modeFlag, diff --git a/src/llerror.c b/src/llerror.c index 6807d83..9b984d4 100644 --- a/src/llerror.c +++ b/src/llerror.c @@ -1,3 +1,4 @@ +#include /*drl take this out*/ /* ** LCLint - annotation-assisted static program checker ** Copyright (C) 1994-2000 University of Virginia, @@ -1200,6 +1201,7 @@ void llbugaux (cstring file, int line, /*@only@*/ cstring s) (void) fflush (stderr); inbug = FALSE; + assert(FALSE); /*drl take this out*/ } # ifndef NOLCL diff --git a/test/db1.out b/test/db1.out index e4ba09d..f1cb5c9 100644 --- a/test/db1.out +++ b/test/db1.out @@ -667,7 +667,7 @@ modnomods 4 0 moduncon 20 0 modunconnomods 1 0 ansireserved 9 0 -fcnpost 0 65 +fcnpost 0 67 fcnconstraint 0 14 nullret 1 0 nullstate 1 0 @@ -684,6 +684,6 @@ paramuse 1 0 typeuse 1 0 varuse 4 0 ======== ========= -Total 331 132 +Total 331 134 Finished LCLint checking --- 331 code errors found, as expected diff --git a/test/help.out b/test/help.out index b40443c..6e9fb9e 100644 --- a/test/help.out +++ b/test/help.out @@ -328,6 +328,7 @@ Finished LCLint checking --- no code processed oldstyle onlytrans onlyunqglobaltrans + orconstraint overload ownedtrans paramimptemp @@ -902,6 +903,7 @@ fcnpost --- Function has the post condition fcnconstraint --- unresolved constraint constraintlocation --- display full c expression for every constraint generated implictconstraint --- Try to generate implicit constraints for functions +orconstraint --- Use limited OR expressions to resolve constraints nullterminated --- misuse of nullterminated allocation nullderef --- possible dereferencce of null pointer fcnderef --- dereferencce of a function type diff --git a/test/maxset/maxsetannotations.c b/test/maxset/maxsetannotations.c index 823d7f7..c2bc474 100644 --- a/test/maxset/maxsetannotations.c +++ b/test/maxset/maxsetannotations.c @@ -1,4 +1,4 @@ -#include "/home/drl7x/re/LCLintDev/lib/ansi.h" +#include "../../lib/ansi.h" void anstrcpy( /*@unique@*/ char * a, char *b) /*@bufferConstraint MaxSet(a) >= MaxRead (b); @*/ { strcpy (a,b); diff --git a/test/maxset/maxsetnoannotations.c b/test/maxset/maxsetnoannotations.c index 05bea2c..90c9a84 100644 --- a/test/maxset/maxsetnoannotations.c +++ b/test/maxset/maxsetnoannotations.c @@ -1,4 +1,4 @@ -#include "/home/drl7x/re/LCLintDev/lib/ansi.h" +#include "../../lib/ansi.h" void noancopy(/*@unique@*/ char * a, char *b) { strcpy (a,b); -- 2.45.1