X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/15b3d2b27a3dce7a3b65e88fb0d1732e235117f4..35e063d82040a7c7a6da8634cf377e19ee0662d1:/src/constraint.c

diff --git a/src/constraint.c b/src/constraint.c
index 82ab08b..71c3855 100644
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -1,11 +1,35 @@
+/*
+** 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
+*/
+
 /*
 ** constraint.c
 */
 
-//#define DEBUGPRINT 1
+/* #define DEBUGPRINT 1 */
 
 # include <ctype.h> /* for isdigit */
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
 # include "basic.h"
 # include "cgrammar.h"
 # include "cgrammar_tokens.h"
@@ -15,8 +39,10 @@
 
 /*@i33*/
 
-/*@access exprNode @*/
-
+/*@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! */
 
 static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
 
@@ -25,43 +51,6 @@ 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)
 {
@@ -75,7 +64,7 @@ static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode
   int c;
   constraint ret;
   ret = constraint_makeNew ();
-  llassert (constraintExpr_isDefined(l) );
+  llassert (constraintExpr_isDefined (l));
       
   ret->lexpr = constraintExpr_copy (l);
 
@@ -87,17 +76,16 @@ static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode
   else if (relOp.tok == EQ_OP)
     ret->ar = EQ;
   else
-  llfatalbug(message("Unsupported relational operator") );
+  llfatalbug (message ("Unsupported relational operator"));
 
 
-  t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
-  c = atoi( t );
+  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) ) ) );
+  DPRINTF (("GENERATED CONSTRAINT:"));
+  DPRINTF ((message ("%s", constraint_print (ret))));
   return ret;
 }
 # endif
@@ -112,12 +100,12 @@ bool constraint_same (constraint c1, constraint c2)
       return FALSE;
     }
   
-  if (!constraintExpr_similar (c1->lexpr, c2->lexpr) )
+  if (!constraintExpr_similar (c1->lexpr, c2->lexpr))
     {
       return FALSE;
     }
 
-  if (!constraintExpr_similar (c1->expr, c2->expr) )
+  if (!constraintExpr_similar (c1->expr, c2->expr))
     {
       return FALSE;
     }
@@ -128,31 +116,37 @@ bool constraint_same (constraint c1, constraint c2)
 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)     
 {
   constraint ret;
-  ret = constraint_makeNew();
-  llassert (constraintExpr_isDefined(l) );
+  ret = constraint_makeNew ();
+  llassert (constraintExpr_isDefined (l));
     
   ret->lexpr = constraintExpr_copy (l);
 
-  if (relOp.tok == GE_OP)
+  if (lltok_getTok (relOp) == GE_OP)
+    {
       ret->ar = GTE;
-  else if (relOp.tok == LE_OP)
-    ret->ar = LTE;
-  else if (relOp.tok == EQ_OP)
-    ret->ar = EQ;
+    }
+  else if (lltok_getTok (relOp) == LE_OP)
+    {
+      ret->ar = LTE;
+    }
+  else if (lltok_getTok (relOp) == EQ_OP)
+    {
+      ret->ar = EQ;
+    }
   else
-  llfatalbug( message("Unsupported relational operator") );
+    llfatalbug ( message ("Unsupported relational operator"));
 
   ret->expr = constraintExpr_copy (r);
 
   ret->post = TRUE;
 
-  ret->orig = constraint_copy(ret);
+  ret->orig = constraint_copy (ret);
 
   ret = constraint_simplify (ret);
-  
-  //  ret->orig = ret;
-  DPRINTF(("GENERATED CONSTRAINT:"));
-  DPRINTF( (message ("%s", constraint_print(ret) ) ) );
+  /* ret->orig = ret; */
+
+  DPRINTF (("GENERATED CONSTRAINT:"));
+  DPRINTF ((message ("%s", constraint_print (ret))));
   return ret;
 }
 
@@ -160,10 +154,9 @@ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
 {
   constraint ret;
 
-  llassert (constraint_isDefined(c) );
-  // DPRINTF((message("Copying constraint %q", constraint_print) ));
-  
-  ret = constraint_makeNew();
+  llassert (constraint_isDefined (c));
+
+  ret = constraint_makeNew ();
   ret->lexpr = constraintExpr_copy (c->lexpr);
   ret->ar = c->ar;
   ret->expr =  constraintExpr_copy (c->expr);
@@ -192,15 +185,15 @@ constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
 
 void constraint_overWrite (constraint c1, constraint c2) 
 {
-  llassert (constraint_isDefined(c1) );
+  llassert (constraint_isDefined (c1));
 
   llassert (c1 != c2);
 
-  DPRINTF((message("OverWriteing constraint %q with %q", constraint_print(c1),
-		   constraint_print(c2) ) ));
+  DPRINTF ((message ("OverWriteing constraint %q with %q", constraint_print (c1),
+		   constraint_print (c2))));
   
-  constraintExpr_free(c1->lexpr);
-  constraintExpr_free(c1->expr);
+  constraintExpr_free (c1->lexpr);
+  constraintExpr_free (c1->expr);
   
   c1->lexpr = constraintExpr_copy (c2->lexpr);
   c1->ar = c2->ar;
@@ -238,7 +231,7 @@ static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
      /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
 {
   constraint ret;
-  ret = dmalloc(sizeof (*ret) );
+  ret = dmalloc (sizeof (*ret));
   ret->lexpr = NULL;
   ret->expr = NULL;
   ret->ar = LT;
@@ -256,11 +249,11 @@ constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed
   if (c->generatingExpr == NULL)
     {
       c->generatingExpr = e;
-      DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(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) )  ));
+      DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print (c), exprNode_unparse (e)) ));
     }
   return c;
 }
@@ -270,16 +263,16 @@ constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNo
 
   if (c->orig != constraint_undefined)
     {
-      c->orig = constraint_addGeneratingExpr(c->orig, e);
+      c->orig = constraint_addGeneratingExpr (c->orig, e);
     }
   else
     {
-      DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
+      DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print (c), exprNode_unparse (e)) ));
     }
   return c;
 }
 
-constraint constraint_setFcnPre (/*@returned@*/ constraint c )
+constraint constraint_setFcnPre (/*@returned@*/ constraint c)
 {
 
   if (c->orig != constraint_undefined)
@@ -289,7 +282,7 @@ constraint constraint_setFcnPre (/*@returned@*/ constraint c )
   else
     {
       c->fcnPre = TRUE;
-      //      DPRINTF(( message("Warning Setting fcnPre directly") ));
+      DPRINTF (( message ("Warning Setting fcnPre directly")));
     }
   return c;
 }
@@ -299,43 +292,43 @@ constraint constraint_setFcnPre (/*@returned@*/ constraint c )
 
 fileloc constraint_getFileloc (constraint c)
 {
-  if (exprNode_isDefined(c->generatingExpr) )
-    return (fileloc_copy (exprNode_getfileloc (c->generatingExpr) ) );
+  if (exprNode_isDefined (c->generatingExpr))
+    return (fileloc_copy (exprNode_getfileloc (c->generatingExpr)));
 	    
-  return (constraintExpr_getFileloc (c->lexpr) );
+  return (constraintExpr_getFileloc (c->lexpr));
 
 
 }
 
 static bool checkForMaxSet (constraint c)
 {
-  if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
+  if (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr))
     return TRUE;
 
   return FALSE;
 }
 
-bool constraint_hasMaxSet(constraint c)
+bool constraint_hasMaxSet (constraint c)
 {
-  if (checkForMaxSet(c) )
+  if (checkForMaxSet (c))
     return TRUE;
   
   if (c->orig != NULL)
     {
-      if (checkForMaxSet(c->orig) )
+      if (checkForMaxSet (c->orig))
 	return TRUE;
     }
 
   return FALSE;
 }
 
-constraint constraint_makeReadSafeExprNode (  exprNode po, exprNode ind)
+constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind)
 {
-  constraint ret = constraint_makeNew();
-  //  constraintTerm term;
+  constraint ret = constraint_makeNew ();
+
   po = po;
   ind = ind;
-  ret->lexpr = constraintExpr_makeMaxReadExpr(po);
+  ret->lexpr = constraintExpr_makeMaxReadExpr (po);
   ret->ar    = GTE;
   ret->expr  = constraintExpr_makeValueExpr (ind);
   ret->post = FALSE;
@@ -344,10 +337,10 @@ constraint constraint_makeReadSafeExprNode (  exprNode po, exprNode ind)
 
 constraint constraint_makeWriteSafeInt (   exprNode po, int ind)
 {
-  constraint ret = constraint_makeNew();
+  constraint ret = constraint_makeNew ();
 
  
-  ret->lexpr =constraintExpr_makeMaxSetExpr(po);
+  ret->lexpr =constraintExpr_makeMaxSetExpr (po);
   ret->ar = GTE;
   ret->expr =  constraintExpr_makeIntLiteral (ind);
   /*@i1*/return ret;
@@ -355,7 +348,7 @@ constraint constraint_makeWriteSafeInt (   exprNode po, int ind)
 
 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
 {
- constraint ret = constraint_makeNew();
+ constraint ret = constraint_makeNew ();
  ret->lexpr = constraintExpr_makeSRefMaxset (s);
  ret->ar = EQ;
  ret->expr =  constraintExpr_makeIntLiteral ((int)size);
@@ -365,10 +358,10 @@ constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
 
 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
 {
-  constraint ret = constraint_makeNew();
+  constraint ret = constraint_makeNew ();
 
  
-  ret->lexpr = constraintExpr_makeSRefMaxset ( s );
+  ret->lexpr = constraintExpr_makeSRefMaxset ( s);
   ret->ar = GTE;
   ret->expr =  constraintExpr_makeIntLiteral (ind);
   ret->post = TRUE;
@@ -377,25 +370,25 @@ constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
 
 /* drl added 01/12/2000
    
-  makes the constraint: Ensures index <= MaxRead(buffer) */
+  makes the constraint: Ensures index <= MaxRead (buffer) */
 
-constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
+constraint constraint_makeEnsureLteMaxRead (exprNode index, exprNode buffer)
 {
-  constraint ret = constraint_makeNew();
+  constraint ret = constraint_makeNew ();
 
   ret->lexpr = constraintExpr_makeValueExpr (index);
   ret->ar = LTE;
-  ret->expr = constraintExpr_makeMaxReadExpr(buffer);
+  ret->expr = constraintExpr_makeMaxReadExpr (buffer);
   ret->post = TRUE;
   return ret;
 }
 
 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 {
-  constraint ret = constraint_makeNew();
+  constraint ret = constraint_makeNew ();
 
  
-  ret->lexpr =constraintExpr_makeMaxSetExpr(po);
+  ret->lexpr =constraintExpr_makeMaxSetExpr (po);
   ret->ar = GTE;
   ret->expr =  constraintExpr_makeValueExpr (ind);
   /*@i1*/return ret;
@@ -404,9 +397,9 @@ constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 
 constraint constraint_makeReadSafeInt ( exprNode t1, int index)
 {
-  constraint ret = constraint_makeNew();
+  constraint ret = constraint_makeNew ();
 
-  ret->lexpr = constraintExpr_makeMaxReadExpr(t1);
+  ret->lexpr = constraintExpr_makeMaxReadExpr (t1);
   ret->ar    = GTE;
   ret->expr  = constraintExpr_makeIntLiteral (index);
   ret->post = FALSE;
@@ -415,10 +408,10 @@ constraint constraint_makeReadSafeInt ( exprNode t1, int index)
 
 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
 {
-  constraint ret = constraint_makeNew();
+  constraint ret = constraint_makeNew ();
 
  
-  ret->lexpr = constraintExpr_makeSRefMaxRead (s );
+  ret->lexpr = constraintExpr_makeSRefMaxRead (s);
   ret->ar = GTE;
   ret->expr =  constraintExpr_makeIntLiteral (ind);
   ret->post = TRUE;
@@ -429,13 +422,10 @@ constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, filelo
 {
   constraint ret;
   
-  ret = constraint_makeReadSafeExprNode(t1, 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;
 }
 
@@ -444,10 +434,9 @@ static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintE
 
   constraint ret;
   
-  llassert(constraintExpr_isDefined(c1) && constraintExpr_isDefined(c2) );
-  //  llassert(sequencePoint);
+  llassert (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2));
 
-  ret = constraint_makeNew();
+  ret = constraint_makeNew ();
   
   ret->lexpr = c1;
   ret->ar = ar;
@@ -463,15 +452,13 @@ static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@depe
   constraint ret;
   exprNode e;
 
-  if (! (exprNode_isDefined(e1) && exprNode_isDefined(e2) ) )
+  if (! (exprNode_isDefined (e1) && exprNode_isDefined (e2)))
     {
-      llcontbug((message("null exprNode, Exprnodes are %s and %s",
-		       exprNode_unparse(e1), exprNode_unparse(e2) )
-	       ));
+      llcontbug ((message ("null exprNode, Exprnodes are %s and %s",
+		       exprNode_unparse (e1), exprNode_unparse (e2))
+		));
     }
 
-  //  llassert (sequencePoint);
-  
   e  =  e1;
   c1 =  constraintExpr_makeValueExpr (e);
   
@@ -488,13 +475,14 @@ static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@depe
 
 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 {
-  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
+  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
 }
 
 /*make constraint ensures e1 < e2 */
 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 {
   constraintExpr t1, t2;
+  constraint t3;
 
   t1 = constraintExpr_makeValueExpr (e1);
   t2 = constraintExpr_makeValueExpr (e2);
@@ -502,18 +490,22 @@ constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequ
   /*change this to e1 <= (e2 -1) */
 
   t2 = constraintExpr_makeDecConstraintExpr (t2);
-  
- return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
+
+  t3 =  constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE);
+
+  t3 = constraint_simplify(t3);
+  return (t3);
 }
 
 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 {
- return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE));
 }
 
 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 {
   constraintExpr t1, t2;
+  constraint t3;
 
   t1 = constraintExpr_makeValueExpr (e1);
   t2 = constraintExpr_makeValueExpr (e2);
@@ -522,27 +514,30 @@ constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc s
   /* change this to e1 >= (e2 + 1) */
   t2 = constraintExpr_makeIncConstraintExpr (t2);
   
+  t3 =  constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE);
+
+  t3 = constraint_simplify(t3);
   
- return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
+  return t3;
 }
 
 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 {
- return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
+ return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE));
 }
 
 
 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
 {
-  constraintList_free(dst->ensuresConstraints);
-  constraintList_free(dst->requiresConstraints);
-  constraintList_free(dst->trueEnsuresConstraints);
-  constraintList_free(dst->falseEnsuresConstraints);
+  constraintList_free (dst->ensuresConstraints);
+  constraintList_free (dst->requiresConstraints);
+  constraintList_free (dst->trueEnsuresConstraints);
+  constraintList_free (dst->falseEnsuresConstraints);
   
-  dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
-  dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
-  dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
-  dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
+  dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints);
+  dst->requiresConstraints = constraintList_copy (src->requiresConstraints);
+  dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints);
+  dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints);
   return dst;
 }
 
@@ -552,10 +547,10 @@ constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoi
   constraintExpr x1, x2, y;
   constraint ret;
 
-  ret = constraint_makeNew();
+  ret = constraint_makeNew ();
 
   x1 =  constraintExpr_makeValueExpr (e);
-  x2 =  constraintExpr_copy(x1);
+  x2 =  constraintExpr_copy (x1);
   y  =  constraintExpr_makeValueExpr (f);
 
   ret->lexpr = x1;
@@ -575,10 +570,10 @@ constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequen
   constraintExpr x1, x2, y;
   constraint ret;
 
-  ret = constraint_makeNew();
+  ret = constraint_makeNew ();
 
   x1 =  constraintExpr_makeValueExpr (e);
-  x2 =  constraintExpr_copy(x1);
+  x2 =  constraintExpr_copy (x1);
   y  =  constraintExpr_makeValueExpr (f);
 
   ret->lexpr = x1;
@@ -593,27 +588,20 @@ constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequen
 
 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
 {
-  constraint ret = constraint_makeNew();
-  //constraintTerm term;
+  constraint ret = constraint_makeNew ();
 
-  //  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;
+  constraint ret = constraint_makeNew ();
 
-  //  e = exprNode_fakeCopy(e);
   ret->lexpr = constraintExpr_makeValueExpr (e);
   ret->ar = EQ;
   ret->post = TRUE;
@@ -621,25 +609,23 @@ 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@*/ constraint c)
 {
-  llassert(constraint_isDefined (c) );
+  llassert (constraint_isDefined (c));
 
 
-  if (constraint_isDefined(c->orig) )
+  if (constraint_isDefined (c->orig))
     constraint_free (c->orig);
-  if ( constraint_isDefined(c->or) )
+  if ( constraint_isDefined (c->or))
     constraint_free (c->or);
 
   
-  constraintExpr_free(c->lexpr);
-  constraintExpr_free(c->expr);
+  constraintExpr_free (c->lexpr);
+  constraintExpr_free (c->expr);
 
   c->orig = NULL;
   c->or = NULL;
@@ -650,22 +636,6 @@ void constraint_free (/*@only@*/ 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;
@@ -693,7 +663,7 @@ cstring arithType_print (arithType ar) /*@*/
       st = cstring_makeLiteral ("POSITIVE");
       break;
     default:
-      llassert(FALSE);
+      llassert (FALSE);
       break;
     }
   return st;
@@ -710,13 +680,19 @@ void constraint_printErrorPostCondition (constraint c, fileloc loc)
 
   loc = NULL;
 
-  temp = constraint_getFileloc(c);
+  temp = constraint_getFileloc (c);
 
-  if (fileloc_isDefined(temp) )
+    
+  if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
+    {
+      string = cstring_replaceChar(string, '\n', ' ');
+    }
+  
+  if (fileloc_isDefined (temp))
     {
       errorLoc = temp;
       voptgenerror (  FLG_CHECKPOST, string, errorLoc);
-      fileloc_free(temp);
+      fileloc_free (temp);
     }
   else
     {
@@ -730,13 +706,13 @@ cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
   cstring string, ret;
   fileloc errorLoc;
   
-  string = constraint_print(c);
+  string = constraint_print (c);
 
-  errorLoc = constraint_getFileloc(c);
+  errorLoc = constraint_getFileloc (c);
 
-  ret = message ("constraint: %q @ %q", string, fileloc_unparse(errorLoc) );
+  ret = message ("constraint: %q @ %q", string, fileloc_unparse (errorLoc));
 
-  fileloc_free(errorLoc);
+  fileloc_free (errorLoc);
   return ret;
 
 }
@@ -747,75 +723,92 @@ 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;
 
-  temp = constraint_getFileloc(c);
+  temp = constraint_getFileloc (c);
 
-  if (fileloc_isDefined(temp) )
+  if (fileloc_isDefined (temp))
     {
       errorLoc = temp;
     }
   else
     {
-      llassert(FALSE);
-      DPRINTF (("constraint %s had undefined fileloc %s", constraint_print(c), fileloc_unparse(temp)));
-      fileloc_free(temp);
-      errorLoc = fileloc_copy(errorLoc);
+      llassert (FALSE);
+      DPRINTF (("constraint %s had undefined fileloc %s", constraint_print (c), fileloc_unparse (temp)));
+      fileloc_free (temp);
+      errorLoc = fileloc_copy (errorLoc);
     }
-      
+
+  
+  if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
+    {
+      string = cstring_replaceChar(string, '\n', ' ');
+    }
+
+
   if (c->post)
     {
       voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
     }
   else
     {
-      if (constraint_hasMaxSet (c) )
-	voptgenerror (FLG_ARRAYBOUNDS, string, errorLoc);
+      if (constraint_hasMaxSet (c))
+	{
+	  voptgenerror (FLG_BOUNDSWRITE, string, errorLoc);
+	}
       else
-	voptgenerror (FLG_ARRAYBOUNDSREAD, string, errorLoc);
+	{
+	  voptgenerror (FLG_BOUNDSREAD, string, errorLoc);
+	}
     }
 
   fileloc_free(errorLoc);
-
 }
 
-
 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);
+      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", genExpr, 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 precondition:\n%q",
-						constraint_printDeep(c->orig) )
-					) );
-	  
+	    {
+	      st = cstring_concatFree (st, message (" needed to satisfy precondition:\n%q",
+						   constraint_printDeep (c->orig)));
+	    }
 	}
       else
 	{
-	  st = cstring_concatFree(st,(message("derived from: %q",
-					      constraint_printDeep(c->orig) )
-				      ) );
+	  st = cstring_concatFree (st, message ("derived from: %q",
+					       constraint_printDeep (c->orig)));
 	}
     }
 
   return st;  
-
 }
 
 
@@ -824,19 +817,20 @@ static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/
   cstring st = cstring_undefined;
   cstring genExpr;
   
-  st = message ("Unsatisfied ensures constraint condition:\nLCLint is unable to verify the constraint %q", constraint_printDeep (c) );
+  st = message ("Unsatisfied ensures constraint condition:\nSplint is unable to verify the constraint %q", constraint_printDeep (c));
 
   genExpr = exprNode_unparse (c->generatingExpr);
     
-  if (context_getFlag (FLG_CONSTRAINTLOCATION) )
+  if (context_getFlag (FLG_CONSTRAINTLOCATION))
     {
       cstring temp;
-      // llassert (c->generatingExpr);
-      temp = message ("\nOriginal Generating expression %q: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
-		      genExpr );
+
+      temp = message ("\nOriginal Generating expression %q: %s\n", 
+		      fileloc_unparse ( exprNode_getfileloc (c->generatingExpr)),
+		      genExpr);
       st = cstring_concatFree (st, temp);
 
-      if (constraint_hasMaxSet(c) )
+      if (constraint_hasMaxSet (c))
 	{
 	  temp = message ("Has MaxSet\n");
 	  st = cstring_concatFree (st, temp);
@@ -849,36 +843,36 @@ cstring  constraint_printDetailed (constraint c)
 {
   cstring st = cstring_undefined;
   cstring temp = cstring_undefined;
-    cstring genExpr;
+  cstring genExpr;
   
   if (!c->post)
     {
-      st = message ("Unable to resolve constraint:\n%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) );
+      st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c));
     }
 
-  if (constraint_hasMaxSet(c) )
+  if (constraint_hasMaxSet (c))
     {
-      temp = cstring_makeLiteral("Possible out-of-bounds store:\n");
+      temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
     }
   else
     {
-      temp = cstring_makeLiteral("Possible out-of-bounds read:\n");
+      temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
     }
   
   genExpr = exprNode_unparse (c->generatingExpr);
   
-  if (context_getFlag (FLG_CONSTRAINTLOCATION) )
+  if (context_getFlag (FLG_CONSTRAINTLOCATION))
     {
       cstring temp2;
-      temp2 = message ("%s\n", genExpr );
+      temp2 = message ("%s\n", genExpr);
       temp = cstring_concatFree (temp, temp2);
     }
 
-  st  = cstring_concatFree(temp,st);
+  st  = cstring_concatFree (temp,st);
   
   return st;
 }
@@ -890,7 +884,7 @@ cstring  constraint_printDetailed (constraint c)
   llassert (c !=NULL);
   if (c->post)
     {
-      if (context_getFlag (FLG_PARENCONSTRAINT) )
+      if (context_getFlag (FLG_PARENCONSTRAINT))
 	{
 	  type = cstring_makeLiteral ("ensures: ");
 	}
@@ -901,7 +895,7 @@ cstring  constraint_printDetailed (constraint c)
     }
   else
     {
-      if (context_getFlag (FLG_PARENCONSTRAINT) )
+      if (context_getFlag (FLG_PARENCONSTRAINT))
 	{
 	  type = cstring_makeLiteral ("requires: ");
 	}
@@ -911,13 +905,13 @@ cstring  constraint_printDetailed (constraint c)
 	}
 	
     }
-      if (context_getFlag (FLG_PARENCONSTRAINT) )
+      if (context_getFlag (FLG_PARENCONSTRAINT))
 	{
 	  st = message ("%q: %q %q %q",
 			type,
 			constraintExpr_print (c->lexpr),
-			arithType_print(c->ar),
-			constraintExpr_print(c->expr)
+			arithType_print (c->ar),
+			constraintExpr_print (c->expr)
 			);
 	}
       else
@@ -925,8 +919,8 @@ cstring  constraint_printDetailed (constraint c)
 	  st = message ("%q %q %q %q",
 			type,
 			constraintExpr_print (c->lexpr),
-			arithType_print(c->ar),
-			constraintExpr_print(c->expr)
+			arithType_print (c->ar),
+			constraintExpr_print (c->expr)
 		);
 	}
   return st;
@@ -940,14 +934,14 @@ cstring  constraint_printOr (constraint c) /*@*/
   ret = cstring_undefined;
   temp = c;
 
-  ret = cstring_concatFree (ret, constraint_print(temp) );
+  ret = cstring_concatFree (ret, constraint_print (temp));
 
   temp = temp->or;
   
-  while ( constraint_isDefined(temp) ) 
+  while ( constraint_isDefined (temp)) 
     {
-      ret = cstring_concatFree (ret, cstring_makeLiteral (" OR ") );
-      ret = cstring_concatFree (ret, constraint_print(temp) );
+      ret = cstring_concatFree (ret, cstring_makeLiteral (" OR "));
+      ret = cstring_concatFree (ret, constraint_print (temp));
       temp = temp->or;
     }
 
@@ -975,6 +969,18 @@ constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exp
 
   return postcondition;
 }
+/*Commenting out temporally
+  
+/ *@only@* /constraint  constraint_doSRefFixInvarConstraint(constraint invar, sRef s, ctype ct )
+{
+
+  invar = constraint_copy (invar);
+  invar->lexpr = constraintExpr_doSRefFixInvarConstraint (invar->lexpr, s, ct);
+  invar->expr = constraintExpr_doSRefFixInvarConstraint (invar->expr, s, ct);
+
+  return invar;
+}
+*/
 
 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
 						   exprNodeList arglist)
@@ -985,26 +991,13 @@ constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exp
   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
 
   precondition->fcnPre = FALSE;
-  return precondition;
+  return constraint_simplify(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 @*/
 {
 
-  DPRINTF( (message("Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
+  DPRINTF ((message ("Doing constraint_preserverOrig for %q ", constraint_printDetailed (c))));
   
   if (c->orig == constraint_undefined)
     c->orig = constraint_copy (c);
@@ -1025,18 +1018,18 @@ constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @
 	}
       else
 	{
-	  llcontbug((message("Expected c->orig->orig to be null" ) ));
-	  constraint_free(c->orig->orig);
+	  llcontbug ((message ("Expected c->orig->orig to be null")));
+	  constraint_free (c->orig->orig);
 	  c->orig->orig = temp;
 	  temp = NULL;
 	}
     }
   else
     {
-      DPRINTF( (message("Not changing constraint") ));
+      DPRINTF ((message ("Not changing constraint")));
     }
   
-  DPRINTF( (message("After Doing constraint_preserverOrig for %q ", constraint_printDetailed(c) ) ));
+  DPRINTF ((message ("After Doing constraint_preserverOrig for %q ", constraint_printDetailed (c))));
 
   return c;
 }
@@ -1054,11 +1047,11 @@ constraint constraint_togglePost (/*@returned@*/ constraint c)
 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
 {
   if (c->orig != NULL)
-    c->orig = constraint_togglePost(c->orig);
+    c->orig = constraint_togglePost (c->orig);
   return c;
 }
 
-bool constraint_hasOrig( /*@observer@*/ /*@temp@*/ constraint c)
+bool constraint_hasOrig ( /*@observer@*/ /*@temp@*/ constraint c)
 {
   if (c->orig == NULL)
     return FALSE;
@@ -1082,32 +1075,30 @@ constraint constraint_undump (FILE *f)
 
   char *os;
 
-  s = mstring_create (MAX_DUMP_LINE_LENGTH);
+  os = mstring_create (MAX_DUMP_LINE_LENGTH);
 
-  os = s;
-  
-  s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+  s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 
   /*@i33*/ /*this should probably be wrappered...*/
   
   fcnPre = (bool) reader_getInt (&s);
-  advanceField(&s);
+  advanceField (&s);
   post = (bool) reader_getInt (&s);
-  advanceField(&s);
+  advanceField (&s);
   ar = (arithType) reader_getInt (&s);
 
-  s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+  s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 
   reader_checkChar (&s, 'l');
 
   lexpr = constraintExpr_undump (f);
 
-  s = fgets(os, MAX_DUMP_LINE_LENGTH, f);
+  s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 
   reader_checkChar (&s, 'r');
   expr = constraintExpr_undump (f);
 
-  c = constraint_makeNew();
+  c = constraint_makeNew ();
   
   c->fcnPre = fcnPre; 
   c->post = post;
@@ -1116,8 +1107,8 @@ constraint constraint_undump (FILE *f)
   c->lexpr = lexpr;
   c->expr =  expr;
 
-  free(os);
-  c = constraint_preserveOrig(c);
+  free (os);
+  c = constraint_preserveOrig (c);
   return c;
 }
 
@@ -1138,10 +1129,10 @@ void constraint_dump (/*@observer@*/ constraint c,  FILE *f)
   lexpr = c->lexpr;
   expr = c->expr;
   
-  fprintf(f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
-  fprintf(f,"l\n");
+  fprintf (f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
+  fprintf (f,"l\n");
   constraintExpr_dump (lexpr, f);
-  fprintf(f,"r\n");
+  fprintf (f,"r\n");
   constraintExpr_dump (expr, f);
 }
 
@@ -1152,29 +1143,29 @@ int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@obse
 
   int ret;
   
-  llassert(constraint_isDefined(*c1) );
-  llassert(constraint_isDefined(*c2) );
+  llassert (constraint_isDefined (*c1));
+  llassert (constraint_isDefined (*c2));
 
-  if (constraint_isUndefined(*c1) )
+  if (constraint_isUndefined (*c1))
     {
-        if (constraint_isUndefined(*c2) )
+        if (constraint_isUndefined (*c2))
 	  return 0;
 	else
 	  return 1;
     }
 
-  if (constraint_isUndefined(*c2) )
+  if (constraint_isUndefined (*c2))
     {
       return -1;
     }
     
-  loc1 = constraint_getFileloc(*c1);
-  loc2 = constraint_getFileloc(*c2);
+  loc1 = constraint_getFileloc (*c1);
+  loc2 = constraint_getFileloc (*c2);
 
-  ret = fileloc_compare(loc1, loc2);
+  ret = fileloc_compare (loc1, loc2);
 
-  fileloc_free(loc1);
-  fileloc_free(loc2);
+  fileloc_free (loc1);
+  fileloc_free (loc2);
     
   return ret;
 }
@@ -1182,30 +1173,30 @@ int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@obse
 
 bool constraint_isPost  (/*@observer@*/ /*@temp@*/ constraint c)
 {
-  llassert(constraint_isDefined(c) );
+  llassert (constraint_isDefined (c));
 
-  if (constraint_isUndefined(c) )
+  if (constraint_isUndefined (c))
     return FALSE;
   
   return (c->post);
 }
 
 
-static int constraint_getDepth(/*@observer@*/ /*@temp@*/ constraint c)
+static int constraint_getDepth (/*@observer@*/ /*@temp@*/ constraint c)
 {
   int l , r;
 
-  l = constraintExpr_getDepth(c->lexpr);
-  r = constraintExpr_getDepth(c->expr);
+  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) ) ));
+      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) ) ));
+      DPRINTF (( message ("constraint depth returning %d for %s", r, constraint_print (c))));
       return r;
     }
 }
@@ -1215,9 +1206,9 @@ bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
 {
   int temp;
 
-  temp = constraint_getDepth(c);
+  temp = constraint_getDepth (c);
 
-  if (temp >= 20 )
+  if (temp >= 20)              
     {
       return TRUE;
     }