Fix tracker issue 1837229.

[splint.git] / src / constraintGeneration.c

diff --git a/src/constraintGeneration.c b/src/constraintGeneration.c
index aa8657e3c1defb39f152b2549a39f2e9a8faabe8..4d46ca178d36af0993c20c2cbd7aa4469ffd1b67 100644 (file)
--- a/src/constraintGeneration.c
+++ b/src/constraintGeneration.c
@@ -53,7 +53,7 @@ static constraintList exprNode_traverseFalseEnsuresConstraints (/*@temp@*/ exprN
 
 static void checkArgumentList (/*@out@*/ exprNode p_temp, exprNodeList p_arglist, fileloc p_sequencePoint) /*@modifies p_temp @*/;
 
-static  constraintList checkCall (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist);
+static constraintList checkCall (/*@temp@*/ exprNode p_fcn, exprNodeList p_arglist);
 
 static bool exprNode_isUnhandled (/*@temp@*/ /*@observer@*/ exprNode e)
 {
@@ -155,7 +155,6 @@ static void exprNode_stmt (/*@temp@*/ exprNode e)
 {
   exprNode snode;
   fileloc loc;
-  //! cstring s;
   
   DPRINTF (("Generating constraint for: %s", exprNode_unparse (e)));
 
@@ -850,7 +849,7 @@ void exprNode_multiStatement (/*@dependent@*/ exprNode e)
   constraintList temp;
 
   DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse(e),
-                   fileloc_unparse(exprNode_getfileloc(e)))));
+                   fileloc_unparse(exprNode_getNextSequencePoint(e)))));
   
   if (exprNode_handleError (e))
     {
@@ -1337,7 +1336,7 @@ void exprNode_exprTraverse (/*@dependent@*/ exprNode e,
       
       fcn->requiresConstraints = 
        constraintList_addListFree (fcn->requiresConstraints,
-                                   checkCall (fcn, exprData_getArgs (data) ));      
+                                   checkCall (fcn, exprData_getArgs (data)));      
       
       fcn->ensuresConstraints = 
        constraintList_addListFree (fcn->ensuresConstraints,
@@ -1429,6 +1428,10 @@ void exprNode_exprTraverse (/*@dependent@*/ exprNode e,
        {
          break;
        }
+      else if (lltok_isPlus_Op (tok))
+       {
+         break;
+       }
       else if (lltok_isExcl_Op (tok))
        {
          break;
@@ -2213,7 +2216,7 @@ we'll include it in a production release when its stable...
       rt =  ctype_realType (ct);
       
       if (ctype_isStruct (rt))
-       TPRINTF((message("Found structure %s", exprNode_unparse(expr))
+       DPRINTF((message("Found structure %s", exprNode_unparse(expr))
                 ));
       if (hasInvariants(ct))
        {
@@ -2222,13 +2225,13 @@ we'll include it in a production release when its stable...
          invars = getInvariants(ct);
 
 
-         TPRINTF((message ("findStructs has invariants %s ", constraintList_unparse (invars))
+         DPRINTF((message ("findStructs has invariants %s ", constraintList_unparse (invars))
                   ));
          
          invars = constraintList_doSRefFixStructConstraint(invars, exprNode_getSref(expr), ct);
 
          
-         TPRINTF((message ("findStructs finded invariants to be %s ", constraintList_unparse (invars))
+         DPRINTF((message ("findStructs finded invariants to be %s ", constraintList_unparse (invars))
                   ));
        }
     }
@@ -2260,23 +2263,23 @@ constraintList checkCall (/*@dependent@*/ exprNode fcn, exprNodeList arglist)
        preconditions = constraintList_makeNew();
     }
   
-  if (context_getFlag (FLG_IMPLICTCONSTRAINT) )
+  if (context_getFlag (FLG_IMPBOUNDSCONSTRAINTS))
     {
 
       /*
       uentryList_elements (arglist, el)
        {
          sRef s;
-         TPRINTF((message("setImplictfcnConstraints doing: %s", uentry_unparse(el) ) ));
+         DPRINTF((message("setImplicitfcnConstraints doing: %s", uentry_unparse(el) ) ));
          
          s = uentry_getSref(el);
          if (sRef_isReference (s) )
            {
-             TPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
+             DPRINTF((message ("%s is a pointer", sRef_unparse(s) ) ));
            }
          else
            {
-             TPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
+             DPRINTF((message ("%s is NOT a pointer", sRef_unparse(s) ) ));
            }
          //drl 4/26/01
          //chagned this from MaxSet(s) == 0 to MaxSet(s) >= 0