Fixed bug cause spurious bounds errors.

[splint.git] / src / constraint.c

diff --git a/src/constraint.c b/src/constraint.c
index 24596df56a1ef4810d35ba78871df9fce4b2f97f..71c3855093eade6be2c43f29475faf9a22e661a0 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -39,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);
 
@@ -119,14 +121,20 @@ constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r
     
   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);
 
@@ -314,7 +322,7 @@ bool constraint_hasMaxSet (constraint c)
   return FALSE;
 }
 
-constraint constraint_makeReadSafeExprNode (  exprNode po, exprNode ind)
+constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind)
 {
   constraint ret = constraint_makeNew ();
 
@@ -474,6 +482,7 @@ constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequenc
 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 {
   constraintExpr t1, t2;
+  constraint t3;
 
   t1 = constraintExpr_makeValueExpr (e1);
   t2 = constraintExpr_makeValueExpr (e2);
@@ -481,8 +490,11 @@ 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)
@@ -493,6 +505,7 @@ constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc
 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 {
   constraintExpr t1, t2;
+  constraint t3;
 
   t1 = constraintExpr_makeValueExpr (e1);
   t2 = constraintExpr_makeValueExpr (e2);
@@ -501,8 +514,11 @@ 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)
@@ -666,6 +682,12 @@ void constraint_printErrorPostCondition (constraint c, fileloc loc)
 
   temp = constraint_getFileloc (c);
 
+    
+  if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
+    {
+      string = cstring_replaceChar(string, '\n', ' ');
+    }
+  
   if (fileloc_isDefined (temp))
     {
       errorLoc = temp;
@@ -727,7 +749,14 @@ void constraint_printError (constraint c, fileloc loc)
       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);
@@ -814,7 +843,7 @@ cstring  constraint_printDetailed (constraint c)
 {
   cstring st = cstring_undefined;
   cstring temp = cstring_undefined;
-    cstring genExpr;
+  cstring genExpr;
   
   if (!c->post)
     {
@@ -962,7 +991,7 @@ constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exp
   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
 
   precondition->fcnPre = FALSE;
-  return precondition;
+  return constraint_simplify(precondition);
 }
 
 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/