X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/abd7f89523564e5e238e5852585b98f72c3b48f4..312c981596ce6202de7686f2d4c46aec1bae3939:/src/constraintGeneration.c

diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c
index 6a71ce1..dfb737d 100644
--- a/src/constraintGeneration.c
+++ b/src/constraintGeneration.c
@@ -37,8 +37,10 @@
 # include "exprChecks.h"
 # include "exprNodeSList.h"
 
-/*@access exprNode @*/
-
+/*@access exprNode@*/ /* NO! Don't do this recklessly! */
+/*@-nullderef@*/ /* DRL needs to fix this code! */
+/*@-nullpass@*/ /* DRL needs to fix this code! */
+/*@-temptrans@*/ /* DRL needs to fix this code! */
 
 static /*@truewhennull@*/ bool exprNode_handleError (/*@temp@*/ exprNode p_e);
 
@@ -453,7 +455,7 @@ static exprNode doWhile (/*@returned@*/ exprNode e, /*@dependent@*/ exprNode tes
     {
       if (sRef_isFixedArray(el))
 	{
-	  long int size;
+	  size_t size;
 	  DPRINTF((message("%s is a fixed array",
 			    sRef_unparse(el))));
 	  size = sRef_getArraySize(el);
@@ -548,9 +550,8 @@ static void doFor (/*@dependent@*/ exprNode e, /*@dependent@*/ exprNode forPred,
 
 static /*@dependent@*/ exprNode exprNode_makeDependent(/*@returned@*/  exprNode e)
 {
-  /*@-temptrans@*/
+  /* !!! DRL - this is ridiculous!  Read the manual on memory annotations please! */
   return e;
-  /*@=temptrans@*/  
 }
 
 static void 
@@ -951,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));
@@ -1264,7 +1282,7 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  /*@ob
       t2 = exprData_getOpB (data);
       tok = exprData_getOpTok (data);      
 
-      if (tok.tok == ADD_ASSIGN)
+      if (lltok_getTok (tok) == ADD_ASSIGN)
 	{
 	  exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
 	  exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
@@ -1272,7 +1290,7 @@ void exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  /*@ob
 	  cons = constraint_makeAddAssign (t1, t2,  sequencePoint);
 	  e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 	}
-      else if (tok.tok == SUB_ASSIGN)
+      else if (lltok_getTok (tok) == SUB_ASSIGN)
 	{
 	  exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint);
 	  exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint);
@@ -2223,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))));