X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/1b8ae6904556859bbe91aadf35b8adcc1a0611ce..2a6e9c30f59a18a1f6e678745a79ae5bda5b6a99:/src/constraintExpr.c

diff --git a/src/constraintExpr.c b/src/constraintExpr.c
index 5dded48..7093b6e 100644
--- a/src/constraintExpr.c
+++ b/src/constraintExpr.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
@@ -17,8 +17,8 @@
 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 ** MA 02111-1307, USA.
 **
-** For information on splint: splint@cs.virginia.edu
-** To report a bug: splint-bug@cs.virginia.edu
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
 ** For more information: http://www.splint.org
 */
 
@@ -36,25 +36,31 @@
 # include "exprChecks.h"
 # include "exprNodeSList.h"
 
-/*@-czechfcns@*/
-
-
-
-/*@access exprNode constraintExpr@*/
 
+static ctype constraintExpr_getOrigType (constraintExpr p_e);
+static bool constraintExpr_hasTypeChange(constraintExpr p_e) /*@*/;
 
 static /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/constraintExpr p_expr, int p_literal);
 
 
+/*@only@*/ static constraintExpr
+doSRefFixInvarConstraintTerm (/*@only@*/ constraintExpr p_e,
+			      sRef p_s, ctype p_ct);
+
 /*@only@*/ static constraintExpr 
 doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr p_e, /*@temp@*/ /*@observer@*/ exprNodeList p_arglist) /*@modifies p_e@*/;
 
 static /*@only@*/ constraintExpr 
 doFixResultTerm (/*@only@*/ constraintExpr p_e, /*@exposed@*/ exprNode p_fcnCall)
      /*@modifies p_e@*/;
-     
-     
-/*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void) 
+
+static   bool  constraintExpr_canGetCType (constraintExpr p_e) /*@*/;
+
+static ctype constraintExpr_getCType (constraintExpr p_e);
+
+static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr p_e, ctype p_ct);
+
+/*@special@*/ /*@notnull@*/ static constraintExpr constraintExpr_makeBinaryOp (void) 
      /* @allocates result->data @ @sets result->kind @ */ ;
 
 void constraintExpr_free (/*@only@*/ constraintExpr expr)
@@ -139,7 +145,7 @@ static bool isZeroBinaryOp (constraintExpr expr)
 
 /* change expr + (o - expr) to (expr -expr) */
 
-/*@only@*/ static constraintExpr removeZero (/*@only@*/ /*@returned@*/ constraintExpr expr)
+/*@only@*/ /*@notnull@*/ static constraintExpr removeZero (/*@only@*/ /*@returned@*/ constraintExpr expr)
 {
   constraintExpr expr1, expr2;
   
@@ -149,10 +155,11 @@ static bool isZeroBinaryOp (constraintExpr expr)
   
   constraintExprBinaryOpKind  tempOp;
 
+  llassert (expr != NULL); /* evans 2001-07-18 */
+
   if (!isZeroBinaryOp(expr) )
     return expr;
 
-  llassert (expr != NULL); /* evans 2001-07-18 */
   
   expr1 = constraintExprData_binaryExprGetExpr1(expr->data);
   expr2 = constraintExprData_binaryExprGetExpr2(expr->data);
@@ -186,7 +193,7 @@ static bool isZeroBinaryOp (constraintExpr expr)
 }
 
 
-/*@only@*/ constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
+/*@only@*//*@notnull@*/  constraintExpr constraintExpr_propagateConstants (/*@only@*/ constraintExpr expr,
 						/*@out@*/ bool * propagate,
 						  /*@out@*/ int *literal)
 {
@@ -286,7 +293,8 @@ static bool isZeroBinaryOp (constraintExpr expr)
 	  
 	  constraintExpr_free(expr1);
 	  constraintExpr_free(expr);
-	  
+
+	  llassert (constraintExpr_isDefined(temp) );
 	  return temp;
 	}
       else
@@ -321,7 +329,7 @@ static bool isZeroBinaryOp (constraintExpr expr)
   return expr;
 }
 
-/*@only@*/ static constraintExpr constraintExpr_combineConstants (/*@only@*/ constraintExpr expr ) /*@modifies expr@*/
+/*@notnull@*/ /*@only@*/ static constraintExpr constraintExpr_combineConstants (/*@only@*/ constraintExpr expr ) /*@modifies expr@*/
 {
   bool propagate;
   int literal;
@@ -341,16 +349,20 @@ static bool isZeroBinaryOp (constraintExpr expr)
 	}
     }
    DPRINTF ((message ("After combine %s", constraintExpr_unparse(expr) ) ) );
-  return expr;
+
+   llassert(constraintExpr_isDefined(expr) );
+   return expr;
 }
 
 /*@special@*/
-static constraintExpr constraintExpr_alloc (void) /*@post:isnull result->data@*/
+static /*@notnull@*/ constraintExpr constraintExpr_alloc (void) /*@post:isnull result->data@*/
 {
   constraintExpr ret;
   ret = dmalloc (sizeof (*ret) );
   ret->kind = term;
   ret->data = NULL;
+  ret->ct = FALSE;
+  ret->origType = ctype_undefined; 
   return ret;
 }
 
@@ -379,10 +391,23 @@ static constraintExpr constraintExpr_alloc (void) /*@post:isnull result->data@*/
 constraintExpr constraintExpr_copy (constraintExpr expr)
 {
   constraintExpr ret;
-  ret = constraintExpr_alloc();
+  ret = constraintExpr_alloc ();
+
+
+  /*drl 03/02/2003 this shouldn't be used to copy a null
+    expression but handle things cleanly if it is*/
+  llassert (!constraintExpr_isUndefined(expr) );
+
+  if (constraintExpr_isUndefined(expr) )
+    {
+      return constraintExpr_undefined;
+    }
+  
   ret->kind = expr->kind;
   
   ret->data = copyExprData (expr->data, expr->kind);
+  ret->ct = expr->ct;
+  ret->origType = expr->origType;
   return ret;
 }
 
@@ -396,9 +421,13 @@ constraintExpr constraintExpr_copy (constraintExpr expr)
   ret->data = dmalloc (sizeof *(ret->data) );
   t = constraintTerm_makeExprNode (e);
   ret->data = constraintExprData_termSetTerm (ret->data, t);
+  ret->ct = FALSE;
+  ret->origType = ctype_undefined;
+
   return ret;
 }
 
+/*@access exprNode@*/
 constraintExpr constraintExpr_makeExprNode (exprNode e)
 {
  sRef s;
@@ -407,7 +436,6 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
  exprNode t, t1, t2;
  lltok tok;
  
- 
  llassert (e != NULL);
  
  data = e->edata;
@@ -416,6 +444,10 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
    {
    case XPR_SIZEOF:
      t = exprData_getSingle (data);
+     while (exprNode_isInParens (t) )
+       {
+	 t = exprData_getUopNode (t->edata);
+       }
      s = exprNode_getSref (t);
      if (sRef_isFixedArray(s) )
       {
@@ -424,6 +456,11 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
 	size = (int) sRef_getArraySize(s);
 	ret = constraintExpr_makeIntLiteral (size);
       }
+     else if (exprNode_isStringLiteral (t))
+      {
+	cstring str = multiVal_forceString (exprNode_getValue(t));
+	ret = constraintExpr_makeIntLiteral (size_toLong (cstring_length (str) + 1));
+      } 
      else
        {
 	 DPRINTF ((message ("could not determine the size of %s", exprNode_unparse (e) ) ) );
@@ -443,7 +480,13 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
 	 ce2 = constraintExpr_makeExprNode (t2);
 	 ret = constraintExpr_parseMakeBinaryOp (ce1, tok, ce2);	 
        }
-     /*
+
+     
+     /*@i333*/
+     /* uncomment this block to activate the cheesy heuristic
+	for handling sizeof expressions
+	
+     / *
        drl 8-11-001
        
        We handle expressions containing sizeof with the rule
@@ -451,7 +494,10 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
 
        This is the total wronge way to do this but...
        it may be better than nothing
-     */
+     * /
+
+     
+      
      else if (lltok_isMult(tok) )
        {
 	 if  ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
@@ -461,12 +507,13 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
 	 else if  ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
 	   {
 	     ret = constraintExpr_makeExprNode(t1);
-	   }
+	     } 
 	 else
 	   {
 	   ret =  oldconstraintExpr_makeTermExprNode (e);
 	   }
        }
+     */
      else
         ret = oldconstraintExpr_makeTermExprNode (e);
    
@@ -479,13 +526,13 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
    case XPR_PREOP:
       t = exprData_getUopNode (data);
       tok =  exprData_getUopTok (data);
-      if (lltok_isInc_Op (tok) )
+      if (lltok_isIncOp (tok))
 	{
 	  constraintExpr temp;
 	  temp = constraintExpr_makeExprNode(t);
 	  ret = constraintExpr_makeIncConstraintExpr(temp);
 	}
-      else if (lltok_isDec_Op (tok) )
+      else if (lltok_isDecOp (tok))
 	{
 	  constraintExpr temp;
 	  temp = constraintExpr_makeExprNode(t);
@@ -515,6 +562,11 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
   return ret;
 }
 
+/*@noaccess exprNode@*/
+
+
+
+
 /*@only@*/ constraintExpr constraintExpr_makeTermExprNode (/*@exposed@*/ exprNode e)
 {
   return  oldconstraintExpr_makeTermExprNode(e);
@@ -529,6 +581,8 @@ static constraintExpr constraintExpr_makeTerm (/*@only@*/  constraintTerm t)
   ret->data = dmalloc (sizeof *(ret->data) );
   ret->data->term = NULL;
   ret->data = constraintExprData_termSetTerm (ret->data, t);
+  ret->ct = FALSE;
+  ret->origType = ctype_undefined; 
 
   return ret;
 }
@@ -542,10 +596,14 @@ constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s)
   ret->data = dmalloc (sizeof *(ret->data) );
   t = constraintTerm_makesRef (s);
   ret->data = constraintExprData_termSetTerm (ret->data, t);
+
+  ret->ct = FALSE;
+  ret->origType = ctype_undefined; 
+
   return ret;
 }
 
-/*@special@*/ static constraintExpr makeUnaryOpGeneric (void) /*@allocates result->data@*/ /*@defines result->kind@*/
+/*@special@*/ /*@notnull@*/ static constraintExpr makeUnaryOpGeneric (void) /*@allocates result->data@*/ /*@defines result->kind@*/
 {
   constraintExpr ret;
   ret = constraintExpr_alloc();
@@ -555,7 +613,7 @@ constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s)
   return ret;
 }
 
-/*@only@*/ static constraintExpr constraintExpr_makeUnaryOpConstraintExpr (/*@only@*/ constraintExpr cexpr)
+/*@notnull@*/ /*@only@*/ static constraintExpr constraintExpr_makeUnaryOpConstraintExpr (/*@only@*/ constraintExpr cexpr)
 {
   constraintExpr ret;
   ret = makeUnaryOpGeneric();
@@ -572,7 +630,7 @@ constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s)
 }
 
 
-/*@only@*/ static constraintExpr constraintExpr_makeUnaryOp (/*@only@*/ constraintExpr cexpr,   constraintExprUnaryOpKind Op )
+/*@only@*/ /*@notnull@*/static constraintExpr constraintExpr_makeUnaryOp (/*@only@*/ constraintExpr cexpr,   constraintExprUnaryOpKind Op )
 {
   constraintExpr ret;
   ret = makeUnaryOpGeneric();
@@ -580,18 +638,13 @@ constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s)
   ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
   ret->data = constraintExprData_unaryExprSetOp (ret->data, Op);
 
-  return ret;
-}
+  ret->ct = FALSE;
+  ret->origType = ctype_undefined; 
 
-/*@only@*/
-static constraintExpr constraintExpr_makeMaxSetConstraintExpr (/*@only@*/ constraintExpr c)
-{
-  constraintExpr ret;
-  ret = constraintExpr_makeUnaryOp (c, MAXSET);
   return ret;
 }
 
-/*@only@*/
+/*@only@*/ /*@notnull@*/
 static constraintExpr constraintExpr_makeUnaryOpExprNode (/*@exposed@*/ exprNode expr)
 {
   constraintExpr ret;
@@ -602,9 +655,16 @@ static constraintExpr constraintExpr_makeUnaryOpExprNode (/*@exposed@*/ exprNode
   return ret;
 }
 
+/*@only@*/ /*@notnull@*/
+static constraintExpr constraintExpr_makeMaxSetConstraintExpr (/*@only@*/ constraintExpr c)
+{
+  constraintExpr ret;
+  ret = constraintExpr_makeUnaryOp (c, MAXSET);
+  return ret;
+}
 
 
-/*@only@*/
+/*@only@*/ /*@notnull@*/
 static constraintExpr constraintExpr_makeSRefUnaryOp (/*@temp@*/ /*@observer@*/ sRef s,  constraintExprUnaryOpKind op)
 {
   constraintExpr ret;
@@ -635,7 +695,7 @@ constraintExpr constraintExpr_parseMakeUnaryOp (lltok op, constraintExpr cexpr)
   constraintExpr ret;
   ret = constraintExpr_makeUnaryOpConstraintExpr ( cexpr);
 
-  switch (op.tok)
+  switch (lltok_getTok (op))
     {
     case QMAXSET:
       ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXSET);
@@ -644,7 +704,7 @@ constraintExpr constraintExpr_parseMakeUnaryOp (lltok op, constraintExpr cexpr)
       ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXREAD);
       break;
     default:
-      llfatalbug(message("Unhandled Operation in Constraint") );
+      llfatalbug (message ("Unhandled operation in constraint: %s", lltok_unparse (op)));
     }
   return ret;
 }
@@ -698,7 +758,7 @@ constraintExpr constraintExpr_makeValueExpr (/*@exposed@*/ exprNode expr)
   return ret;
 }
 
-/*@only@*/
+/*@only@*/ /*@notnull@*/
 constraintExpr constraintExpr_makeIntLiteral (long i)
 {
   constraintExpr ret;
@@ -708,6 +768,10 @@ constraintExpr constraintExpr_makeIntLiteral (long i)
   ret->data = dmalloc (sizeof *(ret->data) );
   t = constraintTerm_makeIntLiteral (i);
   ret->data = constraintExprData_termSetTerm (ret->data, t);
+
+  ret->ct = FALSE;
+  ret->origType = ctype_undefined; 
+
   return ret;
 }
 
@@ -718,7 +782,7 @@ constraintExpr constraintExpr_makeValueInt (int i)
 }
 */
 
-/*@only@*/
+/*@only@*/ /*@notnull@*/
  /*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void)
       /*@allocates result->data @*/ /*@sets result->kind @*/
 {
@@ -734,7 +798,7 @@ constraintExpr constraintExpr_makeValueInt (int i)
 }
 
 
-static /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExpr (/*@only@*/constraintExpr expr1, /*@only@*/ constraintExpr expr2)
+static /*@notnull@*/ /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExpr (/*@only@*/constraintExpr expr1, /*@only@*/ constraintExpr expr2)
      
 {
   constraintExpr ret;
@@ -743,6 +807,10 @@ static /*@only@*/ constraintExpr constraintExpr_makeBinaryOpConstraintExpr (/*@o
   ret->data = constraintExprData_binaryExprSetExpr1 (ret->data, expr1);
   ret->data = constraintExprData_binaryExprSetExpr2 (ret->data, expr2);
   ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_UNDEFINED);
+
+  ret->ct = FALSE;
+  ret->origType = ctype_undefined; 
+
   return ret;
 }
 
@@ -751,14 +819,20 @@ constraintExpr constraintExpr_parseMakeBinaryOp (/*@only@*/ constraintExpr expr1
 {
   constraintExpr ret;
   ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
-  if (op.tok == TPLUS)
-    ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
-  else if (op.tok == TMINUS)
-    ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
-    else
-      {
-	llassert(FALSE);
-      }
+
+  if (lltok_getTok (op) == TPLUS)
+    {
+      ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_PLUS);
+    }
+  else if (lltok_getTok (op) == TMINUS)
+    {
+      ret->data = constraintExprData_binaryExprSetOp(ret->data, BINARYOP_MINUS);
+    }
+  else
+    {
+      llassert (FALSE);
+    }
+
   return ret;
 }
 
@@ -775,7 +849,7 @@ constraintExpr constraintExpr_parseMakeBinaryOp (/*@only@*/ constraintExpr expr1
 }
 # endif
 
-static /*@only@*/
+static /*@notnull@*/ /*@only@*/
 constraintExpr constraintExpr_makeBinaryOpConstraintExprIntLiteral (/*@only@*/ constraintExpr expr, int literal)
 {
   constraintExpr ret;
@@ -978,20 +1052,25 @@ bool constraintExpr_same (constraintExpr expr1, constraintExpr expr2)
   BADEXIT;
 }
 
-bool constraintExpr_search (/*@observer@*/ constraintExpr c, /*@observer@*/ constraintExpr old)
+bool 
+constraintExpr_search (/*@observer@*/ constraintExpr c, 
+		       /*@observer@*/ constraintExpr old)
 {
   bool ret = FALSE;
   constraintExprKind kind;
   constraintExpr temp;
   
-  if ( constraintExpr_similar (c, old) )
+  if (constraintExpr_similar (c, old))
     {
-      DPRINTF((message ("Found  %q",
-			constraintExpr_unparse(old)
-			)));
+      DPRINTF (("Found  %q", constraintExpr_unparse (old)));
       return TRUE;
     }
 
+  llassert (constraintExpr_isDefined (c) && constraintExpr_isDefined(old) );
+
+  if ( !(constraintExpr_isDefined (c) && constraintExpr_isDefined(old) ) )
+    return FALSE;
+
   kind = c->kind;
   
   switch (kind)
@@ -1022,15 +1101,61 @@ bool constraintExpr_search (/*@observer@*/ constraintExpr c, /*@observer@*/ cons
 {
   constraintExprKind kind;
   constraintExpr temp;
+  constraintExpr ret;
+
+  llassert(constraintExpr_isDefined (newExpr) && (constraintExpr_isDefined (old) && constraintExpr_isDefined(c) ) );
   
   if ( constraintExpr_similar (c, old) )
     {
+      
+      ctype newType, cType;
+
 
+      
+      
+      ret = constraintExpr_copy (newExpr);
+      llassert(constraintExpr_isDefined(ret) );
+      /*drl if newExpr != NULL then ret will != NULL*/
+      
       DPRINTF((message ("Replacing %s with %s",
 			constraintExpr_unparse(old), constraintExpr_unparse(newExpr)
 			)));
+
+      if (constraintExpr_canGetCType(c) && constraintExpr_canGetCType(newExpr) )
+	{
+	  cType = constraintExpr_getCType(c);
+	  newType =  constraintExpr_getCType(newExpr);
+	  
+	  if (ctype_match(cType,newType) )
+	    {
+	      DPRINTF(( message("constraintExpr_searchandreplace: replacing "
+				" %s with type %s with %s with type %s",
+				constraintExpr_print(c), ctype_unparse(cType),
+				constraintExpr_print(newExpr), ctype_unparse(newType)
+				)
+			));
+	      
+	      ret->ct = TRUE;
+	      ret->origType = cType;
+	    }
+	}
+
+      if (constraintExpr_hasMaxSet(c) )
+	{
+	  if (constraintExpr_hasTypeChange(c))
+	  {
+	  DPRINTF(( message("constraintExpr_searchandreplace: encountered "
+			    "MaxSet with changed type %s ",
+			    constraintExpr_print(c) )
+		    ));
+	  
+	  /*fix this with a conversation */
+	  ret = constraintExpr_adjustMaxSetForCast(ret, constraintExpr_getOrigType(c));
+	  }
+	}
       constraintExpr_free(c);
-      return constraintExpr_copy (newExpr);
+      
+      return ret;
     }
 
   kind = c->kind;
@@ -1061,10 +1186,9 @@ bool constraintExpr_search (/*@observer@*/ constraintExpr c, /*@observer@*/ cons
       llassert(FALSE);
     }
   return c;
-  
 }
 
-static constraintExpr constraintExpr_simplifyChildren (/*@returned@*/ constraintExpr c)
+/*@notnull@*/ static constraintExpr constraintExpr_simplifyChildren (/*@returned@*/ /*@notnull@*/ constraintExpr c)
 {
   constraintExprKind kind;
   constraintExpr temp;
@@ -1140,7 +1264,7 @@ constraintExpr constraintExpr_setFileloc (/*@returned@*/ constraintExpr c, filel
   return c;
 }
 
-static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/constraintExpr c)
+static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/ /*@notnull@*/ constraintExpr c)
 {
   constraintExpr e1, e2;
   constraintExprBinaryOpKind  op;
@@ -1183,6 +1307,8 @@ static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/co
 {
   constraintExpr expr1, expr2;
   constraintExprBinaryOpKind op;
+
+  llassert(constraintExpr_isDefined (lexpr)  && constraintExpr_isDefined (expr)  );
   
   if (lexpr->kind != binaryexpr)
     return expr;
@@ -1194,7 +1320,9 @@ static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/co
 
   expr1 = constraintExpr_copy(expr1);
   expr2 = constraintExpr_copy(expr2);
-
+  
+  llassert(constraintExpr_isDefined (expr1)  && constraintExpr_isDefined (expr2)  );
+  
   /* drl possible problem : warning make sure this works */
   
   lexpr->kind = expr1->kind;
@@ -1225,7 +1353,8 @@ static /*@only@*/ constraintExpr constraintExpr_simplifybinaryExpr (/*@only@*/co
 static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ constraintExpr c)
 {
   constraintExpr exp;
-  
+
+  llassert(constraintExpr_isDefined (c) );
   llassert (c->kind == unaryExpr);
 
   DPRINTF ((message ("Doing constraintExpr_simplifyunaryExpr:%s", constraintExpr_unparse (c) ) ) );
@@ -1239,6 +1368,8 @@ static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ co
   exp = constraintExprData_unaryExprGetExpr (c->data);
   exp = constraintExpr_copy(exp);
   
+  llassert(constraintExpr_isDefined (exp)  );
+  
   if (exp->kind == term)
     {
       constraintTerm cterm;
@@ -1353,8 +1484,15 @@ static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ co
   
   /* drl: I think this is an Splint bug */
 
+  llassert ( constraintExpr_isDefined (c) );
+  if (constraintExpr_isUndefined (c) )
+    {
+      return constraintExpr_undefined;
+    }
+  
   ret =  constraintExpr_copy(c);
-
+  llassert(constraintExpr_isDefined (ret) );
+	   
   constraintExpr_free(c);
 
   ret = constraintExpr_simplifyChildren (ret);
@@ -1405,11 +1543,11 @@ cstring constraintExpr_unparse (/*@temp@*/ /*@observer@*/ constraintExpr ex) /*@
 
             if (context_getFlag (FLG_PARENCONSTRAINT) )
 	      {
-		st = message ("(%q) ", constraintTerm_print (constraintExprData_termGetTerm (ex->data)));
+		st = message ("(%q) ", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
 	      }
 	    else
 	      {
-		st = message ("%q", constraintTerm_print (constraintExprData_termGetTerm (ex->data)));
+		st = message ("%q", constraintTerm_unparse (constraintExprData_termGetTerm (ex->data)));
 	      }
       break;
     case unaryExpr:
@@ -1497,6 +1635,50 @@ constraintExpr constraintExpr_doSRefFixBaseParam (/*@returned@*/  constraintExpr
   return expr;
 }
 
+/*
+/ *@only@* / constraintExpr constraintExpr_doSRefFixInvarConstraint (/ *@only@* / constraintExpr expr, sRef s, ctype ct)
+{
+  constraintExprKind kind;
+  constraintExpr expr1, expr2;
+  constraintExprData data;
+  llassert (expr != NULL);
+
+  data = expr->data;
+  
+  kind = expr->kind;
+  
+  switch (kind)
+    {
+    case term:
+      expr = doSRefFixInvarConstraintTerm (expr, s, ct);
+      break;
+    case unaryExpr:
+      expr1 = constraintExprData_unaryExprGetExpr (data);
+      expr1 = constraintExpr_copy(expr1);
+      expr1 = constraintExpr_doSRefFixInvarConstraint (expr1, s, ct);
+      data = constraintExprData_unaryExprSetExpr (data, expr1);
+      break;
+    case binaryexpr:
+      expr1 = constraintExprData_binaryExprGetExpr1 (data);
+      expr2 = constraintExprData_binaryExprGetExpr2 (data);
+      
+      expr1 = constraintExpr_copy(expr1);
+      expr2 = constraintExpr_copy(expr2);
+
+      expr1 = constraintExpr_doSRefFixInvarConstraint (expr1, s, ct);
+      data = constraintExprData_binaryExprSetExpr1 (data, expr1);
+      expr2 = constraintExpr_doSRefFixInvarConstraint (expr2, s, ct);
+      data = constraintExprData_binaryExprSetExpr2 (data, expr2);
+      
+      break;
+    default:
+      llassert(FALSE);
+      data = NULL;
+    }
+  return expr;
+}
+*/
+
 /*@only@*/ constraintExpr constraintExpr_doSRefFixConstraintParam (/*@only@*/ constraintExpr expr, exprNodeList arglist) /*@modifies expr@*/
 {
   constraintExprKind kind;
@@ -1637,12 +1819,20 @@ int constraintExpr_compare (constraintExpr expr1, constraintExpr expr2)
 
 long constraintExpr_getValue (constraintExpr expr)
 {
+  llassert (constraintExpr_isDefined(expr) );
   llassert (expr->kind == term);
+  
   return (constraintTerm_getValue (constraintExprData_termGetTerm (expr->data)));
 }
 
 bool constraintExpr_canGetValue (constraintExpr expr)
 {
+  llassert ( constraintExpr_isDefined (expr) );
+  if (constraintExpr_isUndefined (expr) )
+    {
+      return FALSE;
+    }
+
   switch (expr->kind)
     {
     case term:
@@ -1661,6 +1851,13 @@ fileloc constraintExpr_getFileloc (constraintExpr expr)
 constraintTerm t;
   constraintExprKind kind;
 
+  llassert ( constraintExpr_isDefined (expr) );
+  if (constraintExpr_isUndefined (expr) )
+    {
+      return fileloc_undefined;
+    }
+
+  
  kind = expr->kind;
   
   switch (kind)
@@ -1691,28 +1888,29 @@ doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall)
 {
   constraintTerm t;
   sRef s;
-  /*maybe this should move to cosntraintExpr.c -drl7x 5/18/01*/
-  /*@i22*/
-
-  constraintExprData data = e->data;
-  constraintExprKind kind = e->kind;
-  
+  constraintExprData data;
+  constraintExprKind kind;
   constraintExpr ret;
-
-  llassert(kind == term);
-
+  
+  llassert (constraintExpr_isDefined (e) );
+  
+  data = e->data;
+  kind = e->kind;
+  
+  llassert (kind == term);
+  
   t = constraintExprData_termGetTerm (data);
-  llassert (constraintTerm_isDefined(t) );
-
+  llassert (constraintTerm_isDefined (t));
+  
   ret = e;
-  switch (constraintTerm_getKind(t) )
+
+  switch (constraintTerm_getKind (t))
     {
-    case EXPRNODE:
-      break;
-    case INTLITERAL:
+    case CTT_EXPR:
+    case CTT_INTLITERAL:
       break;
       
-    case SREF:
+    case CTT_SREF:
       s = constraintTerm_getSRef(t);
       if (sRef_isResult (s))
 	{
@@ -1733,9 +1931,13 @@ doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall)
   
 }
 
-/*drl moved from constriantTerm.c 5/20/001*/
-/*@only@*/ static constraintExpr 
-doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
+#if 0
+
+/*to be used for structure checking */
+
+/ *@only@* / static constraintExpr
+doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e,
+ sRef s, ctype ct)
 {
   constraintTerm t;
 
@@ -1756,20 +1958,88 @@ doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@tem
 
   switch (constraintTerm_getKind(t))
     {
-    case EXPRNODE:
-      DPRINTF((message ("%q @ %q ", constraintTerm_print(t),
+    case CTT_EXPR:
+      DPRINTF((message ("%q @ %q ", constraintTerm_unparse(t),
 			fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
       break;
-    case INTLITERAL:
-      DPRINTF((message (" %q ", constraintTerm_print (t)) ));
+    case CTT_INTLITERAL:
+      DPRINTF((message (" %q ", constraintTerm_unparse (t)) ));
       break;
       
-    case SREF:
+    case CTT_SREF:
+      / * evans 2001-07-24: constants should use the original term * /
+      if (!constraintTerm_canGetValue (t))
+	{
+	  sRef snew;
+	  DPRINTF ((message("Doing sRef_fixInvarConstraint for %q ", 
+			     constraintTerm_unparse (t) ) ));
+
+	  snew = fixSref (ct, s, constraintTerm_getSRef(t));
+
+	  ret = constraintExpr_makeTermsRef(snew);
+	  
+	  constraintExpr_free (e);
+	  
+	  DPRINTF (( message("After Doing sRef_fixConstraintParam constraintExpr is %q ", 
+			     constraintExpr_print (ret) ) ));
+	  / *@-branchstate@* /
+	} / *@=branchstate@* /
+
+      break;
+    default:
+      BADEXIT;
+    }
+
+  return ret;
+  
+}
+#endif
+ 
+/*drl moved from constriantTerm.c 5/20/001*/
+/*@only@*/ static constraintExpr 
+doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
+{
+  constraintTerm t;
+
+  constraintExprData data;
+  
+  constraintExprKind kind;
+  
+  constraintExpr ret;
+
+
+  llassert(constraintExpr_isDefined (e) );
+
+  data = e->data;
+  
+  kind = e->kind;
+
+  
+
+  llassert(kind == term);
+
+  t = constraintExprData_termGetTerm (data);
+  llassert (constraintTerm_isDefined(t) );
+
+  ret = e;
+
+  DPRINTF (("Fixing: %s", constraintExpr_print (e)));
+
+  switch (constraintTerm_getKind(t))
+    {
+    case CTT_EXPR:
+      DPRINTF((message ("%q @ %q ", constraintTerm_unparse(t),
+			fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
+      break;
+    case CTT_INTLITERAL:
+      DPRINTF((message (" %q ", constraintTerm_unparse (t)) ));
+      break;
+    case CTT_SREF:
       /* evans 2001-07-24: constants should use the original term */
       if (!constraintTerm_canGetValue (t))
 	{
 	  DPRINTF ((message("Doing sRef_fixConstraintParam for %q ", 
-			     constraintTerm_print (t) ) ));
+			     constraintTerm_unparse (t) ) ));
 	  ret = sRef_fixConstraintParam (constraintTerm_getSRef(t), arglist);
 	  
 	  constraintExpr_free (e);
@@ -1789,22 +2059,30 @@ doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@tem
 }
 
 
-/* bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term) */
-/* { */
-/*   if (constraintTerm_hasTerm (expr->term, term) ) */
-/*     return TRUE; */
+#if 0
+bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term)
+{
+  if (constraintTerm_hasTerm (expr->term, term) )
+    return TRUE;
 
-/*   if ((expr->expr) != NULL) */
-/*     { */
-/*       return ( constraintExpr_includesTerm (expr->expr, term) ); */
-/*     } */
-/*   return FALSE; */
+  if ((expr->expr) != NULL)
+    {
+      return ( constraintExpr_includesTerm (expr->expr, term) );
+    }
+  return FALSE;
 
-/* } */
+}
+#endif
 
 /*drl added 6/11/01 */
 bool constraintExpr_isBinaryExpr (/*@observer@*/ constraintExpr c)
 {
+
+  llassert(constraintExpr_isDefined (c) );
+
+  if ( ! (constraintExpr_isDefined (c) ) )
+    return FALSE;
+  
   if (c->kind == binaryexpr)
     return TRUE;
 
@@ -1815,6 +2093,8 @@ bool constraintExpr_isBinaryExpr (/*@observer@*/ constraintExpr c)
 /*drl added 8/08/001 */
 bool constraintExpr_isTerm (/*@observer@*/ constraintExpr c) /*@*/
 {
+  llassert(constraintExpr_isDefined (c) );
+  
   if (c->kind == term)
     return TRUE;
 
@@ -1826,6 +2106,8 @@ bool constraintExpr_isTerm (/*@observer@*/ constraintExpr c) /*@*/
 {
   constraintTerm term;
   
+  llassert(constraintExpr_isDefined (c) );
+  
   llassert(constraintExpr_isTerm(c) );
 
   term = constraintExprData_termGetTerm(c->data);
@@ -1873,11 +2155,20 @@ static constraintExpr  binaryExpr_undump (FILE *f)
 
   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
 
+  if (! mstring_isDefined(str) )
+    {
+      llfatalbug(message("Library file is corrupted") );
+    }
   
   binaryOp = (constraintExprBinaryOpKind) reader_getInt(&str);
   
   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
 
+  if (! mstring_isDefined(str) )
+    {
+      llfatalbug(message("Library file is corrupted") );
+    }
+
   reader_checkChar (&str, 'e');
   reader_checkChar (&str, '1');
   
@@ -1928,6 +2219,11 @@ static  constraintExpr  unaryExpr_undump ( FILE *f)
   os = str;
   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
 
+  if (! mstring_isDefined(str) )
+    {
+      llfatalbug(message("Library file is corrupted") );
+    }
+
   unaryOp = (constraintExprUnaryOpKind) reader_getInt(&str);
   
   expr = constraintExpr_undump (f);
@@ -1944,6 +2240,12 @@ void  constraintExpr_dump (/*@observer@*/ constraintExpr expr,  FILE *f)
   constraintExprKind kind;
   constraintTerm t;
   
+
+  llassert(constraintExpr_isDefined(expr) );
+  
+  DPRINTF((message("constraintExpr_dump:: dumping constraintExpr %s",
+		   constraintExpr_unparse(expr)
+		   ) ));
   
   kind = expr->kind;
   
@@ -1979,6 +2281,11 @@ void  constraintExpr_dump (/*@observer@*/ constraintExpr expr,  FILE *f)
   
   s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
 
+  if (! mstring_isDefined(s) )
+    {
+      llfatalbug(message("Library file is corrupted") );
+    }
+
   kind = (constraintExprKind) reader_getInt(&s);
 
   free (os);
@@ -2038,4 +2345,357 @@ int constraintExpr_getDepth (constraintExpr ex)
 }
 
 
-     
+bool  constraintExpr_canGetCType (constraintExpr e) /*@*/
+{
+  if (constraintExpr_isUndefined(e) )
+    return FALSE;
+  
+  if (e->kind == term)
+    {
+      return TRUE;
+    }
+  else
+    {
+      DPRINTF(( message("constraintExpr_canGetCType: can't get type for %s ",
+			constraintExpr_print(e) ) ));
+      return FALSE;
+    }
+}
+
+ctype constraintExpr_getCType (constraintExpr e) /*@*/
+{
+  constraintTerm t;
+
+  llassert(constraintExpr_isDefined(e) );
+
+  llassert(constraintExpr_canGetCType(e) );
+
+  switch (e->kind)
+    {
+    case term:
+      t = constraintExprData_termGetTerm (e->data);
+      return (constraintTerm_getCType(t) );
+      /* assume that a unary expression will be an int ... */
+    case unaryExpr:
+      return ctype_signedintegral;
+
+      /* drl for just return type of first operand */
+    case binaryexpr:
+      return (
+	      constraintExpr_getCType
+	      (constraintExprData_binaryExprGetExpr1 (e->data) )
+	      );
+    default:
+      BADEXIT;
+    }
+  BADEXIT;
+}
+
+/* drl add 10-5-001 */
+
+static bool constraintExpr_hasTypeChange(constraintExpr e)
+{
+  llassert(constraintExpr_isDefined(e) );
+  if (constraintExpr_isDefined((e)) && (e->ct == TRUE) )
+    {
+      return TRUE;
+    }
+
+  if (e->kind == unaryExpr)
+    {
+      if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
+	{
+	  constraintExpr ce;
+
+	  ce = constraintExprData_unaryExprGetExpr(e->data);
+
+	  return (constraintExpr_hasTypeChange(ce) );
+	}
+	
+    }
+  return FALSE;
+}
+
+/* drl add 10-5-001 */
+
+static ctype constraintExpr_getOrigType (constraintExpr e)
+{
+
+  llassert(constraintExpr_isDefined(e) );
+  llassert(constraintExpr_hasTypeChange(e) );
+  
+  
+  if (e->ct == TRUE) 
+    {
+      return e->origType;
+    }
+
+  if (e->kind == unaryExpr)
+    {
+      if (constraintExprData_unaryExprGetOp (e->data) == MAXSET)
+	{
+	  constraintExpr ce;
+
+	  ce = constraintExprData_unaryExprGetExpr(e->data);
+
+	  return (constraintExpr_getOrigType(ce) );
+	}
+	
+    }
+
+  BADEXIT;
+} 
+
+/*drl added these around 10/18/001*/
+
+static /*@only@*/ constraintExpr constraintExpr_div (/*@only@*/ constraintExpr e, /*@unused@*/ ctype ct)
+{
+  return e;
+}
+
+
+/*@access exprNode@*/ 
+static /*@only@*/ constraintExpr  constraintTerm_simpleDivTypeExprNode(/*@only@*/ constraintExpr e, ctype ct)
+{
+  exprData data;
+  exprNode t1, t2, expr;
+  lltok tok;
+  constraintTerm t;
+
+  llassert(constraintExpr_isDefined(e) );
+  
+  DPRINTF((
+	   message("constraintTerm_simpleDivTypeExprNode e=%s, ct=%s",
+		   constraintExpr_print(e), ctype_unparse(ct)
+		   )
+	   ));
+  
+  t = constraintExprData_termGetTerm(e->data);
+  
+  expr = constraintTerm_getExprNode(t);
+
+  llassert(constraintExpr_isDefined(e) );
+  llassert(exprNode_isDefined(expr) );
+  
+  if (expr->kind == XPR_OP)
+    {
+      data = expr->edata;
+      
+      t1 = exprData_getOpA (data);
+      t2 = exprData_getOpB (data);
+      tok = exprData_getOpTok (data);
+      if (lltok_isMult(tok) )
+	{
+	  llassert(exprNode_isDefined(t1) && exprNode_isDefined(t2) );
+	  /*drl 3/2/2003 we know this from the fact that it's a
+	    multiplication operation...*/
+	  
+	  if  ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
+	    {
+	      ctype ct2;
+	      
+	      if (t1->kind == XPR_SIZEOFT)
+		{
+		  ct2 = qtype_getType (exprData_getType (t1->edata));
+		}
+	      else
+		{
+		  exprNode tempE;
+		
+		  tempE = exprData_getSingle (t1->edata);
+		  
+		  ct2 =  exprNode_getType (tempE); 
+		}
+	      if (ctype_match (ctype_makePointer(ct2), ct) )
+		{
+		  /* this is a bit sloopy but ... */
+		  		  constraintExpr_free(e);
+		  return constraintExpr_makeExprNode(t2);
+		}
+	    }
+	  
+	  
+	  else   if  ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
+	    {
+	      ctype ct2;
+	      
+	      if (t2->kind == XPR_SIZEOFT)
+		{
+		  ct2 = qtype_getType (exprData_getType (t2->edata));
+		}
+	      else
+		{
+		  exprNode exprTemp;
+		  exprData eDTemp;
+		  
+		  exprTemp = exprData_getSingle (t2->edata);
+
+		  llassert(exprNode_isDefined(exprTemp) );
+		  eDTemp = exprTemp->edata;
+		  
+		  ct2 = qtype_getType (exprData_getType(eDTemp ) );
+		  
+		}
+	      if (ctype_match (ctype_makePointer(ct2),ct) )
+		{
+		  /* sloopy way to do this... */ /*@i22*/
+		  		  constraintExpr_free(e);
+		  return constraintExpr_makeExprNode(t1);
+		}
+	    }
+	  else
+	    {
+	      /*empty*/
+	    }
+	  
+	}
+    }
+  return (constraintExpr_div (e, ct) );
+}
+/*@noaccess exprNode@*/ 
+
+static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype ct)
+{
+  /*@i333*/
+  DPRINTF(( (message("simpleDiv got %s ", constraintExpr_unparse(e) ) )
+	    ));
+
+  llassert(constraintExpr_isDefined(e) );
+  
+  switch (e->kind)
+    {
+    case term:
+      
+      {
+	constraintTerm t;
+
+	t = constraintExprData_termGetTerm(e->data);
+	
+
+	if (constraintTerm_isExprNode (t) )
+	{
+	  return constraintTerm_simpleDivTypeExprNode(e, ct);
+	  
+	  /* search for * size of ct and remove */
+	}
+	return constraintExpr_div (e, ct);
+      }
+      
+    case binaryexpr:
+      {
+	constraintExpr temp;
+	
+	temp = constraintExprData_binaryExprGetExpr1 (e->data);
+	temp = constraintExpr_copy(temp);
+	temp = simpleDivType (temp, ct);
+	
+	e->data = constraintExprData_binaryExprSetExpr1 (e->data, temp);
+	
+	temp = constraintExprData_binaryExprGetExpr2 (e->data);
+	temp = constraintExpr_copy(temp);
+	temp = simpleDivType (temp, ct);
+	e->data = constraintExprData_binaryExprSetExpr2 (e->data, temp);
+
+	DPRINTF(( (message("simpleDiv binaryexpr returning %s ", constraintExpr_unparse(e) ) )
+	    ));
+
+	return e;
+      }
+    case unaryExpr:
+      return constraintExpr_div (e, ct);
+
+    default:
+      BADEXIT;
+    }
+}
+
+static /*@only@*/ constraintExpr constraintExpr_adjustMaxSetForCast(/*@only@*/ constraintExpr e, ctype ct)
+{
+
+  DPRINTF(( (message("constraintExpr_adjustMaxSetForCast got %s ", constraintExpr_unparse(e) ) )
+	    ));
+  
+  e = constraintExpr_makeIncConstraintExpr(e);
+  
+  e = constraintExpr_simplify(e);
+  
+
+  e = simpleDivType (e, ct);
+
+  e = constraintExpr_makeDecConstraintExpr(e);
+  
+  e = constraintExpr_simplify(e);
+  
+  DPRINTF(( (message("constraintExpr_adjustMaxSetForCast returning %s ", constraintExpr_unparse(e) ) )
+	    ));
+
+  return e;
+}
+
+
+bool  constraintExpr_isConstantOnly ( constraintExpr e )
+{
+  DPRINTF(( (message("constraintExpr_isConstantOnly %s ",
+		     constraintExpr_unparse(e) ) )
+	    ));
+
+  llassert(constraintExpr_isDefined(e) );
+
+  switch (e->kind)
+    {
+    case term:
+      {
+	constraintTerm t;
+	
+	t = constraintExprData_termGetTerm(e->data);
+	
+	
+	if (constraintTerm_isConstantOnly (t) )
+	  {
+	    return TRUE;
+	  }
+	else
+	  {
+	    return FALSE;
+	  }
+      }
+      
+    case binaryexpr:
+      {
+	constraintExpr temp1, temp2;
+	
+	temp1 = constraintExprData_binaryExprGetExpr1 (e->data);
+	
+	temp2 = constraintExprData_binaryExprGetExpr2 (e->data);
+	
+	if (constraintExpr_isConstantOnly(temp1) &&
+	    constraintExpr_isConstantOnly(temp2) )
+	  {
+	    return TRUE;
+	  }
+	else
+	  {
+	    return FALSE;
+	  }
+      }
+      
+    case unaryExpr:
+      {
+	constraintExpr temp;
+	
+	temp = constraintExprData_unaryExprGetExpr (e->data );
+
+	if (constraintExpr_isConstantOnly(temp) )
+	  {
+	    return TRUE;
+	  }
+	else
+	  {
+	    return FALSE;
+	  }
+      }
+    default:
+      BADEXIT;
+    }
+}
+