Fixed problem with loop guards in loop test effects. New test case

[splint.git] / src / constraint.c

diff --git a/src/constraint.c b/src/constraint.c
index 66ca75c5b79958a48e684fdd1aa3d017b5dcbd90..cb87d1025e6e0550d5eb06a81a7f2c6e60df90bf 100644 (file)
--- a/src/constraint.c
+++ b/src/constraint.c
@@ -17,8 +17,8 @@
 ** 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 information on splint: info@splint.org
+** To report a bug: splint-bug@splint.org
 ** For more information: http://www.splint.org
 */
 
@@ -29,7 +29,7 @@
 /* #define DEBUGPRINT 1 */
 
 # include <ctype.h> /* for isdigit */
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
 # include "basic.h"
 # include "cgrammar.h"
 # include "cgrammar_tokens.h"
@@ -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 ();
 
@@ -666,6 +674,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 +741,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);
@@ -744,7 +765,7 @@ void constraint_printError (constraint c, fileloc loc)
        }
     }
 
-  fileloc_free (errorLoc);
+  fileloc_free(errorLoc);
 }
 
 static cstring constraint_printDeep (constraint c)
@@ -752,7 +773,7 @@ static cstring constraint_printDeep (constraint c)
   cstring genExpr;
   cstring st = cstring_undefined;
 
-  st = constraint_print (c);
+  st = constraint_print(c);
   
   if (c->orig != constraint_undefined)
     {
@@ -814,7 +835,7 @@ cstring  constraint_printDetailed (constraint c)
 {
   cstring st = cstring_undefined;
   cstring temp = cstring_undefined;
-    cstring genExpr;
+  cstring genExpr;
   
   if (!c->post)
     {
@@ -940,6 +961,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)