Added check of user specified post conditions.

Added the flag +checkpost ot turn this on and off.

diff --git a/src/Headers/local_constants.h b/src/Headers/local_constants.h
index a6f582af761d0ffa2998cd7bd4bb22ace4c68fc1..de2e753d565b5dd04b32ab07e7e55603e4151838 100644 (file)
--- 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 92a1e16bdfac18d0a7fadfae906c033f0492540f..a39808fa8b7c152d04cd54a7e94a2a966d2c6097 100644 (file)
--- 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 fa1dbd854667baa5f8729bc0175aff684fda4c44..1ce9f550a908ade2265fe9097b02c240e35ecb89 100644 (file)
--- 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 a48b909ff5a40ef6d6205e791fd69a764007239d..5fb36e0d3f62bb566d92bb5399a80ae183f1d1fd 100644 (file)
--- 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 bc448d5a69a66264e79e216e629624e61754b7fe..541d6bd64200422addf530a0aed45fdf149dc3a1 100644 (file)
--- 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",