X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/8ea5df88d4d589854cfd2cf734e203ce58da744d..909cf5eb75a37820d441f670ee02a6e0c42944fc:/src/exprNode.c

diff --git a/src/exprNode.c b/src/exprNode.c
index 7af8f10..f082ecd 100644
--- a/src/exprNode.c
+++ b/src/exprNode.c
@@ -5594,34 +5594,38 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
 	     status */
 	  
 	  if ((sRef_isPossiblyNullTerminated (e2->sref)) || (sRef_isNullTerminated(e2->sref))) {
-	    int val = (int) multiVal_forceInt (e1->val);
-	    
-	    /* Operator : + or += */
-	    if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) {
-	      if (sRef_getSize(e2->sref) >= val) {/* Incrementing the pointer by 
-						     val should not result in a 
-						     size < 0 (size = 0 is ok !) */
+	    if (multiVal_isDefined (e1->val)) 
+	      {
+		int val = (int) multiVal_forceInt (e1->val);
 		
-		sRef_setSize (ret->sref, sRef_getSize(e2->sref) - val);
+		/* Operator : + or += */
+		if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) {
+		  if (sRef_getSize(e2->sref) >= val) {/* Incrementing the pointer by 
+							 val should not result in a 
+							 size < 0 (size = 0 is ok !) */
+		    
+		    sRef_setSize (ret->sref, sRef_getSize(e2->sref) - val);
+		    
+		    if (sRef_getLen(e2->sref) == val) { /* i.e. the character at posn val is \0 */
+		      sRef_setNotNullTerminatedState(ret->sref);
+		      sRef_resetLen (ret->sref);
+		    } else {
+		      sRef_setNullTerminatedState(ret->sref);
+		      sRef_setLen (ret->sref, sRef_getLen(e2->sref) - val);
+		    }
+		  }
+		}
 		
-		if (sRef_getLen(e2->sref) == val) { /* i.e. the character at posn val is \0 */
-		  sRef_setNotNullTerminatedState(ret->sref);
-		  sRef_resetLen (ret->sref);
-		} else {
-		  sRef_setNullTerminatedState(ret->sref);
-		  sRef_setLen (ret->sref, sRef_getLen(e2->sref) - val);
+		/* Operator : - or -= */
+		if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) {
+		  if (sRef_getSize(e2->sref) >= 0) {
+		    sRef_setSize (ret->sref, sRef_getSize(e2->sref) + val);
+		    sRef_setLen (ret->sref, sRef_getLen(e2->sref) + val);
+		  }
 		}
 	      }
-	    }
-	    
-	    /* Operator : - or -= */
-	    if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) {
-	      if (sRef_getSize(e2->sref) >= 0) {
-		sRef_setSize (ret->sref, sRef_getSize(e2->sref) + val);
-		sRef_setLen (ret->sref, sRef_getLen(e2->sref) + val);
-	      }
-	    }
 	  }
+
 	  /* end modifications */
 	  
 	  sRef_setNullError (ret->sref);
@@ -11517,3 +11521,13 @@ exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
   dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints);
   return dst;
 }
+
+void exprNode_revealState (exprNode e)
+{
+  if (exprNode_isDefined (e)) {
+    llmsg (message ("%s: State of %s: %s", fileloc_unparse (exprNode_loc (e)), 
+		    exprNode_unparse (e), sRef_unparseFull (e->sref)));
+  } else {
+    llmsg (message ("%s: Reveal state undefined", fileloc_unparse (g_currentloc)));
+  }
+}