Added check of user specified post conditions.

[splint.git] / src / exprChecks.c

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