X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/dcaf75eaed37623f27c23241c146ad25910208f3..8f29980557a7d8dc71b0d2696e28960a240efcf0:/src/exprChecks.c

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);