X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/346fab44f091e9870a7319f99c824bd0de3d71d1..acfb6ad9a989e335242f8ea98940827e213228b4:/src/exprNode.c

diff --git a/src/exprNode.c b/src/exprNode.c
index 4f36072..3f1260e 100644
--- a/src/exprNode.c
+++ b/src/exprNode.c
@@ -105,16 +105,20 @@ static ctype ctypeType;
 static ctype filelocType; 
 static bool initMod = FALSE;
 
-static void exprNode_defineConstraints(/*@sef@*/ /*@special@*/ /*@notnull@*/ exprNode p_e)
-     /*@defines p_e->requiresConstraints,  p_e->ensuresConstraints,  p_e->trueEnsuresConstraints,  p_e->falseEnsuresConstraints @*/
-     ;
-     
-# define exprNode_defineConstraints(e)  \
-do{					  (e)->requiresConstraints = constraintList_makeNew(); \
-					  (e)->ensuresConstraints = constraintList_makeNew(); \
-					  (e)->trueEnsuresConstraints = constraintList_makeNew(); \
-					    (e)->falseEnsuresConstraints = constraintList_makeNew(); } while(FALSE)
+/*@function void exprNode_swap (sef exprNode, sef exprNode)@*/
+/*@-macroassign@*/
+# define exprNode_swap(e1,e2) do { exprNode m_tmp = (e1); (e1) = (e2); (e2) = m_tmp; } while (FALSE)
+/*@=macroassign@*/
 
+static void exprNode_defineConstraints(/*@sef@*/ /*@special@*/ /*@notnull@*/ exprNode e)
+   /*@defines e->requiresConstraints,  e->ensuresConstraints, 
+              e->trueEnsuresConstraints,  e->falseEnsuresConstraints @*/ 
+{
+  e->requiresConstraints = constraintList_makeNew (); 
+  e->ensuresConstraints = constraintList_makeNew (); 
+  e->trueEnsuresConstraints = constraintList_makeNew (); 
+  e->falseEnsuresConstraints = constraintList_makeNew (); 
+}
 
 /*
 ** must occur after library has been read
@@ -824,7 +828,7 @@ exprNode_rawStringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc)
   e->kind = XPR_STRINGLITERAL;
   e->val = multiVal_makeString (cstring_copy (t));
   e->edata = exprData_makeLiteral (t);
-  e->sref = sRef_makeType (ctype_string);
+  e->sref = sRef_makeConst (ctype_string);
 
   if (context_getFlag (FLG_READONLYSTRINGS))
     {
@@ -1013,7 +1017,6 @@ exprNode_fromIdentifier (/*@observer@*/ uentry c)
     }
 
   ret = exprNode_fromIdentifierAux (c);
-  
   return ret;
 }
 
@@ -2284,8 +2287,10 @@ static void checkExpressionDefined (exprNode e1, exprNode e2, lltok op)
 	  hasError = optgenerror 
 	    (FLG_EVALORDER,
 	     message ("Expression has undefined behavior "
-		      "(value of left operand is modified "
-		      "by right operand): %s %s %s", 
+		      "(value of left operand %s is modified "
+		      "by right operand %s): %s %s %s", 
+		      exprNode_unparse (e1),
+		      exprNode_unparse (e2),
 		      exprNode_unparse (e1), lltok_unparse (op),
 		      exprNode_unparse (e2)),
 	     e2->loc);
@@ -3085,7 +3090,7 @@ void checkGlobUse (uentry glob, bool isCall, /*@notnull@*/ exprNode e)
 }  
 
 static void
-reflectEnsuresClause (uentry le, exprNode f, exprNodeList args)
+reflectEnsuresClause (exprNode ret, uentry le, exprNode f, exprNodeList args)
 {
   DPRINTF (("Reflect ensures clause: %s(%s) / %s / %s",
 	    exprNode_unparse (f), exprNodeList_unparse (args),
@@ -3139,16 +3144,17 @@ reflectEnsuresClause (uentry le, exprNode f, exprNodeList args)
 			  
 			  if (sRef_isResult (sRef_getRootBase (sel)))
 			    {
-			      ; /*@i423 what do we do about results */
+			      s = exprNode_getSref (ret);
 			    }
 			  else 
 			    {
 			      s = sRef_fixBaseParam (sel, args);
-			      DPRINTF (("Reflecting state clause on: %s / %s",
-					sRef_unparse (sel), sRef_unparse (s)));
-			      
-			      sRef_setMetaStateValueComplete (s, key, mvalue, exprNode_loc (f));
 			    }
+
+			  DPRINTF (("Reflecting state clause on: %s / %s",
+				    sRef_unparse (sel), sRef_unparse (s)));
+			  
+			  sRef_setMetaStateValueComplete (s, key, mvalue, exprNode_loc (f));
 			} end_sRefSet_elements;
 
 		      sRefSet_free (osrs);
@@ -3172,25 +3178,259 @@ reflectEnsuresClause (uentry le, exprNode f, exprNodeList args)
 			  
 			  if (sRef_isResult (sRef_getRootBase (sel)))
 			    {
-			      ; /*@i423 what do we do about results */
+			      DPRINTF (("Fix base: %s / %s",
+					sRef_unparse (sel), sRef_unparse (exprNode_getSref (ret))));
+			      s = sRef_fixBase (sel, exprNode_getSref (ret));
+			      DPRINTF (("==> %s", sRef_unparseFull (s)));
 			    }
 			  else
 			    {
 			      s = sRef_fixBaseParam (sel, args);
+			    }
+
+			  DPRINTF (("elements: %s", sRef_unparse (s)));
+			  DPRINTF (("elements: %s", sRef_unparseFull (s)));
+			  
+			  DPRINTF (("Reflecting state clause on: %s / %s",
+				    sRef_unparseFull (sel), sRef_unparseFull (s)));
+			  
+			  /* evans 2001-08-24 - added aliasSetCompleteParam */
+			  sRef_aliasSetCompleteParam (modf, s, eparam, exprNode_loc (f));
+
+			  DPRINTF (("After reflecting state clause on: %s / %s",
+				    sRef_unparseFull (sel), sRef_unparseFull (s)));
+			} end_sRefSet_elements;
+		    }
+		}
+	    } end_stateClauseList_elements ;	    
+	}
+
+      DPRINTF (("Here: %s / %s",
+		uentry_unparseFull (le),
+		bool_unparse (uentry_hasMetaStateEnsures (le))));
+
+      if (uentry_hasMetaStateEnsures (le))
+	{
+	  fileloc loc = exprNode_loc (f);
+
+	  metaStateConstraintList mscl = uentry_getMetaStateEnsures (le);
+
+	  metaStateConstraintList_elements (mscl, msc)
+	    {
+	      metaStateSpecifier msspec = metaStateConstraint_getSpecifier (msc);
+	      metaStateInfo msinfo = metaStateSpecifier_getMetaStateInfo (msspec);
+	      metaStateExpression msexpr = metaStateConstraint_getExpression (msc);
+	      cstring key = metaStateInfo_getName (msinfo);	      
+	      sRef mlsr = metaStateSpecifier_getSref (msspec);
+	      sRef s;
+	      sRef lastref = sRef_undefined;
+	      stateValue sval = stateValue_undefined;
+	      
+	      DPRINTF (("Meta state constraint for %s: %s", uentry_unparse (le),
+			metaStateConstraint_unparse (msc)));
+	      DPRINTF (("Matches left: %s", sRef_unparseDebug (mlsr)));
+	      
+	      if (sRef_isResult (sRef_getRootBase (mlsr)))
+		{
+		  s = exprNode_getSref (ret);
+		}
+	      else
+		{
+		  s = sRef_fixBaseParam (mlsr, args);
+		}
+	      
+	      DPRINTF (("Setting state: %s", sRef_unparseFull (s)));
+	      
+	      while (metaStateExpression_isDefined (msexpr)) 
+		{
+		  metaStateSpecifier ms = metaStateExpression_getSpecifier (msexpr);
+		  metaStateInfo msi = metaStateSpecifier_getMetaStateInfo (ms);
+		  sRef msr, fs;
+
+		  DPRINTF (("Check expression: %s", metaStateExpression_unparse (msexpr)));
+		  
+		  if (metaStateExpression_isMerge (msexpr))
+		    {
+		      msexpr = metaStateExpression_getRest (msexpr);
+		    }
+		  else
+		    {
+		      msexpr = metaStateExpression_undefined;
+		    }
+		  
+		  if (metaStateInfo_isDefined (msi))
+		    {
+		      /* Must match lhs state */
+		      llassert (metaStateInfo_equal (msinfo, msi));
+		    }
+		  
+		  if (metaStateSpecifier_isElipsis (ms))
+		    {
+		      /*
+		      ** For elipsis, we need to merge all the relevant elipsis parameters
+		      ** 
+		      */
+		      
+		      uentryList params = uentry_getParams (le);
+		      int paramno = uentryList_size (params) - 1;
+
+		      if (!uentry_isElipsisMarker (uentryList_getN (params, paramno)))
+			{
+			  voptgenerror 
+			    (FLG_TYPE,
+			     message ("Ensures clauses uses ... for function without ... in parameter list: %q",
+				      uentry_getName (le)),
+			     uentry_whereLast (le));
+			  /*@innerbreak@*/ break;
+			}
+
+		      while (paramno < exprNodeList_size (args))
+			{
+			  exprNode arg = exprNodeList_getN (args, paramno);
+			  fs = exprNode_getSref (arg);
+			  DPRINTF (("Merge arg: %s", exprNode_unparse (arg)));
+
+			  /* cut and pasted... gack*/
+			  if (stateValue_isDefined (sval))
+			    {
+			      /* Use combination table to merge old state value with new one: */
+			      stateValue tval = sRef_getMetaStateValue (fs, key);
 			      
-			      DPRINTF (("elements: %s", sRef_unparse (s)));
-			      DPRINTF (("elements: %s", sRef_unparseFull (s)));
+			      if (stateValue_isDefined (tval))
+				{
+				  stateCombinationTable sctable = metaStateInfo_getMergeTable (msinfo);
+				  cstring msg = cstring_undefined;
+				  int nval = stateCombinationTable_lookup (sctable, 
+									   stateValue_getValue (sval), 
+									   stateValue_getValue (tval), 
+									   &msg);
+				  DPRINTF (("Combining: %s + %s -> %d",
+					    stateValue_unparseValue (sval, msinfo),
+					    stateValue_unparseValue (tval, msinfo),
+					    nval));
+				  
+				  if (nval == stateValue_error)
+				    {
+				      if (optgenerror 
+					  (FLG_STATEMERGE,
+					   message
+					   ("Attributes merged in ensures clause in states that "
+					    "cannot be combined (%q is %q, %q is %q)%q",
+					    sRef_unparse (lastref),
+					    stateValue_unparseValue (sval, msinfo),
+					    sRef_unparse (fs),
+					    stateValue_unparseValue (tval, msinfo),
+					    cstring_isDefined (msg) ? 
+					    message (": %s", msg) : cstring_undefined),
+					   exprNode_loc (f)))
+					{
+					  sRef_showMetaStateInfo (fs, key);
+					}		    
+				    }
+				  
+				  stateValue_updateValueLoc (sval, nval, fileloc_undefined);
+				  loc = exprNode_loc (arg);
+				}
+			      else
+				{
+				  DPRINTF (("No value for: %s:%s", sRef_unparse (fs), key));
+				}
+			    }
+			  else
+			    {
+			      sval = sRef_getMetaStateValue (fs, key);
+			    }
+			  
+			  lastref = fs;
+			  
+			  if (stateValue_isError (sval))
+			    {
+			      /*@innerbreak@*/ break; /* Don't merge any more values if here was an error */
+			    }
+			
+			  
+			  paramno++;
+			}
+		    }
+		  else
+		    {
+		      msr = metaStateSpecifier_getSref (ms);
+		  
+		      
+		      llassert (sRef_isParam (sRef_getRootBase (msr)));
+		      fs = sRef_fixBaseParam (msr, args);
+		      
+		      if (stateValue_isDefined (sval))
+			{
+			  /* Use combination table to merge old state value with new one: */
+			  stateValue tval = sRef_getMetaStateValue (fs, key);
+			  
+			  if (stateValue_isDefined (tval))
+			    {
+			      stateCombinationTable sctable = metaStateInfo_getMergeTable (msinfo);
+			      cstring msg = cstring_undefined;
+			      int nval = stateCombinationTable_lookup (sctable, 
+								       stateValue_getValue (sval), 
+								       stateValue_getValue (tval), 
+								       &msg);
+			      DPRINTF (("Combining: %s + %s -> %d",
+					stateValue_unparseValue (sval, msinfo),
+					stateValue_unparseValue (tval, msinfo),
+					nval));
 			      
-			      DPRINTF (("Reflecting state clause on: %s / %s",
-					sRef_unparse (sel), sRef_unparse (s)));
+			      if (nval == stateValue_error)
+				{
+				  if (optgenerror 
+				      (FLG_STATEMERGE,
+				       message
+				       ("Attributes merged in ensures clause in states that "
+					"cannot be combined (%q is %q, %q is %q)%q",
+					sRef_unparse (lastref),
+					stateValue_unparseValue (sval, msinfo),
+					sRef_unparse (fs),
+					stateValue_unparseValue (tval, msinfo),
+ 					cstring_isDefined (msg) 
+ 					? message (": %s", msg) : cstring_undefined),
+				       exprNode_loc (f)))
+				    {
+				      sRef_showMetaStateInfo (fs, key);
+				    }		    
+				}
 			      
-			      modf (s, eparam, exprNode_loc (f));
+			      stateValue_updateValueLoc (sval, nval, fileloc_undefined);
 			    }
-			} end_sRefSet_elements;
+			  else
+			    {
+			      DPRINTF (("No value for: %s:%s", sRef_unparse (fs), key));
+			    }
+			}
+		      else
+			{
+			  sval = sRef_getMetaStateValue (fs, key);
+			}
+		      
+		      lastref = fs;
+		      
+		      if (stateValue_isError (sval))
+			{
+			  /*@innerbreak@*/ break; /* Don't merge any more values if here was an error */
+			}
 		    }
 		}
-	    } end_stateClauseList_elements ;
-	    
+
+	      DPRINTF (("Setting: %s:%s <- %s", sRef_unparse (s), key, stateValue_unparse (sval)));
+	      
+	      if (stateValue_isDefined (sval))
+		{
+		  sRef_setMetaStateValueComplete (s, key, stateValue_getValue (sval), loc);
+		}
+	      else
+		{
+		  DPRINTF (("Undefined state: %s", cstring_toCharsSafe (sRef_unparse (s))));
+		}
+	    } end_metaStateConstraintList_elements ;
+
+	  metaStateConstraintList_free (mscl);
 	}
     }
 }
@@ -3252,7 +3492,7 @@ checkRequiresClause (uentry le, exprNode f, exprNodeList args)
 			  
 			  if (sRef_isResult (sRef_getRootBase (sel)))
 			    {
-			      ; /*@i423 what do we do about results */
+			      BADBRANCH;
 			    }
 			  else 
 			    {
@@ -3385,10 +3625,6 @@ functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f,
   checkRequiresClause (le, f, args);
   setCodePoint ();
 
-  DPRINTF (("Reflect: %s", uentry_unparseFull (le)));
-  reflectEnsuresClause (le, f, args);
-  setCodePoint ();
-
   if (uentry_isValid (le)
       && (uentry_isFunction (le) 
           || (uentry_isVariable (le)
@@ -3398,11 +3634,12 @@ functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f,
 
       /* f->typ is already set to the return type */
 
+      DPRINTF (("Function: %s", uentry_unparseFull (le)));
       ret->sref = uentry_returnedRef (le, args);
       DPRINTF (("Returned: %s / %s",
 		uentry_unparseFull (le),
 		sRef_unparseFull (ret->sref)));
-
+      
       if (uentry_isFunction (le) && exprNodeList_size (args) >= 1)
 	{
 	  qual nullPred = uentry_nullPred (le);
@@ -3511,6 +3748,11 @@ functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f,
       exprNode_checkSetAny (ret, uentry_rawName (le));
     }
 
+  DPRINTF (("Before reflect: %s", sRef_unparseFull (ret->sref)));
+  DPRINTF (("Reflect: %s", uentry_unparseFull (le)));
+  reflectEnsuresClause (ret, le, f, args);
+  setCodePoint ();
+
   return (ret);
 }
 
@@ -3518,8 +3760,7 @@ functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f,
 ** this is yucky!  should keep the uentry as part of exprNode!
 */
 
-/*@observer@*/ uentry
-exprNode_getUentry (exprNode e)
+uentry exprNode_getUentry (exprNode e)
 {
   if (exprNode_isError (e))
     {
@@ -4010,53 +4251,54 @@ exprNode_postOp (/*@only@*/ exprNode e, /*@only@*/ lltok op)
   /*DRL 6/8/01 I decided to disable all LCLint Warning here since the code 
     probably needs a rewrite any way */
 
+  /*@i65234@*/
   /*@ignore@*/
 
-  //  updateEnvironmentForPostOp (e);
-
-	/* start modifications */
-	/* added by Seejo on 4/16/2000 */
-
-	/* Arithmetic operations on pointers wil modify the size/len/null terminated 
-		 status */
-	if ((sRef_isPossiblyNullTerminated (e->sref)) || (sRef_isNullTerminated(e->sref))) {
-
-		ret->sref = sRef_copy (e->sref);
-
-		/* Operator : ++ */
-		if (lltok_getTok (op) == INC_OP) {
-			if (sRef_getSize(e->sref) > 0) {
-
-				sRef_setSize (ret->sref, sRef_getSize(e->sref) - 1);
-				
-				if (sRef_getLen(e->sref) == 1) { /* i.e. the first character is \0 */
-					/* Assumption: there is only 1 \0 in the buffer */
-					/* This will not be correct if there are 2 \0's in the buffer */
-					sRef_setNotNullTerminatedState(ret->sref);
-					sRef_resetLen(ret->sref);
-				} else {
-					sRef_setNullTerminatedState(ret->sref);
-					sRef_setLen (ret->sref, sRef_getLen(e->sref) - 1);
-				}
-				if (sRef_isNullTerminated (ret->sref))
-					printf ("ret->sref is Null Terminated\n");
-				else if (sRef_isPossiblyNullTerminated (ret->sref))
-					printf ("ret->sref is Possibly Null Terminated\n");
-				else if (sRef_isNotNullTerminated (ret->sref))
-					printf ("ret->sref is Not Null Terminated\n");
-			}
-		}
-
-		/* Operator : -- */
-		if (lltok_getTok (op) == DEC_OP) {
-			if (sRef_getSize(e->sref) >= 0) {
-				sRef_setSize (ret->sref, sRef_getSize(e->sref) + 1);
-				sRef_setLen (ret->sref, sRef_getLen(e->sref) + 1);
-			}
-		}
-	}
-	/*@end@*/
-	/* end modifications */
+  /* updateEnvironmentForPostOp (e); */
+  
+  /* start modifications */
+  /* added by Seejo on 4/16/2000 */
+  
+  /* Arithmetic operations on pointers wil modify the size/len/null terminated 
+     status */
+  if ((sRef_isPossiblyNullTerminated (e->sref)) || (sRef_isNullTerminated(e->sref))) {
+    
+    ret->sref = sRef_copy (e->sref);
+    
+    /* Operator : ++ */
+    if (lltok_getTok (op) == INC_OP) {
+      if (sRef_getSize(e->sref) > 0) {
+	
+	sRef_setSize (ret->sref, sRef_getSize(e->sref) - 1);
+	
+	if (sRef_getLen(e->sref) == 1) { /* i.e. the first character is \0 */
+	  /* Assumption: there is only 1 \0 in the buffer */
+	  /* This will not be correct if there are 2 \0's in the buffer */
+	  sRef_setNotNullTerminatedState(ret->sref);
+	  sRef_resetLen(ret->sref);
+	} else {
+	  sRef_setNullTerminatedState(ret->sref);
+	  sRef_setLen (ret->sref, sRef_getLen(e->sref) - 1);
+	}
+	if (sRef_isNullTerminated (ret->sref))
+	  printf ("ret->sref is Null Terminated\n");
+	else if (sRef_isPossiblyNullTerminated (ret->sref))
+	  printf ("ret->sref is Possibly Null Terminated\n");
+	else if (sRef_isNotNullTerminated (ret->sref))
+	  printf ("ret->sref is Not Null Terminated\n");
+      }
+    }
+    
+    /* Operator : -- */
+    if (lltok_getTok (op) == DEC_OP) {
+      if (sRef_getSize(e->sref) >= 0) {
+	sRef_setSize (ret->sref, sRef_getSize(e->sref) + 1);
+	sRef_setLen (ret->sref, sRef_getLen(e->sref) + 1);
+      }
+    }
+  }
+  /*@end@*/
+  /* end modifications */
 
   return ret;
 }
@@ -4998,6 +5240,20 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
 		     e1->loc);
 		}
 
+	      /*
+	      ** Swap terms so e1 is always the pointer
+	      */
+
+	      if (ctype_isRealPointer (tr1))
+		{
+		  ;
+		}
+	      else
+		{
+		  exprNode_swap (e1, e2);
+		}
+
+
 	      if (sRef_possiblyNull (e1->sref)
 		  && !usymtab_isGuarded (e1->sref))
 		{
@@ -5012,56 +5268,52 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
 
 	      ret->sref = sRef_copy (e1->sref);
 
-     	 /* start modifications */
-	     /* added by Seejo on 4/16/2000 */
-
-  	    /* Arithmetic operations on pointers wil modify the size/len/null terminated 
-			status */
- 	    if ((sRef_isPossiblyNullTerminated (e1->sref)) || (sRef_isNullTerminated(e1->sref))) {
-				//if (sRef_isKnown (e->sref)) {
-				//ret->sref = sRef_makeAddress (e->sref);
-				//}
-
-	      int val;
-	      /*drl 1-4-2001
-		added ugly fixed to stop
-		program from crashing on point + int +int
-		one day I'll fix this or ask Seejo wtf the codes supposed to do. */
-
-	      if (!multiVal_isInt (e2->val) )
-		break;
-	      /*end drl*/
+	      /* start modifications */
+	      /* added by Seejo on 4/16/2000 */
+
+	      /* Arithmetic operations on pointers wil modify the size/len/null terminated 
+		 status */
+	      if ((sRef_isPossiblyNullTerminated (e1->sref)) || (sRef_isNullTerminated(e1->sref))) {
+		int val;
+		/*drl 1-4-2001
+		  added ugly fixed to stop
+		  program from crashing on point + int +int
+		  one day I'll fix this or ask Seejo wtf the codes supposed to do. */
+		
+		if (!multiVal_isInt (e2->val) )
+		  break;
+		/*end drl*/
+		
+		val = (int) multiVal_forceInt (e2->val);
+		
+		/* Operator : + or += */
+		if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) {
+		  if (sRef_getSize(e1->sref) >= val) {/* Incrementing the pointer by 
+							 val should not result in a 
+							 size < 0 (size = 0 is ok !) */
+		    
+		    sRef_setSize (ret->sref, sRef_getSize(e1->sref) - val);
+		    
+		    if (sRef_getLen(e1->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(e1->sref) - val);
+		    }
+		  }
+		}
+		
+		/* Operator : - or -= */
+		if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) {
+		  if (sRef_getSize(e1->sref) >= 0) {
+		    sRef_setSize (ret->sref, sRef_getSize(e1->sref) + val);
+		    sRef_setLen (ret->sref, sRef_getLen(e1->sref) + val);
+		  }
+		}
+	      }
 	      
-	      val = (int) multiVal_forceInt (e2->val);
-
-			/* Operator : + or += */
-		    if ((lltok_getTok (op) == TPLUS) || (lltok_getTok(op) == ADD_ASSIGN)) {
-				if (sRef_getSize(e1->sref) >= val) {/* Incrementing the pointer by 
-																           val should not result in a 
-																		   size < 0 (size = 0 is ok !) */
-					
-					sRef_setSize (ret->sref, sRef_getSize(e1->sref) - val);
-					
-					if (sRef_getLen(e1->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(e1->sref) - val);
-					}
-				}
-			}
-			
-			/* Operator : - or -= */
-			 if ((lltok_getTok (op) == TMINUS) || (lltok_getTok (op) == SUB_ASSIGN)) {
-				if (sRef_getSize(e1->sref) >= 0) {
-					sRef_setSize (ret->sref, sRef_getSize(e1->sref) + val);
-					sRef_setLen (ret->sref, sRef_getLen(e1->sref) + val);
-				}
-			}
-	    }
-			
-	     /* end modifications */  
+	      /* end modifications */  
 
 	      sRef_setNullError (ret->sref);
 
@@ -5112,56 +5364,52 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
 				 status */
 
  	    if ((sRef_isPossiblyNullTerminated (e2->sref)) || (sRef_isNullTerminated(e2->sref))) {
-				//if (sRef_isKnown (e->sref)) {
-				//ret->sref = sRef_makeAddress (e->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 !) */
-					
-					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);
-					}
-				}
-			}
-			
-			/* 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);
-
-	      /*
-	      ** Fixed for 2.2c: the alias state of ptr + int is dependent,
-	      ** since is points to storage that should not be deallocated
-	      ** through this pointer.
-	      */
-
-	      if (sRef_isOnly (ret->sref) 
-		  || sRef_isFresh (ret->sref)) {
-		sRef_setAliasKind (ret->sref, AK_DEPENDENT, exprNode_loc (ret));
+	      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 !) */
+		  
+		  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);
+		  }
+		}
 	      }
-
-	      tret = e2->typ;
-	      ret->sref = e2->sref;
+	      
+	      /* 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);
+	    
+	    /*
+	    ** Fixed for 2.2c: the alias state of ptr + int is dependent,
+	    ** since is points to storage that should not be deallocated
+	    ** through this pointer.
+	    */
+	    
+	    if (sRef_isOnly (ret->sref) 
+		|| sRef_isFresh (ret->sref)) {
+	      sRef_setAliasKind (ret->sref, AK_DEPENDENT, exprNode_loc (ret));
+	    }
+	    
+	    tret = e2->typ;
+	    ret->sref = e2->sref;
 	    }
 	  else
 	    {
@@ -5354,6 +5602,21 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
 	      tret = ctype_bool;
 	    }
 
+	  /* certain comparisons on unsigned's and zero look suspicious */
+
+	  if (opid == TLT || opid == LE_OP || opid == GE_OP)
+	    {
+	      if ((ctype_isUnsigned (tr1) && exprNode_isZero (e2))
+		  || (ctype_isUnsigned (tr2) && exprNode_isZero (e1)))
+		{
+		  voptgenerror 
+		    (FLG_UNSIGNEDCOMPARE,
+		     message ("Comparison of unsigned value involving zero: %s",
+			      exprNode_unparse (ret)),
+		     e1->loc);
+		}
+	    }
+
 	  /* EQ_OP should NOT be used with booleans (unless one is FALSE) */
 	  
 	  if ((opid == EQ_OP || opid == NE_OP) && 
@@ -5622,6 +5885,8 @@ exprNode_assign (/*@only@*/ exprNode e1,
 			      sRef_unparse (e1->sref)),
 		     g_currentloc);
 		}
+
+	      exprNode_checkAssignMod (e1, ret); /* evans 2001-07-22 */
 	    }
 	}
       else
@@ -5692,11 +5957,11 @@ exprNode_assign (/*@only@*/ exprNode e1,
       /*
       ** be careful!  this defines e1->sref.
       */
-   
-      if (!sRef_isMacroParamRef (e1->sref))
-	{
-	  exprNode_checkSet (ret, e1->sref);
-	}
+
+      /* evans 2001-07-22: removed if (!sRef_isMacroParamRef (e1->sref)) */
+
+      DPRINTF (("Setting: %s -> %s", exprNode_unparse (ret), sRef_unparse (e1->sref)));
+      exprNode_checkSet (ret, e1->sref);
       
       if (isjustalloc) 
 	{
@@ -5847,7 +6112,7 @@ exprNode_cond (/*@keep@*/ exprNode pred, /*@keep@*/ exprNode ifclause,
 	}
       else /* all errors! */
 	{
-	  ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+	  ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
 	}
     }
   
@@ -6334,7 +6599,7 @@ exprNode exprNode_if (/*@only@*/ exprNode pred, /*@only@*/ exprNode tclause)
     {
       if (exprNode_isError (tclause))
 	{
-	  ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+	  ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
 	}
       else
 	{
@@ -6456,7 +6721,7 @@ exprNode exprNode_ifelse (/*@only@*/ exprNode pred,
 	{
 	  if (exprNode_isError (eclause))
 	    {
-	      ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+	      ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
 	    }
 	  else
 	    {
@@ -6860,7 +7125,7 @@ exprNode exprNode_while (/*@keep@*/ exprNode t, /*@keep@*/ exprNode b)
     {
       if (exprNode_isError (b))
 	{
-	  ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+	  ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
 	}
       else
 	{
@@ -6956,7 +7221,7 @@ exprNode exprNode_doWhile (/*@only@*/ exprNode b, /*@only@*/ exprNode t)
     {
       if (exprNode_isError (b))
 	{
-	  ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+	  ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
 	}
       else
 	{
@@ -7001,7 +7266,7 @@ exprNode exprNode_doWhile (/*@only@*/ exprNode b, /*@only@*/ exprNode t)
 
   ret->kind = XPR_DOWHILE;
   ret->edata = exprData_makePair (t, b);
-    return ret;
+  return ret;
 }
 
 exprNode exprNode_for (/*@keep@*/ exprNode inc, /*@keep@*/ exprNode body)
@@ -7436,7 +7701,7 @@ exprNode exprNode_comma (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2)
     {
       if (exprNode_isError (e2))
 	{
-	  ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+	  ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
 	}
       else
 	{
@@ -7535,6 +7800,8 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val)
 	  int i = 0;
 	  int nerrors = 0;
 
+	  /*@i423 check number of entries int a[3] = { 1, 2, 3, 4 } ; */
+
 	  exprNodeList_elements (vals, oneval)
 	    {
 	      cstring istring = message ("%d", i);
@@ -7720,8 +7987,13 @@ exprNode_makeInitializationAux (/*@temp@*/ idDecl t)
     }
   else
     {
-      uentry ue = uentry_makeUnrecognized (idDecl_observeId (t),
-					   g_currentloc);
+      uentry ue;
+
+      DPRINTF (("Unrecognized: %s", idDecl_unparse (t)));
+
+      ue = uentry_makeUnrecognized (idDecl_observeId (t), fileloc_copy (g_currentloc));
+      /*!! fileloc_copy (g_currentloc)); */
+      /*@i32!!! should get error without this */
       ret = exprNode_fromIdentifierAux (ue);
 
       /*
@@ -7738,6 +8010,7 @@ exprNode_makeInitializationAux (/*@temp@*/ idDecl t)
 
   exprData_free (ret->edata, ret->kind); 
   ret->edata = exprData_undefined;
+
   ret->exitCode = XK_NEVERESCAPE;
   ret->mustBreak = FALSE;
   ret->kind = XPR_INIT;
@@ -7758,7 +8031,7 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t,
   uentry ue = usymtab_lookup (idDecl_observeId (t));
   exprNode ret = exprNode_makeInitializationAux (t);
   fileloc loc = exprNode_loc (e);
-
+  
   if (exprNode_isError (e)) 
     {
       e = exprNode_createUnknown ();
@@ -8526,6 +8799,9 @@ static /*@observer@*/ cstring exprNode_rootVarName (exprNode e)
     case XPR_VAR:
       ret = exprData_getId (data);
       break;
+    case XPR_INIT:
+      ret = idDecl_getName (exprData_getInitId (data));
+      break;
     case XPR_LABEL:
     case XPR_TOK:
     case XPR_ITERCALL:
@@ -8567,7 +8843,6 @@ static /*@observer@*/ cstring exprNode_rootVarName (exprNode e)
     case XPR_BLOCK:
     case XPR_STMT:
     case XPR_STMTLIST:
-    case XPR_INIT:
     case XPR_FACCESS:
     case XPR_ARROW:
     case XPR_NODE:
@@ -9242,6 +9517,7 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc)
 		    {
 		      lastRef = errorRef;
 		      errorRef = s;
+		      DPRINTF (("Setting ERROR: %s", sRef_unparseFull (s)));
 		      deadRef = sRef_isPossiblyDead (errorRef);
 		      unuseable = sRef_isUnuseable (errorRef);
 		      errorMaybe = TRUE;
@@ -9257,6 +9533,7 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc)
 
 		  if (!sRef_isPartial (s))
 		    {
+		      DPRINTF (("Defining! %s", sRef_unparseFull (s)));
 		      sRef_setDefined (s, fileloc_undefined);
 		    }
 		}
@@ -9337,6 +9614,8 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc)
 			      sRef_unparseOpt (errorRef),
 			      cstring_makeLiteral (errorMaybe ? "may be " : "")),
 		     loc);
+
+		  DPRINTF (("Error: %s", sRef_unparseFull (errorRef)));
 		}
 	      
 	      sRef_setDefined (errorRef, loc);
@@ -9393,8 +9672,7 @@ exprNode_checkSet (exprNode e, /*@exposed@*/ sRef s)
 	}
      
       if (sRef_isMeaningful (s))
-	{
-	  
+	{	  
 	  if (sRef_isDead (s))
 	    {
 	      sRef base = sRef_getBaseSafe (s);
@@ -9964,9 +10242,12 @@ checkOneRepExpose (sRef ysr, sRef base,
 		   sRef s2b)
 {
   if (!(sRef_isOnly (ysr) || sRef_isKeep (ysr) 
-	|| sRef_isOwned (ysr) || sRef_isExposed (ysr)))
+	|| sRef_isOwned (ysr) 
+	|| sRef_isExposed (ysr)))
     {
-      if (sRef_isAnyParam (base) && !sRef_isExposed (base))
+      if (sRef_isAnyParam (base) && !sRef_isExposed (base)
+	  && !sRef_isObserver (base)) /* evans 2001-07-11: added isObserver */
+
 	{
 	  if (sRef_isIReference (ysr))
 	    {
@@ -10475,8 +10756,9 @@ long exprNode_getLongValue (exprNode e) {
     lltok t = exprData_getUopTok (e->edata);
     return fileloc_copy(lltok_getLoc (t));
   } else {
-    //drl possible problem : warning fix
-    //    llcontbug (message ("Cannot get next sequence point: %s", exprNode_unparse (e)));
+    /* drl possible problem : warning fix
+       llcontbug (message ("Cannot get next sequence point: %s", exprNode_unparse (e)));
+    */
     return fileloc_undefined;
   }
  }
@@ -10489,3 +10771,8 @@ exprNode exprNode_createNew(ctype c)
 
   return ret;
 }
+
+bool exprNode_isInitBlock (exprNode e)
+{
+  return (exprNode_isDefined(e) && e->kind == XPR_INITBLOCK);
+}