]> andersk Git - splint.git/blobdiff - src/exprNode.c
Fixed problem with shadow parameters.
[splint.git] / src / exprNode.c
index 7af8f10720673667cff5194eda0aaf1dec27b751..f082ecda733ecb445a8eee13cd708d045be97a71 100644 (file)
@@ -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)));
+  }
+}
This page took 0.035826 seconds and 4 git commands to generate.