Fixed bug in handling of sizeof

[splint.git] / src / constraintGeneration.c

diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c
index c08063d3ce058c39864a8ee5c57167983410d798..dfb737ddbb3f29464cf8bb5651efd7ec0c29ebad 100644 (file)
--- a/src/constraintGeneration.c
+++ b/src/constraintGeneration.c
@@ -952,14 +952,31 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e)
       p->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(p);
       constraintList_free(temp);
 
+
+
+      DPRINTF((message("p->trueEnsuresConstraints before substitue %s", constraintList_print(p->trueEnsuresConstraints)  )
+              ));
+
+            /*drl 10/10/2002 this is a bit of a hack but the reason why we do this is so that any function post conditions or similar things get applied correctly to each branch.  e.g. in strlen(s) < 5 we want the trueEnsures to be maxRead(s) < 5*/
+
+      p->trueEnsuresConstraints = constraintList_substituteFreeTarget (p->trueEnsuresConstraints,
+                                                                      p->ensuresConstraints);
+      
+      DPRINTF(( message ("p->trueEnsuresConstraints after substitue %s", constraintList_print(p->trueEnsuresConstraints) )
+               ));
+      
       temp = p->falseEnsuresConstraints;
       p->falseEnsuresConstraints =  exprNode_traversFalseEnsuresConstraints(p);
       constraintList_free(temp);
 
+      /*See comment on trueEnsures*/
+      p->falseEnsuresConstraints = constraintList_substituteFreeTarget (p->falseEnsuresConstraints,
+                                                                      p->ensuresConstraints);
+      
       e = doIfElse (e, p, trueBranch, falseBranch);
       DPRINTF(("Done IFELSE"));
       break;
- 
+      
     case XPR_DOWHILE:
 
       e2 = (exprData_getPairB (data));
@@ -2224,6 +2241,44 @@ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
       if (constraintList_isUndefined(preconditions))
        preconditions = constraintList_makeNew();
     }
+  
+  // drl remember to remove this code before you make a pslint release.
+  /*
+  if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
+    {
+      
+      uentryList_elements (params, el)
+       {
+         DPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) ));
+         
+         s = uentry_getSref(el);
+         if (sRef_isReference (s) )
+           {
+             DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
+           }
+         else
+           {
+             DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
+           }
+         //drl 4/26/01
+         //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0 
+         c = constraint_makeSRefWriteSafeInt (s, 0);
+         
+         implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
+         
+         //drl 10/23/2002 added support for out
+         if (!uentry_isOut(el) )
+           {
+             c = constraint_makeSRefReadSafeInt (s, 0);
+             
+             implicitFcnConstraints = constraintList_add(implicitFcnConstraints , c);
+           }
+         
+         
+       }
+      
+    }
+  */
   DPRINTF ((message("Done checkCall\n")));
   DPRINTF ((message("Returning list %q ", constraintList_printDetailed(preconditions))));