EXtensive code clean up. Almost passes LCLint.

[splint.git] / src / exprChecks.c

diff --git a/src/exprChecks.c b/src/exprChecks.c
index 7ed778c9a24306eadd2624051844995421156d10..72be47c0fa520eebd45d6d003ffe6fdf9cb0315d 100644 (file)
--- a/src/exprChecks.c
+++ b/src/exprChecks.c
@@ -883,6 +883,9 @@ void exprNode_checkFunctionBody (exprNode body)
                }
            }
        }
+
+      /* drl added call*/
+      exprNode_checkFunction (context_getHeader (), body);
       
       if (!checkret)
        {
@@ -890,12 +893,18 @@ void exprNode_checkFunctionBody (exprNode body)
        }
     }
 }
+/*drl modified */
+
+extern constraintList implicitFcnConstraints;
 
 void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
 {
   constraintList c, t;
-  /* drl added 8-8-2000 */
+ constraintList c2, fix;
+
+ //  return;
 
+ //  context_setFlag(FLG_ORCONSTRAINT, TRUE);
   exprNode_generateConstraints (body);
   
   c =   uentry_getFcnPreconditions (ue);
@@ -906,14 +915,27 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
   
    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);
+
+       c2  =  constraintList_copy (c);
+       fix =  constraintList_makeFixedArrayConstraints (body->uses);
+       c2  =  reflectChanges (c2, constraintList_copy(fix) );
+       if ( context_getFlag (FLG_ORCONSTRAINT) )
+        {
+          t = reflectChangesOr (body->requiresConstraints, constraintList_copy (c2) );
+        }
+       else
+        {
+          t = reflectChanges (body->requiresConstraints, constraintList_copy (c2) );
+        }
+       body->requiresConstraints = constraintList_copy (t);
        
-       DPRINTF ( (message ("The body has the required cosntraints: %s", constraintList_printDetailed (t) ) ) );
-   t = constraintList_mergeEnsures (c, body->ensuresConstraints);
+       DPRINTF ( (message ("The body has the required constraints: %s", constraintList_printDetailed (t) ) ) );
+       t = constraintList_mergeEnsures (c, body->ensuresConstraints);
 
    body->ensuresConstraints = constraintList_copy (t);
    
@@ -922,15 +944,30 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
 
    if (c)
      {
-       TPRINTF((message ("The Function %s has the preconditions %s", uentry_unparse(ue), constraintList_printDetailed(c) ) ) );
+       DPRINTF((message ("The Function %s has the preconditions %s", uentry_unparse(ue), constraintList_printDetailed(c) ) ) );
      }
    else
      {
-       TPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue) ) ) );
+       DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue) ) ) );
      }
 
-   printf ("The required constraints are:\n%s", constraintList_printDetailed(body->requiresConstraints) );
-   printf ("The ensures constraints are:\n%s", constraintList_printDetailed(body->ensuresConstraints) );
+   if ( implicitFcnConstraints)
+     {
+          if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
+             {
+               body->requiresConstraints = reflectChanges (body->requiresConstraints, constraintList_copy (implicitFcnConstraints) );
+             }
+     }
+   
+   constraintList_printError(body->requiresConstraints, g_currentloc);
+   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);
+  
+     //  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); */