]> andersk Git - splint.git/blobdiff - src/exprChecks.c
Passes the standard LCLint test suite. YAAAAAAYYYY!!!!!
[splint.git] / src / exprChecks.c
index ee0def2fed975dcf489e6cd8ed69e3164ee265ab..b638d6fac3584a235864d07690f9d9f5af1a72dd 100644 (file)
@@ -890,11 +890,57 @@ void exprNode_checkFunctionBody (exprNode body)
        }
     }
 }
-      
+
 void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
 {
-  exprNode_free (body);
-  }
+  constraintList c, t;
+  /* drl added 8-8-2000 */
+
+  //return;
+  
+  exprNode_generateConstraints (body);
+  
+  c =   uentry_getFcnPreconditions (ue);
+  DPRINTF(("function constraints\n"));
+  DPRINTF (("\n\n\n\n\n\n\n"));
+
+  context_enterInnerContext ();
+  
+   if (c)
+     {
+       llassert (c);
+       DPRINTF ( (message ("Function preconditions are %s \n\n\n\n\n", constraintList_printDetailed (c) ) ) );
+       
+       t = reflectChanges (body->requiresConstraints, constraintList_copy (c) );
+       body->requiresConstraints = constraintList_copy (t);
+       
+       DPRINTF ( (message ("The body has the required cosntraints: %s", constraintList_printDetailed (t) ) ) );
+   t = constraintList_mergeEnsures (c, body->ensuresConstraints);
+
+   body->ensuresConstraints = constraintList_copy (t);
+   
+   DPRINTF ( (message ("The body has the ensures constraints: %s", constraintList_printDetailed (t) ) ) );
+     }
+
+   if (c)
+     {
+       DPRINTF((message ("The Function %s has the preconditions %s", uentry_unparse(ue), constraintList_printDetailed(c) ) ) );
+     }
+   else
+     {
+       DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue) ) ) );
+     }
+
+   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);
+  
+     //  printf ("The required constraints are:\n%s", constraintList_printDetailed(body->requiresConstraints) );
+     //   printf ("The ensures constraints are:\n%s", constraintList_printDetailed(body->ensuresConstraints) );
+   
+   context_exitInnerPlain();
+   /* exprNode_free (body); */
+}
 
 void exprChecks_checkEmptyMacroBody (void)
 {
This page took 0.033407 seconds and 4 git commands to generate.