]> andersk Git - splint.git/blobdiff - src/constraintExpr.c
Fixed internal bug that occured when dumping bounds-check annotations involving struc...
[splint.git] / src / constraintExpr.c
index 7dff64c1a3c0eab1c293c5b365d532c2b04d6657..c40a31f2848d4d3b2144e29445d82576068ad77e 100644 (file)
@@ -1,10 +1,34 @@
+/*
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2002 University of Virginia,
+**         Massachusetts Institute of Technology
+**
+** This program is free software; you can redistribute it and/or modify it
+** under the terms of the GNU General Public License as published by the
+** Free Software Foundation; either version 2 of the License, or (at your
+** option) any later version.
+** 
+** This program is distributed in the hope that it will be useful, but
+** WITHOUT ANY WARRANTY; without even the implied warranty of
+** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+** General Public License for more details.
+** 
+** The GNU General Public License is available from http://www.gnu.org/ or
+** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+** MA 02111-1307, USA.
+**
+** For information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
+** For more information: http://www.splint.org
+*/
+
 /*
 ** constraintExpr.c
 */
 
 /* #define DEBUGPRINT 1 */
 
 /*
 ** constraintExpr.c
 */
 
 /* #define DEBUGPRINT 1 */
 
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
 # include "basic.h"
 # include "cgrammar.h"
 # include "cgrammar_tokens.h"
 # include "basic.h"
 # include "cgrammar.h"
 # include "cgrammar_tokens.h"
 
 /*@-czechfcns@*/
 
 
 /*@-czechfcns@*/
 
+/*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */
+/*@-nullderef@*/ /* !!! DRL needs to fix this code! */
+/*@-nullstate@*/ /* !!! DRL needs to fix this code! */
+/*@-temptrans@*/ /* !!! DRL needs to fix this code! */
 
 
 
 
-/*@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);
 
 
 
 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@*/;
 /*@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@*/;
-     
-     
+
+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@*/ static constraintExpr constraintExpr_makeBinaryOp (void) 
      /* @allocates result->data @ @sets result->kind @ */ ;
 
 /*@special@*/ static constraintExpr constraintExpr_makeBinaryOp (void) 
      /* @allocates result->data @ @sets result->kind @ */ ;
 
@@ -190,7 +227,7 @@ static bool isZeroBinaryOp (constraintExpr expr)
 
   op = constraintExprData_binaryExprGetOp (expr->data);
 
 
   op = constraintExprData_binaryExprGetOp (expr->data);
 
-  DPRINTF( (message("constraintExpr_propagateConstants: binaryexpr: %s", constraintExpr_unparse(expr) ) ) );
+  DPRINTF((message("constraintExpr_propagateConstants: binaryexpr: %s", constraintExpr_unparse(expr) ) ) );
 
   expr = removeZero(expr);
   
 
   expr = removeZero(expr);
   
@@ -229,9 +266,9 @@ static bool isZeroBinaryOp (constraintExpr expr)
       constraintExpr_free (expr2);
 
       if (op == BINARYOP_PLUS )
       constraintExpr_free (expr2);
 
       if (op == BINARYOP_PLUS )
-       return (constraintExpr_makeIntLiteral ( (t1+t2) ));
+       return (constraintExpr_makeIntLiteral ((t1+t2) ));
       else if (op ==  BINARYOP_MINUS)
       else if (op ==  BINARYOP_MINUS)
-       return (constraintExpr_makeIntLiteral ( (t1-t2) ));
+       return (constraintExpr_makeIntLiteral ((t1-t2) ));
       else
        BADEXIT;
     }
       else
        BADEXIT;
     }
@@ -288,7 +325,7 @@ static bool isZeroBinaryOp (constraintExpr expr)
       return expr1;
     }
   
       return expr1;
     }
   
-  DPRINTF( (message("constraintExpr_propagateConstants returning: %s", constraintExpr_unparse(expr) ) ) );
+  DPRINTF((message("constraintExpr_propagateConstants returning: %s", constraintExpr_unparse(expr) ) ) );
 
   expr->data = constraintExprData_binaryExprSetExpr1 (expr->data, expr1);
   expr->data = constraintExprData_binaryExprSetExpr2 (expr->data, expr2);
 
   expr->data = constraintExprData_binaryExprSetExpr1 (expr->data, expr1);
   expr->data = constraintExprData_binaryExprSetExpr2 (expr->data, expr2);
@@ -302,7 +339,7 @@ static bool isZeroBinaryOp (constraintExpr expr)
   bool propagate;
   int literal;
 
   bool propagate;
   int literal;
 
-  DPRINTF ( (message ("Before combine %s", constraintExpr_unparse(expr) ) ) );
+  DPRINTF ((message ("Before combine %s", constraintExpr_unparse(expr) ) ) );
   expr = constraintExpr_propagateConstants (expr, &propagate, &literal);
  
 
   expr = constraintExpr_propagateConstants (expr, &propagate, &literal);
  
 
@@ -316,17 +353,19 @@ static bool isZeroBinaryOp (constraintExpr expr)
          expr = ret;
        }
     }
          expr = ret;
        }
     }
-   DPRINTF ( (message ("After combine %s", constraintExpr_unparse(expr) ) ) );
+   DPRINTF ((message ("After combine %s", constraintExpr_unparse(expr) ) ) );
   return expr;
 }
 
 /*@special@*/
   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;
 {
   constraintExpr ret;
   ret = dmalloc (sizeof (*ret) );
   ret->kind = term;
   ret->data = NULL;
+  ret->ct = FALSE;
+  ret->origType = ctype_undefined; 
   return ret;
 }
 
   return ret;
 }
 
@@ -355,10 +394,12 @@ static constraintExpr constraintExpr_alloc (void) /*@post:isnull result->data@*/
 constraintExpr constraintExpr_copy (constraintExpr expr)
 {
   constraintExpr ret;
 constraintExpr constraintExpr_copy (constraintExpr expr)
 {
   constraintExpr ret;
-  ret = constraintExpr_alloc();
+  ret = constraintExpr_alloc ();
   ret->kind = expr->kind;
   
   ret->data = copyExprData (expr->data, expr->kind);
   ret->kind = expr->kind;
   
   ret->data = copyExprData (expr->data, expr->kind);
+  ret->ct = expr->ct;
+  ret->origType = expr->origType;
   return ret;
 }
 
   return ret;
 }
 
@@ -372,6 +413,9 @@ constraintExpr constraintExpr_copy (constraintExpr expr)
   ret->data = dmalloc (sizeof *(ret->data) );
   t = constraintTerm_makeExprNode (e);
   ret->data = constraintExprData_termSetTerm (ret->data, t);
   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;
 }
 
   return ret;
 }
 
@@ -383,7 +427,6 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
  exprNode t, t1, t2;
  lltok tok;
  
  exprNode t, t1, t2;
  lltok tok;
  
  llassert (e != NULL);
  
  data = e->edata;
  llassert (e != NULL);
  
  data = e->edata;
@@ -419,7 +462,13 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
         ce2 = constraintExpr_makeExprNode (t2);
         ret = constraintExpr_parseMakeBinaryOp (ce1, tok, ce2);         
        }
         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
        drl 8-11-001
        
        We handle expressions containing sizeof with the rule
@@ -427,7 +476,10 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
 
        This is the total wronge way to do this but...
        it may be better than nothing
 
        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) )
      else if (lltok_isMult(tok) )
        {
         if  ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
@@ -437,12 +489,13 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
         else if  ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
           {
             ret = constraintExpr_makeExprNode(t1);
         else if  ((t2->kind == XPR_SIZEOF) || (t2->kind == XPR_SIZEOFT) )
           {
             ret = constraintExpr_makeExprNode(t1);
-          }
+            } 
         else
           {
           ret =  oldconstraintExpr_makeTermExprNode (e);
           }
        }
         else
           {
           ret =  oldconstraintExpr_makeTermExprNode (e);
           }
        }
+     */
      else
         ret = oldconstraintExpr_makeTermExprNode (e);
    
      else
         ret = oldconstraintExpr_makeTermExprNode (e);
    
@@ -482,7 +535,7 @@ constraintExpr constraintExpr_makeExprNode (exprNode e)
    case XPR_COMMA:
      t = exprData_getPairA(data);
      ret = constraintExpr_makeExprNode(t);
    case XPR_COMMA:
      t = exprData_getPairA(data);
      ret = constraintExpr_makeExprNode(t);
-     /*@i3434*/ /*I'm not sure if this is right.  I'm adding a break to quite LCLint*/
+     /*@i3434*/ /* drl: I'm not sure if this is right.  I'm adding a break to quiet Splint */
      break;
    default:
      ret = oldconstraintExpr_makeTermExprNode (e);
      break;
    default:
      ret = oldconstraintExpr_makeTermExprNode (e);
@@ -505,6 +558,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->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;
 }
 
   return ret;
 }
@@ -518,6 +573,10 @@ constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s)
   ret->data = dmalloc (sizeof *(ret->data) );
   t = constraintTerm_makesRef (s);
   ret->data = constraintExprData_termSetTerm (ret->data, t);
   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;
 }
 
   return ret;
 }
 
@@ -556,6 +615,9 @@ constraintExpr constraintExpr_makeTermsRef (/*@temp@*/ sRef s)
   ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
   ret->data = constraintExprData_unaryExprSetOp (ret->data, Op);
 
   ret->data = constraintExprData_unaryExprSetExpr (ret->data, cexpr);
   ret->data = constraintExprData_unaryExprSetOp (ret->data, Op);
 
+  ret->ct = FALSE;
+  ret->origType = ctype_undefined; 
+
   return ret;
 }
 
   return ret;
 }
 
@@ -611,7 +673,7 @@ constraintExpr constraintExpr_parseMakeUnaryOp (lltok op, constraintExpr cexpr)
   constraintExpr ret;
   ret = constraintExpr_makeUnaryOpConstraintExpr ( cexpr);
 
   constraintExpr ret;
   ret = constraintExpr_makeUnaryOpConstraintExpr ( cexpr);
 
-  switch (op.tok)
+  switch (lltok_getTok (op))
     {
     case QMAXSET:
       ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXSET);
     {
     case QMAXSET:
       ret->data = constraintExprData_unaryExprSetOp (ret->data, MAXSET);
@@ -684,6 +746,10 @@ constraintExpr constraintExpr_makeIntLiteral (long i)
   ret->data = dmalloc (sizeof *(ret->data) );
   t = constraintTerm_makeIntLiteral (i);
   ret->data = constraintExprData_termSetTerm (ret->data, t);
   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;
 }
 
   return ret;
 }
 
@@ -719,6 +785,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->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;
 }
 
   return ret;
 }
 
@@ -727,14 +797,20 @@ constraintExpr constraintExpr_parseMakeBinaryOp (/*@only@*/ constraintExpr expr1
 {
   constraintExpr ret;
   ret = constraintExpr_makeBinaryOpConstraintExpr (expr1, expr2);
 {
   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;
 }
 
   return ret;
 }
 
@@ -780,7 +856,7 @@ constraintExpr constraintExpr_makeDecConstraintExpr (/*@only@*/constraintExpr ex
 {
   constraintExpr  ret;
   
 {
   constraintExpr  ret;
   
-  DPRINTF ( (message ("Making  subtract expression") ) );
+  DPRINTF ((message ("Making  subtract expression") ) );
 
   ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
   ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_MINUS);
 
   ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
   ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_MINUS);
@@ -794,7 +870,7 @@ constraintExpr addent)
 {
   constraintExpr  ret;
   
 {
   constraintExpr  ret;
   
-  DPRINTF ( (message ("Doing addTerm simplification") ) );
+  DPRINTF ((message ("Doing addTerm simplification") ) );
 
   ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
   ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_PLUS);
 
   ret = constraintExpr_makeBinaryOpConstraintExpr (expr, addent);
   ret->data = constraintExprData_binaryExprSetOp (ret->data, BINARYOP_PLUS);
@@ -998,15 +1074,55 @@ bool constraintExpr_search (/*@observer@*/ constraintExpr c, /*@observer@*/ cons
 {
   constraintExprKind kind;
   constraintExpr temp;
 {
   constraintExprKind kind;
   constraintExpr temp;
+  constraintExpr ret;
   
   if ( constraintExpr_similar (c, old) )
     {
   
   if ( constraintExpr_similar (c, old) )
     {
+      
+      ctype newType, cType;
+
+      
+      ret = constraintExpr_copy (newExpr);
 
       DPRINTF((message ("Replacing %s with %s",
                        constraintExpr_unparse(old), constraintExpr_unparse(newExpr)
                        )));
 
       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);
       constraintExpr_free(c);
-      return constraintExpr_copy (newExpr);
+      
+      return ret;
     }
 
   kind = c->kind;
     }
 
   kind = c->kind;
@@ -1037,7 +1153,6 @@ bool constraintExpr_search (/*@observer@*/ constraintExpr c, /*@observer@*/ cons
       llassert(FALSE);
     }
   return c;
       llassert(FALSE);
     }
   return c;
-  
 }
 
 static constraintExpr constraintExpr_simplifyChildren (/*@returned@*/ constraintExpr c)
 }
 
 static constraintExpr constraintExpr_simplifyChildren (/*@returned@*/ constraintExpr c)
@@ -1206,7 +1321,7 @@ static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ co
 
   DPRINTF ((message ("Doing constraintExpr_simplifyunaryExpr:%s", constraintExpr_unparse (c) ) ) );
   
 
   DPRINTF ((message ("Doing constraintExpr_simplifyunaryExpr:%s", constraintExpr_unparse (c) ) ) );
   
-  if ( (constraintExprData_unaryExprGetOp (c->data) != MAXSET) &&
+  if ((constraintExprData_unaryExprGetOp (c->data) != MAXSET) &&
        (constraintExprData_unaryExprGetOp (c->data) != MAXREAD) )
     {
       return c;
        (constraintExprData_unaryExprGetOp (c->data) != MAXREAD) )
     {
       return c;
@@ -1291,7 +1406,7 @@ static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ co
        
          constraintExpr  temp, temp2;
 
        
          constraintExpr  temp, temp2;
 
-         DPRINTF ( (message ("Doing fancy simplification") ) );
+         DPRINTF ((message ("Doing fancy simplification") ) );
 
          temp = constraintExprData_binaryExprGetExpr2 (exp->data);
 
 
          temp = constraintExprData_binaryExprGetExpr2 (exp->data);
 
@@ -1305,11 +1420,11 @@ static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ co
 
          c = constraintExpr_makeSubtractExpr (c, temp);
 
 
          c = constraintExpr_makeSubtractExpr (c, temp);
 
-         DPRINTF ( (message ("Done fancy simplification:%s", constraintExpr_unparse (c) ) ) );
+         DPRINTF ((message ("Done fancy simplification:%s", constraintExpr_unparse (c) ) ) );
        }
     }
   
        }
     }
   
-  DPRINTF ( (message ("constraintExpr_simplifyUnaryExpr: Done simplification:%s", constraintExpr_unparse (c) ) ) );
+  DPRINTF ((message ("constraintExpr_simplifyUnaryExpr: Done simplification:%s", constraintExpr_unparse (c) ) ) );
 
   constraintExpr_free(exp);
   return c;
 
   constraintExpr_free(exp);
   return c;
@@ -1322,12 +1437,12 @@ static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ co
   constraintExpr ret;
   constraintTerm t;
   
   constraintExpr ret;
   constraintTerm t;
   
-  DPRINTF ( (message ("Doing constraintExpr_simplify:%s", constraintExpr_unparse (c) ) ) );  
+  DPRINTF ((message ("Doing constraintExpr_simplify:%s", constraintExpr_unparse (c) ) ) );  
   
 
   /*@i22*/
   
   
 
   /*@i22*/
   
-  /*I think this is an LCLint bug */
+  /* drl: I think this is an Splint bug */
 
   ret =  constraintExpr_copy(c);
 
 
   ret =  constraintExpr_copy(c);
 
@@ -1360,7 +1475,7 @@ static /*@only@*/ constraintExpr constraintExpr_simplifyunaryExpr (/*@only@*/ co
       llassert(FALSE);
     }    
   
       llassert(FALSE);
     }    
   
-  DPRINTF ( (message ("constraintExpr_simplify returning :%s", constraintExpr_unparse (ret) ) ) );  
+  DPRINTF ((message ("constraintExpr_simplify returning :%s", constraintExpr_unparse (ret) ) ) );  
   return ret;
   
 }
   return ret;
   
 }
@@ -1473,6 +1588,50 @@ constraintExpr constraintExpr_doSRefFixBaseParam (/*@returned@*/  constraintExpr
   return expr;
 }
 
   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;
 /*@only@*/ constraintExpr constraintExpr_doSRefFixConstraintParam (/*@only@*/ constraintExpr expr, exprNodeList arglist) /*@modifies expr@*/
 {
   constraintExprKind kind;
@@ -1708,7 +1867,67 @@ doFixResultTerm (/*@only@*/ constraintExpr e, /*@exposed@*/ exprNode fcnCall)
   return ret;
   
 }
   return ret;
   
 }
+/*
+/ *@only@* / static constraintExpr
+doSRefFixInvarConstraintTerm (/ *@only@* / constraintExpr e,
+ sRef s, ctype ct)
+{
+  constraintTerm t;
 
 
+  constraintExprData data = e->data;
+  
+  constraintExprKind kind = e->kind;
+  
+  constraintExpr ret;
+
+  llassert(kind == term);
+
+  t = constraintExprData_termGetTerm (data);
+  llassert (constraintTerm_isDefined(t) );
+
+  ret = e;
+
+  DPRINTF (("Fixing: %s", constraintExpr_print (e)));
+
+  switch (constraintTerm_getKind(t))
+    {
+    case EXPRNODE:
+      DPRINTF((message ("%q @ %q ", constraintTerm_print(t),
+                       fileloc_unparse (constraintTerm_getFileloc(t) ) ) ));
+      break;
+    case INTLITERAL:
+      DPRINTF((message (" %q ", constraintTerm_print (t)) ));
+      break;
+      
+    case 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_print (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;
+  
+}
+*/
 /*drl moved from constriantTerm.c 5/20/001*/
 /*@only@*/ static constraintExpr 
 doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
 /*drl moved from constriantTerm.c 5/20/001*/
 /*@only@*/ static constraintExpr 
 doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@temp@*/ exprNodeList arglist)
@@ -1770,7 +1989,7 @@ doSRefFixConstraintParamTerm (/*@only@*/ constraintExpr e, /*@observer@*/ /*@tem
 /*   if (constraintTerm_hasTerm (expr->term, term) ) */
 /*     return TRUE; */
 
 /*   if (constraintTerm_hasTerm (expr->term, term) ) */
 /*     return TRUE; */
 
-/*   if ( (expr->expr) != NULL) */
+/*   if ((expr->expr) != NULL) */
 /*     { */
 /*       return ( constraintExpr_includesTerm (expr->expr, term) ); */
 /*     } */
 /*     { */
 /*       return ( constraintExpr_includesTerm (expr->expr, term) ); */
 /*     } */
@@ -1845,8 +2064,8 @@ static constraintExpr  binaryExpr_undump (FILE *f)
   char * str;
   char * os;
 
   char * str;
   char * os;
 
-  str = mstring_create (MAX_DUMP_LINE_LENGTH);
-  os = str;
+  os = mstring_create (MAX_DUMP_LINE_LENGTH);
+
   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
 
   
   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
 
   
@@ -1920,6 +2139,10 @@ void  constraintExpr_dump (/*@observer@*/ constraintExpr expr,  FILE *f)
   constraintExprKind kind;
   constraintTerm t;
   
   constraintExprKind kind;
   constraintTerm t;
   
+
+  DPRINTF((message("constraintExpr_dump:: dumping constraintExpr %s",
+                  constraintExpr_unparse(expr)
+                  ) ));
   
   kind = expr->kind;
   
   
   kind = expr->kind;
   
@@ -2014,4 +2237,257 @@ int constraintExpr_getDepth (constraintExpr ex)
 }
 
 
 }
 
 
-     
+bool  constraintExpr_canGetCType (constraintExpr e) /*@*/
+{
+  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_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)
+{
+  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_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;
+}
+
+static /*@only@*/ constraintExpr  constraintTerm_simpleDivTypeExprNode(/*@only@*/ constraintExpr e, ctype ct)
+{
+  exprData data;
+  exprNode t1, t2, expr;
+  lltok tok;
+  constraintTerm t;
+
+  DPRINTF((
+          message("constraintTerm_simpleDivTypeExprNode e=%s, ct=%s",
+                  constraintExpr_print(e), ctype_unparse(ct)
+                  )
+          ));
+  
+  t = constraintExprData_termGetTerm(e->data);
+  
+  expr = constraintTerm_getExprNode(t);
+  
+  if (expr->kind == XPR_OP)
+    {
+      data = expr->edata;
+      
+      t1 = exprData_getOpA (data);
+      t2 = exprData_getOpB (data);
+      tok = exprData_getOpTok (data);
+      if (lltok_isMult(tok) )
+       {
+         
+         if  ((t1->kind == XPR_SIZEOF) || (t1->kind == XPR_SIZEOFT) )
+           {
+             ctype ct2;
+             
+             if (t1->kind == XPR_SIZEOFT)
+               {
+                 ct2 = qtype_getType (exprData_getType (t1->edata));
+               }
+             else
+               {
+                 ct2 = qtype_getType (exprData_getType(exprData_getSingle (t1->edata)->edata ) );
+               }
+             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
+               {
+                 ct2 = qtype_getType (exprData_getType(exprData_getSingle (t2->edata)->edata ) );
+               }
+             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) );
+}
+
+static /*@only@*/ constraintExpr simpleDivType (/*@only@*/ constraintExpr e, ctype ct)
+{
+  /*@i333*/
+  DPRINTF(( (message("simpleDiv got %s ", constraintExpr_unparse(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;
+}
+
This page took 0.715578 seconds and 4 git commands to generate.