Made allocations involving sizeof work correctly (test/malloc.c).

[splint.git] / src / exprChecks.c

diff --git a/src/exprChecks.c b/src/exprChecks.c
index 54fce3ce319f3cca8f9eb7fe0e4bda20e8b795ed..219387b99885217982adfa0e8a15c18611474f43 100644 (file)
--- a/src/exprChecks.c
+++ b/src/exprChecks.c
@@ -1,6 +1,6 @@
 /*
 ** Splint - annotation-assisted static program checker
-** Copyright (C) 1994-2002 University of Virginia,
+** Copyright (C) 1994-2003 University of Virginia,
 **         Massachusetts Institute of Technology
 **
 ** This program is free software; you can redistribute it and/or modify it
@@ -270,7 +270,7 @@ checkRefGlobParam (sRef base, /*@notnull@*/ exprNode e,
                {
                  uentry arg = uentryList_getN (params, paramno);
                  sRef ref = uentry_getSref (arg);
-
+                 
                  if (uentry_isReturned (arg) 
                      || sRef_isOnly (ref) 
                      || sRef_isExposed (ref)
@@ -942,11 +942,12 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
 {
   constraintList c, t, post;
   constraintList c2, fix;
-  constraintList implicitFcnConstraints;
   context_enterInnerContext ();
 
   llassert (exprNode_isDefined (body));
 
+  DPRINTF (("Checking body: %s", exprNode_unparse (body)));
+
   /*
     if we're not going to be printing any errors for buffer overflows
     we can skip the checking to improve performance
@@ -955,39 +956,35 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
     in order to find potential problems like assert failures and seg faults...
   */
 
-  if (!context_getFlag(FLG_DEBUGFUNCTIONCONSTRAINT))
-    {
-      /* check if errors will printed */
-      if (!(context_getFlag(FLG_DEBUGFUNCTIONCONSTRAINT) ||
-           context_getFlag(FLG_BOUNDSWRITE) ||
-           context_getFlag(FLG_BOUNDSREAD)  ||
-           context_getFlag(FLG_LIKELYBOUNDSWRITE) ||
-           context_getFlag(FLG_LIKELYBOUNDSREAD)  ||
-           context_getFlag(FLG_CHECKPOST) ))
-       {
-         exprNode_free (body);
-         context_exitInnerPlain();
-         
-         return;
-       }
-    }
+  if (!(context_getFlag (FLG_DEBUGFUNCTIONCONSTRAINT) 
+       || context_getFlag (FLG_BOUNDSWRITE) 
+       || context_getFlag (FLG_BOUNDSREAD)  
+       || context_getFlag (FLG_LIKELYBOUNDSWRITE) 
+       || context_getFlag (FLG_LIKELYBOUNDSREAD)  
+       || context_getFlag (FLG_CHECKPOST)
+       || context_getFlag (FLG_ALLOCMISMATCH)))
+  {
+    exprNode_free (body);
+    context_exitInnerPlain();    
+    return;
+  }
   
   exprNode_generateConstraints (body); /* evans 2002-03-02: this should not be declared to take a
                                          dependent... fix it! */
   
-  c =   uentry_getFcnPreconditions (ue);
-  DPRINTF(("function constraints\n"));
-  DPRINTF (("\n\n\n\n\n\n\n"));
+  c = uentry_getFcnPreconditions (ue);
   
-  if (constraintList_isDefined(c) )
+  if (constraintList_isDefined (c))
     {
-      DPRINTF ((message ("Function preconditions are %s \n\n\n\n\n", constraintList_printDetailed (c) ) ) );
+      DPRINTF (("Function preconditions are %s", constraintList_unparseDetailed (c)));
       
-      body->requiresConstraints = constraintList_reflectChangesFreePre (body->requiresConstraints, c);
+      body->requiresConstraints = 
+       constraintList_reflectChangesFreePre (body->requiresConstraints, c);
       
       c2  =  constraintList_copy (c);
       fix =  constraintList_makeFixedArrayConstraints (body->uses);
       c2  =  constraintList_reflectChangesFreePre (c2, fix);
+
       constraintList_free (fix);
       
       if (context_getFlag (FLG_ORCONSTRAINT))
@@ -1000,7 +997,7 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
        }
       
       constraintList_free (body->requiresConstraints);
-      DPRINTF ((message ("The body has the required constraints: %s", constraintList_printDetailed (t) ) ) );
+      DPRINTF ((message ("The body has the required constraints: %s", constraintList_unparseDetailed (t) ) ) );
       
       body->requiresConstraints = t;
       
@@ -1008,29 +1005,36 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
       constraintList_free(body->ensuresConstraints);
       
       body->ensuresConstraints = t;
-      
-      DPRINTF ((message ("The body has the ensures constraints: %s", constraintList_printDetailed (t) ) ) );
+     
+      DPRINTF ((message ("The body has the ensures constraints: %s", constraintList_unparseDetailed (t) ) ) );
       constraintList_free(c2);
     }
   
   if (constraintList_isDefined(c))
     {
       DPRINTF ((message ("The Function %s has the preconditions %s", 
-                        uentry_unparse(ue), constraintList_printDetailed(c))));
+                        uentry_unparse(ue), constraintList_unparseDetailed(c))));
     }
   else
     {
       DPRINTF((message ("The Function %s has no preconditions", uentry_unparse(ue))));
     }
   
-  implicitFcnConstraints = getImplicitFcnConstraints();
-  
-  if (constraintList_isDefined(implicitFcnConstraints) )
+  if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS))
     {
-      if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
+      constraintList implicitFcnConstraints = context_getImplicitFcnConstraints (ue);
+      
+      if (constraintList_isDefined (implicitFcnConstraints))
        {
+         DPRINTF (("Implicit constraints: %s", constraintList_unparse (implicitFcnConstraints)));
+         
          body->requiresConstraints = constraintList_reflectChangesFreePre (body->requiresConstraints, 
-                                                                           implicitFcnConstraints );
+                                                                           implicitFcnConstraints);
+         constraintList_free (implicitFcnConstraints);
+       }
+      else
+       {
+         DPRINTF (("No implicit constraints"));
        }
     }
   
@@ -1047,7 +1051,7 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
          constraintList post2;
          
          DPRINTF ((message ("The declared function postconditions are %s \n\n\n\n\n", 
-                            constraintList_printDetailed (post) ) ) );
+                            constraintList_unparseDetailed (post) ) ) );
          
          post = constraintList_reflectChangesFreePre (post, body->ensuresConstraints);
          
@@ -1090,17 +1094,18 @@ void exprNode_checkFunction (/*@unused@*/ uentry ue, /*@only@*/ exprNode body)
        ConPrint (message ("Splint 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) );
+       printf ("The ensures constraints are:\n%s", constraintList_unparseDetailed(body->ensuresConstraints) );
    */
    
-   if (constraintList_isDefined(c) )
+   if (constraintList_isDefined (c))
      constraintList_free(c);
 
    context_exitInnerPlain();
-
-   /*is it okay not to free this?*/
-  exprNode_free (body);
-  }
+   
+   /* is it okay not to free this? */
+   DPRINTF (("Done checking constraints..."));
+   exprNode_free (body);
+}
 
 void exprChecks_checkEmptyMacroBody (void)
 {