X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/2934b455c4074408a0f819009c071456f021ba21..3be9a1658ba93935ee9ba8bfd5a990a8d9fb1377:/src/constraint.c

diff --git a/src/constraint.c b/src/constraint.c
index a3a849e..51f1d67 100644
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -1,8 +1,32 @@
+/*
+** LCLint - annotation-assisted static program checker
+** Copyright (C) 1994-2001 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 lclint: lclint-request@cs.virginia.edu
+** To report a bug: lclint-bug@cs.virginia.edu
+** For more information: http://lclint.cs.virginia.edu
+*/
+
 /*
 ** constraint.c
 */
 
-//#define DEBUGPRINT 1
+/* #define DEBUGPRINT 1 */
 
 # include <ctype.h> /* for isdigit */
 # include "lclintMacros.nf"
@@ -11,65 +35,34 @@
 # include "cgrammar_tokens.h"
 
 # include "exprChecks.h"
-# include "aliasChecks.h"
 # include "exprNodeSList.h"
 
 /*@i33*/
-/*@-fcnuse*/
-/*@-assignexpose*/
 
 /*@access exprNode @*/
 
 
-static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c);
+static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
 
 
-static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
-     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
+static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
+     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/
+     /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
      
-/*  constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant) */
-     
-/*  { */
-/*    char *t; */
-/*    int c; */
-/*    constraint ret; */
-/*    ret = constraint_makeNew(); */
-/*    llassert (sRef_isValid(x) ); */
-/*    if (!sRef_isValid(x)) */
-/*      return ret; */
- 
-    
-/*    ret->lexpr = constraintExpr_makeTermsRef (x); */
-/*    #warning fix abstraction */
-
-/*    if (relOp.tok == GE_OP) */
-/*        ret->ar = GTE; */
-/*    else if (relOp.tok == LE_OP) */
-/*      ret->ar = LTE; */
-/*    else if (relOp.tok == EQ_OP) */
-/*      ret->ar = EQ; */
-/*    else */
-/*      llfatalbug(message ("Unsupported relational operator") ); */
-
-
-/*    t =  cstring_toCharsSafe (exprNode_unparse(cconstant)); */
-/*    c = atoi( t ); */
-/*    ret->expr = constraintExpr_makeIntLiteral (c); */
-
-/*    ret->post = TRUE; */
-/*    //  ret->orig = ret; */
-/*    DPRINTF(("GENERATED CONSTRAINT:")); */
-/*    DPRINTF( (message ("%s", constraint_print(ret) ) ) ); */
-/*    return ret; */
-/*  } */
+static void
+advanceField (char **s)
+{
+  reader_checkChar (s, '@');
+}
 
-constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)    
+# if 0
+static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)    
 {
   char *t;
   int c;
   constraint ret;
-  ret = constraint_makeNew();
-  llassert (l!=NULL);
+  ret = constraint_makeNew ();
+  llassert (constraintExpr_isDefined(l) );
       
   ret->lexpr = constraintExpr_copy (l);
 
@@ -89,23 +82,31 @@ constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconsta
   ret->expr = constraintExpr_makeIntLiteral (c);
 
   ret->post = TRUE;
-  //  ret->orig = ret;
   DPRINTF(("GENERATED CONSTRAINT:"));
   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
   return ret;
 }
+# endif
 
 bool constraint_same (constraint c1, constraint c2)
 {
-  
-  if (c1->ar != c2->ar)
-    return FALSE;
+  llassert (c1 != NULL);
+  llassert (c2 != NULL);
 
+  if (c1->ar != c2->ar)
+    {
+      return FALSE;
+    }
+  
   if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
-    return FALSE;
+    {
+      return FALSE;
+    }
 
   if (!constraintExpr_similar (c1->expr, c2->expr) )
-    return FALSE;
+    {
+      return FALSE;
+    }
 
   return TRUE;
 }
@@ -114,7 +115,7 @@ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r
 {
   constraint ret;
   ret = constraint_makeNew();
-  llassert (l !=NULL);
+  llassert (constraintExpr_isDefined(l) );
     
   ret->lexpr = constraintExpr_copy (l);
 
@@ -134,26 +135,27 @@ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r
   ret->orig = constraint_copy(ret);
 
   ret = constraint_simplify (ret);
-  
-  //  ret->orig = ret;
+  /* ret->orig = ret; */
+
   DPRINTF(("GENERATED CONSTRAINT:"));
   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
   return ret;
 }
 
-constraint constraint_copy (constraint c)
+constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
 {
   constraint ret;
 
   llassert (constraint_isDefined(c) );
-  // TPRINTF((message("Copying constraint %q", constraint_print) ));
-  
+
   ret = constraint_makeNew();
   ret->lexpr = constraintExpr_copy (c->lexpr);
   ret->ar = c->ar;
   ret->expr =  constraintExpr_copy (c->expr);
   ret->post = c->post;
-  ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr);
+  /*@-assignexpose@*/
+  ret->generatingExpr = c->generatingExpr;
+  /*@=assignexpose@*/
   
   /*@i33 fix this*/
   if (c->orig != NULL)
@@ -208,14 +210,17 @@ void constraint_overWrite (constraint c1, constraint c2)
     c1->or = NULL;
 
   c1->fcnPre = c2->fcnPre;
-  
+
+  /*@-assignexpose@*/
   c1->generatingExpr = c2->generatingExpr;
+  /*@=assignexpose@*/
 }
 
 
 
 static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
-     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
+     /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/ 
+     /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
 {
   constraint ret;
   ret = dmalloc(sizeof (*ret) );
@@ -230,12 +235,12 @@ static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
   return ret;
 }
 
-constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
+constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
 {
     
   if (c->generatingExpr == NULL)
     {
-      c->generatingExpr = exprNode_fakeCopy(e);
+      c->generatingExpr = e;
       DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
     }
   else
@@ -269,7 +274,7 @@ constraint constraint_setFcnPre (/*@returned@*/ constraint c )
   else
     {
       c->fcnPre = TRUE;
-      TPRINTF(( message("Warning Setting fcnPre directly") ));
+      DPRINTF(( message("Warning Setting fcnPre directly") ));
     }
   return c;
 }
@@ -297,21 +302,24 @@ static bool checkForMaxSet (constraint c)
 
 bool constraint_hasMaxSet(constraint c)
 {
+  if (checkForMaxSet(c) )
+    return TRUE;
+  
   if (c->orig != NULL)
     {
       if (checkForMaxSet(c->orig) )
 	return TRUE;
     }
 
-  return (checkForMaxSet(c) );
+  return FALSE;
 }
 
-constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
+constraint constraint_makeReadSafeExprNode (  exprNode po, exprNode ind)
 {
   constraint ret = constraint_makeNew();
-  //  constraintTerm term;
-  po = exprNode_fakeCopy(po);
-  ind = exprNode_fakeCopy(ind);
+
+  po = po;
+  ind = ind;
   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
   ret->ar    = GTE;
   ret->expr  = constraintExpr_makeValueExpr (ind);
@@ -319,7 +327,7 @@ constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
   return ret;
 }
 
-constraint constraint_makeWriteSafeInt (exprNode po, int ind)
+constraint constraint_makeWriteSafeInt (   exprNode po, int ind)
 {
   constraint ret = constraint_makeNew();
 
@@ -379,15 +387,13 @@ constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 }
 
 
-constraint constraint_makeReadSafeInt ( exprNode po, int ind)
+constraint constraint_makeReadSafeInt ( exprNode t1, int index)
 {
   constraint ret = constraint_makeNew();
 
-  po = exprNode_fakeCopy(po);
-  
-  ret->lexpr = constraintExpr_makeMaxReadExpr(po);
+  ret->lexpr = constraintExpr_makeMaxReadExpr(t1);
   ret->ar    = GTE;
-  ret->expr  = constraintExpr_makeIntLiteral (ind);
+  ret->expr  = constraintExpr_makeIntLiteral (index);
   ret->post = FALSE;
   return ret;
 }
@@ -404,20 +410,14 @@ constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
   /*@i1*/return ret;
 }
 
-constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
+constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
 {
   constraint ret;
-
-  e1 = exprNode_fakeCopy (e1);
-  t2 = exprNode_fakeCopy (t2);
-  
-  ret = constraint_makeReadSafeExprNode(e1, t2);
-
-  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
   
+  ret = constraint_makeReadSafeExprNode(t1, t2);
+  ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);  
   ret->post = TRUE;  
 
-  //  fileloc_incColumn (ret->lexpr->term->loc);
   return ret;
 }
 
@@ -426,8 +426,7 @@ static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintE
 
   constraint ret;
   
-  llassert(c1 && c2);
-  //  llassert(sequencePoint);
+  llassert(constraintExpr_isDefined(c1) && constraintExpr_isDefined(c2) );
 
   ret = constraint_makeNew();
   
@@ -439,25 +438,23 @@ static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintE
   return ret;
 }
 
-static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
+static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint,  arithType  ar)
 {
   constraintExpr c1, c2;
   constraint ret;
   exprNode e;
 
-  if (! (e1 && e2) )
+  if (! (exprNode_isDefined(e1) && exprNode_isDefined(e2) ) )
     {
       llcontbug((message("null exprNode, Exprnodes are %s and %s",
 		       exprNode_unparse(e1), exprNode_unparse(e2) )
-	       ));
+		 ));
     }
 
-  //  llassert (sequencePoint);
-  
-  e  =  exprNode_fakeCopy(e1);
+  e  =  e1;
   c1 =  constraintExpr_makeValueExpr (e);
   
-  e  =  exprNode_fakeCopy(e2);
+  e  =  e2;
   c2 =  constraintExpr_makeValueExpr (e);
 
   ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
@@ -576,26 +573,19 @@ constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequen
 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();
-  //constraintTerm term;
 
-  e = exprNode_fakeCopy(e);
   ret->lexpr = constraintExpr_makeValueExpr (e);
   ret->ar = EQ;
   ret->post = TRUE;
@@ -603,13 +593,11 @@ constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc seq
   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 
   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
-//   fileloc_incColumn (  ret->lexpr->term->loc);
-//   fileloc_incColumn (  ret->lexpr->term->loc);
   return ret;
 }
 
 
-void constraint_free (/*@only@*/ /*@notnull@*/ constraint c)
+void constraint_free (/*@only@*/ constraint c)
 {
   llassert(constraint_isDefined (c) );
 
@@ -632,47 +620,31 @@ void constraint_free (/*@only@*/ /*@notnull@*/ constraint c)
   
 }
 
-
-// constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
-// {
-//   constraint ret = constraint_makeNew();
-//   //constraintTerm term;
-
-//   e = exprNode_fakeCopy(e);
-//   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
-//   ret->ar = EQ;
-//   ret->post = TRUE;
-//   ret->expr = constraintExpr_makeIncConstraintExpr (e);
-//   ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
-//   return ret;
-// }
-
-
 cstring arithType_print (arithType ar) /*@*/
 {
   cstring st = cstring_undefined;
   switch (ar)
     {
     case LT:
-      st = cstring_makeLiteral (" < ");
+      st = cstring_makeLiteral ("<");
       break;
     case	LTE:
-      st = cstring_makeLiteral (" <= ");
+      st = cstring_makeLiteral ("<=");
       break;
     case 	GT:
-      st = cstring_makeLiteral (" > ");
+      st = cstring_makeLiteral (">");
       break;
     case 	GTE:
-      st = cstring_makeLiteral (" >= ");
+      st = cstring_makeLiteral (">=");
       break;
     case	EQ:
-      st = cstring_makeLiteral (" == ");
+      st = cstring_makeLiteral ("==");
       break;
     case	NONNEGATIVE:
-      st = cstring_makeLiteral (" NONNEGATIVE ");
+      st = cstring_makeLiteral ("NONNEGATIVE");
       break;
     case	POSITIVE:
-      st = cstring_makeLiteral (" POSITIVE ");
+      st = cstring_makeLiteral ("POSITIVE");
       break;
     default:
       llassert(FALSE);
@@ -706,6 +678,22 @@ void constraint_printErrorPostCondition (constraint c, fileloc loc)
     }
 }
 
+ /*drl added 8-11-001*/
+cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
+{
+  cstring string, ret;
+  fileloc errorLoc;
+  
+  string = constraint_print(c);
+
+  errorLoc = constraint_getFileloc(c);
+
+  ret = message ("constraint: %q @ %q", string, fileloc_unparse(errorLoc) );
+
+  fileloc_free(errorLoc);
+  return ret;
+
+}
 
 
 
@@ -713,58 +701,69 @@ void constraint_printError (constraint c, fileloc loc)
 {
   cstring string;
   fileloc errorLoc, temp;
-  
+
+
+  /*drl 11/26/2001 avoid printing tautological constraints */
+  if (constraint_isAlwaysTrue(c) )
+    {
+      return;
+    }
+
+
   string = constraint_printDetailed (c);
 
   errorLoc = loc;
 
-  loc = NULL;
-
   temp = constraint_getFileloc(c);
 
   if (fileloc_isDefined(temp) )
     {
       errorLoc = temp;
-      
-      if (c->post)
-	{
-	  voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
-	}
-      else
-	{
-	  voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
-	}
+    }
+  else
+    {
+      llassert(FALSE);
+      DPRINTF (("constraint %s had undefined fileloc %s", constraint_print(c), fileloc_unparse(temp)));
       fileloc_free(temp);
+      errorLoc = fileloc_copy(errorLoc);
+    }
+      
+  if (c->post)
+    {
+      voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
     }
   else
     {
-      if (c->post)
-	{
-	  voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
-	}
+      if (constraint_hasMaxSet (c) )
+	voptgenerror (FLG_ARRAYBOUNDS, string, errorLoc);
       else
-	{
-	  voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
-	}
+	voptgenerror (FLG_ARRAYBOUNDSREAD, string, errorLoc);
     }
+
+  fileloc_free(errorLoc);
+
 }
 
 
-cstring constraint_printDeep (constraint c)
+static cstring constraint_printDeep (constraint c)
 {
+  cstring genExpr;
   cstring st = cstring_undefined;
 
   st = constraint_print(c);
 
+  
   if (c->orig != constraint_undefined)
     {
+      st = cstring_appendChar(st, '\n');
+      genExpr =  exprNode_unparse(c->orig->generatingExpr);
       if (!c->post)
 	{
 	  if (c->orig->fcnPre)
-	    st = cstring_concatFree(st, (message(" derived from %s precondition: %q", exprNode_unparse(c->orig->generatingExpr), constraint_printDeep(c->orig) )
+	    st = cstring_concatFree(st, (message(" derived from %s precondition: %q", genExpr, constraint_printDeep(c->orig) )
 					 ) );
 	  else
-	    st = cstring_concatFree(st,(message(" needed to satisfy %q",
+	    st = cstring_concatFree(st,(message(" needed to satisfy precondition:\n%q",
 						constraint_printDeep(c->orig) )
 					) );
 	  
@@ -785,15 +784,19 @@ cstring constraint_printDeep (constraint c)
 static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
 {
   cstring st = cstring_undefined;
-
+  cstring genExpr;
+  
   st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
- 
+
+  genExpr = exprNode_unparse (c->generatingExpr);
+    
   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
     {
       cstring temp;
-      // llassert (c->generatingExpr);
-      temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
-		      exprNode_unparse(c->generatingExpr) );
+
+      temp = message ("\nOriginal Generating expression %q: %s\n", 
+		      fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
+		      genExpr );
       st = cstring_concatFree (st, temp);
 
       if (constraint_hasMaxSet(c) )
@@ -808,30 +811,38 @@ static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/
 cstring  constraint_printDetailed (constraint c)
 {
   cstring st = cstring_undefined;
-
+  cstring temp = cstring_undefined;
+    cstring genExpr;
+  
   if (!c->post)
     {
-      st = message ("Unresolved constraint:\nLclint is unable to resolve %q", constraint_printDeep (c) );
+      st = message ("Unable to resolve constraint:\n%q", constraint_printDeep (c) );
     }
   else
     {
       st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c) );
     }
 
+  if (constraint_hasMaxSet(c) )
+    {
+      temp = cstring_makeLiteral("Possible out-of-bounds store:\n");
+    }
+  else
+    {
+      temp = cstring_makeLiteral("Possible out-of-bounds read:\n");
+    }
+  
+  genExpr = exprNode_unparse (c->generatingExpr);
+  
   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
     {
-      cstring temp;
-      // llassert (c->generatingExpr);
-      temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
-		      exprNode_unparse(c->generatingExpr) );
-      st = cstring_concatFree (st, temp);
-
-      if (constraint_hasMaxSet(c) )
-	{
-	  temp = message ("Has MaxSet\n");
-	  st = cstring_concatFree (st, temp);
-	}
+      cstring temp2;
+      temp2 = message ("%s\n", genExpr );
+      temp = cstring_concatFree (temp, temp2);
     }
+
+  st  = cstring_concatFree(temp,st);
+  
   return st;
 }
 
@@ -842,18 +853,45 @@ cstring  constraint_printDetailed (constraint c)
   llassert (c !=NULL);
   if (c->post)
     {
-      type = cstring_makeLiteral ("Ensures: ");
+      if (context_getFlag (FLG_PARENCONSTRAINT) )
+	{
+	  type = cstring_makeLiteral ("ensures: ");
+	}
+      else
+	{
+	   type = cstring_makeLiteral ("ensures");
+	}
     }
   else
     {
-      type = cstring_makeLiteral ("Requires: ");
+      if (context_getFlag (FLG_PARENCONSTRAINT) )
+	{
+	  type = cstring_makeLiteral ("requires: ");
+	}
+      else
+	{
+	  type = cstring_makeLiteral ("requires");
+	}
+	
     }
-  st = message ("%q: %q %q %q",
-		type,
-		constraintExpr_print (c->lexpr),
-		arithType_print(c->ar),
-		constraintExpr_print(c->expr)
+      if (context_getFlag (FLG_PARENCONSTRAINT) )
+	{
+	  st = message ("%q: %q %q %q",
+			type,
+			constraintExpr_print (c->lexpr),
+			arithType_print(c->ar),
+			constraintExpr_print(c->expr)
+			);
+	}
+      else
+	{
+	  st = message ("%q %q %q %q",
+			type,
+			constraintExpr_print (c->lexpr),
+			arithType_print(c->ar),
+			constraintExpr_print(c->expr)
 		);
+	}
   return st;
 }
 
@@ -892,7 +930,7 @@ cstring  constraint_printOr (constraint c) /*@*/
 }
 
 
-constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
+constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
 {
   postcondition = constraint_copy (postcondition);
   postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
@@ -913,19 +951,6 @@ constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
   return precondition;
 }
 
-// bool constraint_hasTerm (constraint c, constraintTerm term)
-// {
-//   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
-  
-//   if (constraintExpr_includesTerm (c->lexpr, term) )
-//     return TRUE;
-
-//   if (constraintExpr_includesTerm (c->expr, term) )
-//     return TRUE;
-
-//   return FALSE;
-// }
-
 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
 {
 
@@ -944,9 +969,17 @@ constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @
       c->orig = NULL;
       c->orig = constraint_copy (c);
       if (c->orig->orig == NULL)
-	c->orig->orig = temp;
+	{
+	  c->orig->orig = temp;
+	  temp = NULL;
+	}
       else
-	llcontbug((message("Expected c->orig->orig to be null" ) ));
+	{
+	  llcontbug((message("Expected c->orig->orig to be null" ) ));
+	  constraint_free(c->orig->orig);
+	  c->orig->orig = temp;
+	  temp = NULL;
+	}
     }
   else
     {
@@ -982,3 +1015,161 @@ bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c)
   else
     return TRUE;
 }
+
+
+constraint constraint_undump (FILE *f)
+{
+  constraint c;
+  bool           fcnPre;
+  bool post;
+  arithType       ar;
+  
+  constraintExpr lexpr;
+  constraintExpr  expr;
+
+
+  char * s;
+
+  char *os;
+
+  os = mstring_create (MAX_DUMP_LINE_LENGTH);
+
+  s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+  /*@i33*/ /*this should probably be wrappered...*/
+  
+  fcnPre = (bool) reader_getInt (&s);
+  advanceField(&s);
+  post = (bool) reader_getInt (&s);
+  advanceField(&s);
+  ar = (arithType) reader_getInt (&s);
+
+  s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+  reader_checkChar (&s, 'l');
+
+  lexpr = constraintExpr_undump (f);
+
+  s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+
+  reader_checkChar (&s, 'r');
+  expr = constraintExpr_undump (f);
+
+  c = constraint_makeNew();
+  
+  c->fcnPre = fcnPre; 
+  c->post = post;
+  c->ar = ar;
+
+  c->lexpr = lexpr;
+  c->expr =  expr;
+
+  free(os);
+  c = constraint_preserveOrig(c);
+  return c;
+}
+
+
+void constraint_dump (/*@observer@*/ constraint c,  FILE *f)
+{
+  bool           fcnPre;
+  bool post;
+  arithType       ar;
+  
+  constraintExpr lexpr;
+  constraintExpr  expr;
+
+
+  fcnPre = c->fcnPre;
+  post   = c->post;
+  ar     = c->ar;
+  lexpr = c->lexpr;
+  expr = c->expr;
+  
+  fprintf(f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
+  fprintf(f,"l\n");
+  constraintExpr_dump (lexpr, f);
+  fprintf(f,"r\n");
+  constraintExpr_dump (expr, f);
+}
+
+
+int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/
+{
+  fileloc loc1, loc2;
+
+  int ret;
+  
+  llassert(constraint_isDefined(*c1) );
+  llassert(constraint_isDefined(*c2) );
+
+  if (constraint_isUndefined(*c1) )
+    {
+        if (constraint_isUndefined(*c2) )
+	  return 0;
+	else
+	  return 1;
+    }
+
+  if (constraint_isUndefined(*c2) )
+    {
+      return -1;
+    }
+    
+  loc1 = constraint_getFileloc(*c1);
+  loc2 = constraint_getFileloc(*c2);
+
+  ret = fileloc_compare(loc1, loc2);
+
+  fileloc_free(loc1);
+  fileloc_free(loc2);
+    
+  return ret;
+}
+
+
+bool constraint_isPost  (/*@observer@*/ /*@temp@*/ constraint c)
+{
+  llassert(constraint_isDefined(c) );
+
+  if (constraint_isUndefined(c) )
+    return FALSE;
+  
+  return (c->post);
+}
+
+
+static int constraint_getDepth(/*@observer@*/ /*@temp@*/ constraint c)
+{
+  int l , r;
+
+  l = constraintExpr_getDepth(c->lexpr);
+  r = constraintExpr_getDepth(c->expr);
+
+  if (l > r)
+    {
+      DPRINTF(( message("constraint depth returning %d for %s", l, constraint_print(c) ) ));
+      return l;
+    }
+  else
+    {
+      DPRINTF(( message("constraint depth returning %d for %s", r, constraint_print(c) ) ));
+      return r;
+    }
+}
+
+
+bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
+{
+  int temp;
+
+  temp = constraint_getDepth(c);
+
+  if (temp >= 20 )
+    {
+      return TRUE;
+    }
+
+  return FALSE;
+  
+}