X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/ef2aa32aebac950c1784a2dd25f0fa299b8840da..9280addf7928b095ee9e0b047d698c05140726aa:/src/constraint.c

diff --git a/src/constraint.c b/src/constraint.c
index 65d6ba4..2187b0d 100644
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -133,6 +133,8 @@ constraint constraint_copy (constraint c)
   ret->ar = c->ar;
   ret->expr =  constraintExpr_copy (c->expr);
   ret->post = c->post;
+  ret->generatingExpr = c->generatingExpr;
+  
   /*@i33 fix this*/
   if (c->orig != NULL)
     ret->orig = constraint_copy (c->orig);
@@ -154,7 +156,7 @@ void constraint_overWrite (constraint c1, constraint c2)
     c1->orig = constraint_copy (c2->orig);
   else
     c1->orig = NULL;
-
+  c1->generatingExpr = c2->generatingExpr;
 }
 
 bool constraint_resolve (/*@unused@*/ constraint c)
@@ -173,16 +175,54 @@ constraint constraint_makeNew (void)
   ret->ar = LT;
   ret->post = FALSE;
   ret->orig = NULL;
+  ret->generatingExpr = NULL;
   /*@i23*/return ret;
 }
 
+constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
+{
+    
+  if (c->generatingExpr == NULL)
+    {
+      c->generatingExpr = e;
+      DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
+    }
+  else
+    {
+      DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
+    }
+  return c;
+}
+
 fileloc constraint_getFileloc (constraint c)
 {
+  if (c->generatingExpr)
+    return (exprNode_getfileloc (c->generatingExpr) );
+	    
   return (constraintExpr_getFileloc (c->lexpr) );
 
 
 }
 
+static bool checkForMaxSet (constraint c)
+{
+  if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
+    return TRUE;
+
+  return FALSE;
+}
+
+bool constraint_hasMaxSet(constraint c)
+{
+  if (c->orig)
+    {
+      if (checkForMaxSet(c->orig) )
+	return TRUE;
+    }
+
+  return (checkForMaxSet(c) );
+}
+
 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 {
   constraint ret = constraint_makeNew();
@@ -348,6 +388,23 @@ exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
   return dst;
 }
 
+constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
+{
+  constraint ret = constraint_makeNew();
+  //constraintTerm term;
+
+  e = exprNode_fakeCopy(e);
+  ret->lexpr = constraintExpr_makeValueExpr (e);
+  ret->ar = EQ;
+  ret->post = TRUE;
+  ret->expr =  constraintExpr_makeValueExpr (e);
+  ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);
+
+  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
+//   fileloc_incColumn (  ret->lexpr->term->loc);
+//   fileloc_incColumn (  ret->lexpr->term->loc);
+  return ret;
+}
 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 {
   constraint ret = constraint_makeNew();
@@ -419,16 +476,23 @@ cstring arithType_print (arithType ar)
 void constraint_printError (constraint c, fileloc loc)
 {
   cstring string;
-
+  fileloc errorLoc;
+  
   string = constraint_printDetailed (c);
+
+  errorLoc = loc;
+
+  if (constraint_getFileloc(c) )
+    errorLoc = constraint_getFileloc(c);
+  
   
   if (c->post)
     {
-       voptgenerror (FLG_FUNCTIONPOST, string, loc);
+       voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
     }
   else
     {
-      voptgenerror (FLG_FUNCTIONCONSTRAINT, string, loc);
+      voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
     }
       
 }
@@ -453,6 +517,22 @@ cstring  constraint_printDetailed (constraint c)
       else
 	st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));	
     }
+
+  if (context_getFlag (FLG_CONSTRAINTLOCATION) )
+    {
+      cstring temp;
+      // llassert (c->generatingExpr);
+      temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
+		      exprNode_unparse(c->generatingExpr) );
+      st = cstring_concat (st, temp);
+
+      if (constraint_hasMaxSet(c) )
+	{
+	  cstring temp2;
+	  temp2 = message ("\nHas MaxSet\n");
+	  st = cstring_concat (st, temp2);
+	}
+    }
   return st;
 }