From 8f29980557a7d8dc71b0d2696e28960a240efcf0 Mon Sep 17 00:00:00 2001 From: dlaroche Date: Mon, 18 Jun 2001 18:35:52 +0000 Subject: [PATCH] Added check of user specified post conditions. Added the flag +checkpost ot turn this on and off. --- src/Headers/local_constants.h | 6 ++-- src/constraint.c | 54 ++++++++++++++++++++++++++++++++++- src/constraintList.c | 16 +++++++++++ src/exprChecks.c | 47 +++++++++++++++++++++++++++++- src/flags.def | 15 ++++++++-- 5 files changed, 131 insertions(+), 7 deletions(-) diff --git a/src/Headers/local_constants.h b/src/Headers/local_constants.h index a6f582a..de2e753 100644 --- a/src/Headers/local_constants.h +++ b/src/Headers/local_constants.h @@ -1,7 +1,7 @@ /* local_constants.h - created automatically by gmake localconstants */ /*@constant observer char *SYSTEM_LIBDIR;@*/ -# define SYSTEM_LIBDIR /usr/include +# define SYSTEM_LIBDIR "/usr/include" /*@constant observer char *DEFAULT_LARCHPATH;@*/ -# define DEFAULT_LARCHPATH /usr/local/lclint-2.5m/lib +# define DEFAULT_LARCHPATH ".:/afs/cert.org/usr/dlaroche/LCLintDev/lib" /*@constant observer char *DEFAULT_LCLIMPORTDIR;@*/ -# define DEFAULT_LCLIMPORTDIR /usr/local/lclint-2.5m/imports +# define DEFAULT_LCLIMPORTDIR "/afs/cert.org/usr/dlaroche/LCLintDev/imports" diff --git a/src/constraint.c b/src/constraint.c index 92a1e16..a39808f 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -637,6 +637,35 @@ cstring arithType_print (arithType ar) /*@*/ return st; } + +void constraint_printErrorPostCondition (constraint c, fileloc loc) +{ + cstring string; + fileloc errorLoc, temp; + + string = constraint_printDetailedPostCondition (c); + + errorLoc = loc; + + loc = NULL; + + temp = constraint_getFileloc(c); + + if (fileloc_isDefined(temp) ) + { + errorLoc = temp; + voptgenerror ( FLG_CHECKPOST, string, errorLoc); + fileloc_free(temp); + } + else + { + voptgenerror ( FLG_CHECKPOST, string, errorLoc); + } +} + + + + void constraint_printError (constraint c, fileloc loc) { cstring string; @@ -709,6 +738,29 @@ cstring constraint_printDeep (constraint c) } +cstring constraint_printDetailedPostCondition (constraint c) +{ + cstring st = cstring_undefined; + + st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) ); + + if (context_getFlag (FLG_CONSTRAINTLOCATION) ) + { + cstring temp; + // llassert (c->generatingExpr); + temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ), + exprNode_unparse(c->generatingExpr) ); + st = cstring_concatFree (st, temp); + + if (constraint_hasMaxSet(c) ) + { + temp = message ("Has MaxSet\n"); + st = cstring_concatFree (st, temp); + } + } + return st; +} + cstring constraint_printDetailed (constraint c) { cstring st = cstring_undefined; @@ -732,7 +784,7 @@ cstring constraint_printDetailed (constraint c) if (constraint_hasMaxSet(c) ) { - temp = message ("\nHas MaxSet\n"); + temp = message ("Has MaxSet\n"); st = cstring_concatFree (st, temp); } } diff --git a/src/constraintList.c b/src/constraintList.c index fa1dbd8..1ce9f55 100644 --- a/src/constraintList.c +++ b/src/constraintList.c @@ -190,6 +190,21 @@ constraintList_print (constraintList s) /*@*/ return st; } +void constraintList_printErrorPostConditions (constraintList s, fileloc loc) +{ + + constraintList_elements (s, elem) + { + if (elem != NULL) + { + constraint_printErrorPostCondition (elem, loc); + } + } + end_constraintList_elements; + return; +} + + void constraintList_printError (constraintList s, fileloc loc) { @@ -204,6 +219,7 @@ void constraintList_printError (constraintList s, fileloc loc) return; } + cstring constraintList_printDetailed (constraintList s) { diff --git a/src/exprChecks.c b/src/exprChecks.c index a48b909..5fb36e0 100644 --- a/src/exprChecks.c +++ b/src/exprChecks.c @@ -899,7 +899,7 @@ extern constraintList implicitFcnConstraints; void exprNode_checkFunction (/*@unused@*/ uentry ue, exprNode body) { - constraintList c, t; + constraintList c, t, post; constraintList c2, fix; // return; @@ -966,8 +966,53 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, exprNode body) } constraintList_printError(body->requiresConstraints, g_currentloc); + + + post = uentry_getFcnPostconditions (ue); + + if ( context_getFlag (FLG_CHECKPOST) ) + { + if (post) + { + + constraintList post2; + + DPRINTF ( (message ("The declared function postconditions are %s \n\n\n\n\n", constraintList_printDetailed (post) ) ) ); + + post = reflectChangesFreePre (post, body->ensuresConstraints); + + post2 = constraintList_copy (post); + fix = constraintList_makeFixedArrayConstraints (body->uses); + post2 = reflectChangesFreePre (post2, fix); + constraintList_free(fix); + if ( context_getFlag (FLG_ORCONSTRAINT) ) + { + t = reflectChangesOr (post2, body->ensuresConstraints); + } + else + { + t = reflectChanges (post2, body->ensuresConstraints); + } + + constraintList_free(post2); + + constraintList_free(post); + post = t; + + + + printf("Unresolved post conditions\n"); + constraintList_printErrorPostConditions(post, g_currentloc); + } + } + + if (post) + constraintList_free(post); + + constraintList_printError(body->ensuresConstraints, g_currentloc); + // ConPrint (message ("Unable to resolve function constraints:\n%s", constraintList_printDetailed(body->requiresConstraints) ), g_currentloc); // ConPrint (message ("LCLint has found function post conditions:\n%s", constraintList_printDetailed(body->ensuresConstraints) ), g_currentloc); diff --git a/src/flags.def b/src/flags.def index bc448d5..541d6bd 100644 --- a/src/flags.def +++ b/src/flags.def @@ -2791,11 +2791,12 @@ NULL, NULL, "Memory is set past the end of an array or or after the allocated buffer, ", 0, 0 }, + { FK_NT, FK_MEMORY, modeFlag, "fcnpost", FLG_FUNCTIONPOST, - "Function has the post condition", + "Function has the post condition_Block Post condition:_This function block has the post condition ", "LCLint has determined that the following statement true after the function, ", 0, 0 }, @@ -2803,10 +2804,20 @@ NULL, NULL, FK_NT, FK_MEMORY, modeFlag, "fcnconstraint", FLG_FUNCTIONCONSTRAINT, - "unresolved constraint", + "unresolved constraint:", "LCLint was unable to resolve a constraint at the top of the function. If code is correct consider using explict annotation assertions, ", 0, 0 }, + /*drl7x added 6/18/01 */ +{ + FK_NT, FK_MEMORY, modeFlag, + "checkpost", + FLG_CHECKPOST, + "unable to verify ensures annotation", + "LCLint was unable to determine that the function satisfies a post condition given in an ensures annotation, ", + 0, 0 +}, + { FK_NT, FK_MEMORY, modeFlag, "constraintlocation", -- 2.45.1