]> andersk Git - splint.git/blobdiff - src/exprNode.c
Fixed line numbering when multi-line macro parameters are used.
[splint.git] / src / exprNode.c
index 4f36072412172350d108aeb8c8837cad8b28b3be..f3040f796fa2efb93015898828b3076726afab58 100644 (file)
@@ -1,6 +1,6 @@
 /*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2001 University of Virginia,
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2002 University of Virginia,
 **         Massachusetts Institute of Technology
 **
 ** This program is free software; you can redistribute it and/or modify it
 ** 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 more information: http://lclint.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
 */
 /*
 ** exprNode.c
 */
 
 # include <ctype.h> /* for isdigit */
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
 # include "basic.h"
 # include "cgrammar.h"
 # include "cgrammar_tokens.h"
 # include "transferChecks.h"
 # include "exprNodeSList.h"
 
+static bool exprNode_sameStorage (exprNode p_e1, exprNode p_e2) /*@*/ ;
 static bool exprNode_isEmptyStatement (exprNode p_e);
 static /*@exposed@*/ exprNode exprNode_firstStatement (/*@returned@*/ exprNode p_e);
 static bool exprNode_isFalseConstant (exprNode p_e) /*@*/ ;
-static bool exprNode_isBlock (exprNode p_e);
+static bool exprNode_isStatement (exprNode p_e);
 static void checkGlobUse (uentry p_glob, bool p_isCall, /*@notnull@*/ exprNode p_e);
 static void exprNode_addUse (exprNode p_e, /*@exposed@*/ sRef p_s);
 static bool exprNode_matchArgType (ctype p_ct, exprNode p_e);
@@ -105,16 +106,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
@@ -671,7 +676,13 @@ exprNode_isUnknownConstant (/*@notnull@*/ exprNode e)
   while (e->kind == XPR_PARENS)
     {
       e = exprData_getUopNode (e->edata);
-      llassert (exprNode_isDefined (e));
+      
+      if (!exprNode_isDefined (e))
+       {
+         return FALSE;
+       }
+
+      /* evans 2002-02-05: was llassert (exprNode_isDefined (e)); but this can fail */
     }
 
   if (e->kind == XPR_CONST)
@@ -804,17 +815,17 @@ exprNode_combineLiterals (exprNode e, exprNode rest)
 exprNode_rawStringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc)
 {
   exprNode e = exprNode_createLoc (ctype_string, loc);
-  int len = cstring_length (t);
+  size_t len = cstring_length (t);
 
   if (context_getFlag (FLG_STRINGLITERALLEN))
     {
-      if (len > context_getValue (FLG_STRINGLITERALLEN))
+      if (len > size_fromInt (context_getValue (FLG_STRINGLITERALLEN)))
        {
          voptgenerror (FLG_STRINGLITERALLEN,
                        message
                        ("String literal length (%d) exceeds maximum "
                         "length (%d): \"%s\"",
-                        len,
+                        size_toInt (len),
                         context_getValue (FLG_STRINGLITERALLEN),
                         t),
                        e->loc);
@@ -824,7 +835,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))
     {
@@ -839,15 +850,23 @@ exprNode_rawStringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc)
   return (e); /* s released */
 }
 
+/*@only@*/ exprNode
+exprNode_wideStringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc)
+{
+  exprNode res = exprNode_stringLiteral (t, loc);
+  res->typ = ctype_makeWideString ();
+  return res;
+}
+
 /*@only@*/ exprNode
 exprNode_stringLiteral (/*@only@*/ cstring t, /*@only@*/ fileloc loc)
 {
-  int len = cstring_length (t) - 2;
+  size_t len = size_fromInt (cstring_length (t) - 2);
   char *ts = cstring_toCharsSafe (t);
   char *s = cstring_toCharsSafe (cstring_create (len + 1));
 
   llassert (*ts == '\"' && *(ts + len + 1) == '\"');
-  strncpy (s, ts+1, size_fromInt (len));
+  strncpy (s, ts+1, len);
   *(s + len) = '\0';
   cstring_free (t);
   return exprNode_rawStringLiteral (cstring_fromCharsO (s), loc);
@@ -922,12 +941,30 @@ exprNode exprNode_fromUIO (cstring c)
   return (e);
 }
 
+exprNode exprNode_makeConstantString (cstring c, /*@only@*/ fileloc loc)
+{
+  exprNode e  = exprNode_createPlain (ctype_unknown);
+  e->kind = XPR_VAR;
+  e->loc = loc; 
+  e->sref = sRef_makeConst (ctype_string);
+  e->edata = exprData_makeId (uentry_makeUnrecognized (c, fileloc_copy (loc)));
+  e->typ = ctype_string;
+  
+  /* No alias errors for unrecognized identifiers */
+  sRef_setAliasKind (e->sref, AK_STATIC, loc); 
+  sRef_setExKind (e->sref, XO_OBSERVER, loc);
+  
+  return (e);
+}
+
 exprNode exprNode_createId (/*@observer@*/ uentry c)
 {
   if (uentry_isValid (c))
     {
       exprNode e = exprNode_new ();
-      
+
+      DPRINTF (("create id: %s", uentry_unparse (c)));
+
       e->typ = uentry_getType (c);
 
       if (uentry_isFunction (c)
@@ -947,7 +984,7 @@ exprNode exprNode_createId (/*@observer@*/ uentry c)
       
       /*
       ** yoikes!  leaving this out was a heinous bug...that would have been
-      ** caught if i had lclint working first.  gag!
+      ** caught if i had splint working first.  gag!
       */
       
       e->etext = cstring_undefined;
@@ -977,7 +1014,7 @@ exprNode exprNode_createId (/*@observer@*/ uentry c)
       e->msets = sRefSet_new ();
       e->uses = sRefSet_new ();
       
-      /*> missing fields, detected by lclint <*/
+      /*> missing fields, detected by splint <*/
       e->exitCode = XK_NEVERESCAPE;
       e->isJumpPoint = FALSE;
       e->canBreak = FALSE;
@@ -1013,11 +1050,84 @@ exprNode_fromIdentifier (/*@observer@*/ uentry c)
     }
 
   ret = exprNode_fromIdentifierAux (c);
-  
   return ret;
 }
 
 
+static void exprNode_checkStringLiteralLength (ctype t1, exprNode e2)
+{
+  multiVal mval = exprNode_getValue (e2);
+  cstring slit;
+  int len;
+
+  if (ctype_isFixedArray (t1))
+    {
+      int nelements = long_toInt (ctype_getArraySize (t1));
+      
+      llassert (multiVal_isString (mval));
+      slit = multiVal_forceString (mval);
+      
+      len = cstring_lengthExpandEscapes (slit);
+      
+      llassert (exprNode_isDefined (e2));
+
+      if (len == nelements)
+       {
+         mstring temp;
+
+         temp = cstring_expandEscapes (slit);
+
+         if (temp[len-1] == '\0')
+           {
+             voptgenerror 
+               (FLG_STRINGLITNOROOMFINALNULL,
+                message ("String literal with %d character%& "
+                         "is assigned to %s (no room for final null terminator): %s",
+                         len + 1,
+                         ctype_unparse (t1),
+                         exprNode_unparse (e2)),
+                e2->loc);
+           }
+         else
+           {
+             voptgenerror 
+               (FLG_STRINGLITNOROOM,
+                message ("String literal with %d character%& "
+                         "is assigned to %s (no room for null terminator): %s",
+                         len + 1,
+                         ctype_unparse (t1),
+                         exprNode_unparse (e2)),
+                e2->loc);
+           }
+       }
+      else if (len > nelements) 
+       {
+         voptgenerror 
+           (FLG_STRINGLITTOOLONG,
+            message ("String literal with %d character%& (counting null terminator) "
+                     "is assigned to %s (insufficient storage available): %s",
+                     len + 1,
+                     ctype_unparse (t1),
+                     exprNode_unparse (e2)),
+            e2->loc);                        
+       }
+      else if (len < nelements - 1)
+       {
+         voptgenerror 
+           (FLG_STRINGLITSMALLER,
+            message ("String literal with %d character%& is assigned to %s (possible waste of storage): %s",
+                     len + 1,
+                     ctype_unparse (t1),
+                     exprNode_unparse (e2)),
+            e2->loc);    
+       }
+      else
+       {
+         ; /* okay */
+       }
+    }
+}
+
 static /*@only@*/ /*@notnull@*/ exprNode
 exprNode_fromIdentifierAux (/*@observer@*/ uentry c)
 {
@@ -1061,6 +1171,16 @@ exprNode_isNonNegative (exprNode e)
        {
          return (multiVal_forceInt (m) >= 0);
        }
+
+      /*
+      ** This is not always true if programmer defines enum
+      ** values, but then the constant should be known.
+      */
+
+      if (ctype_isEnum (ctype_realType (e->typ)))
+       {
+         return TRUE;
+       }
     }
 
   return FALSE;
@@ -1083,6 +1203,9 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2)
   ** error in ind, assume valid and continue
   */
 
+  DPRINTF (("Array fetch: %s / %s",
+           exprNode_unparse (e1), exprNode_unparse (e2)));
+
   if (exprNode_isError (e1))
     {
       exprNode_free (e2);
@@ -1097,10 +1220,12 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2)
  
       /*
       ** this sets up funny aliasing, that leads to spurious
-      ** lclint errors.  Hence, the i2 comments.
+      ** splint errors.  Hence, the i2 comments.
       */
 
-      if (!ctype_isRealArray (crarr) 
+      /* evans 2001-09-09 added ctype_isKnown so there is no swap when e1 type is unknown */
+      if (ctype_isKnown (crarr)
+         && !ctype_isRealArray (crarr) 
          && ctype_isRealNumeric (crarr) 
          && !exprNode_isError (e2)
          && ctype_isRealAP (exprNode_getType (e2)))  /* fetch like 3[a] */
@@ -1117,6 +1242,8 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2)
          ind = e2;
        }
 
+      DPRINTF (("arr: %s", exprNode_unparse (arr)));
+
       if (sRef_possiblyNull (arr->sref))
         {
           if (!usymtab_isGuarded (arr->sref))
@@ -1128,6 +1255,7 @@ exprNode_arrayFetch (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2)
                                        exprNode_unparse (arr)),
                               arr->loc))
                {
+                 DPRINTF (("ref: %s", sRef_unparseFull (arr->sref)));
                  sRef_showNullInfo (arr->sref);
 
                  /* suppress future messages */
@@ -1490,7 +1618,14 @@ checkPrintfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn,
                          /*@switchbreak@*/ break;
                          
                        case 'c': /* int converted to char (check its a char?) */
-                         expecttype = ctype_makeConj (ctype_char, ctype_uchar);
+                         expecttype = ctype_makeConj (ctype_int, 
+                                                      ctype_makeConj (ctype_char,
+                                                                      ctype_uchar));
+                         /*@i231@*/
+                         /* evans 2001-10-05 - changed to reflect correct ISO spec:
+                            int converted to char */
+                         
+                         /* expecttype = ctype_makeConj (ctype_char, ctype_uchar); */
                          /*@switchbreak@*/ break;
                              
                        case 's': /* string */
@@ -2284,8 +2419,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);
@@ -3031,7 +3168,7 @@ checkGlobMods (/*@notnull@*/ /*@dependent@*/ exprNode f,
   if (freshMods)
     {
       /*
-      ** Spurious errors reported, because lclint can't tell
+      ** Spurious errors reported, because splint can't tell
       ** mods must be fresh if freshMods is true.
       */
 
@@ -3085,7 +3222,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 +3276,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);
@@ -3158,7 +3296,9 @@ reflectEnsuresClause (uentry le, exprNode f, exprNodeList args)
                      sRefSet srs = stateClause_getRefs (cl);
                      sRefModVal modf = stateClause_getEnsuresFunction (cl);
                      int eparam = stateClause_getStateParameter (cl);
-                     
+
+                     llassert (modf != NULL);
+
                      DPRINTF (("Reflect after clause: %s / %s", 
                                stateClause_unparse (cl),
                                sRefSet_unparse (srs)));
@@ -3172,25 +3312,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 +3626,7 @@ checkRequiresClause (uentry le, exprNode f, exprNodeList args)
                          
                          if (sRef_isResult (sRef_getRootBase (sel)))
                            {
-                             ; /*@i423 what do we do about results */
+                             BADBRANCH;
                            }
                          else 
                            {
@@ -3298,6 +3672,8 @@ checkRequiresClause (uentry le, exprNode f, exprNodeList args)
                                stateClause_unparse (cl),
                                sRefSet_unparse (srs)));
                      
+                     llassert (modf != NULL);
+
                      sRefSet_elements (srs, sel)
                        {
                          sRef s;
@@ -3385,10 +3761,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 +3770,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 +3884,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 +3896,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))
     {
@@ -3534,6 +3911,19 @@ exprNode_getUentry (exprNode e)
     }
 }
 
+/*
+** Returns true iff e1 and e2 are both exactly the same storage
+** (conservative).
+*/
+
+static bool exprNode_sameStorage (exprNode e1, exprNode e2)
+{
+  sRef s1 = exprNode_getSref (e1);
+  sRef s2 = exprNode_getSref (e2);
+  
+  return (sRef_realSame (s1, s2));
+}
+
 exprNode 
 exprNode_makeInitBlock (lltok brace, /*@only@*/ exprNodeList inits)
 {
@@ -4007,56 +4397,57 @@ exprNode_postOp (/*@only@*/ exprNode e, /*@only@*/ lltok op)
 
   /* added 7/11/2000 D.L */
   /*@i223*/ 
-  /*DRL 6/8/01 I decided to disable all LCLint Warning here since the code 
+  /*DRL 6/8/01 I decided to disable all Splint warnings 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;
 }
@@ -4318,8 +4709,11 @@ exprNode_preOp (/*@only@*/ exprNode e, /*@only@*/ lltok op)
       
       if (sRef_isKnown (e->sref))
        {
+         DPRINTF (("Checking possibly null: %s", sRef_unparseFull (e->sref)));
+
          if (sRef_possiblyNull (e->sref))
            {
+             DPRINTF (("Checking possibly null: %s", sRef_unparse (e->sref)));
              if (!usymtab_isGuarded (e->sref) && !context_inProtectVars ())
                {
                  if (optgenerror 
@@ -4373,7 +4767,7 @@ ctype sizeof_resultType (void)
        }
       else
        {
-                 sizet = ctype_ulint;
+         sizet = ctype_ulint;
        }
     }
   return sizet;
@@ -4881,6 +5275,7 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
     }
 
   ret->val = multiVal_undefined;
+
   ret->kind = XPR_OP;
   ret->edata = exprData_makeOp (e1, e2, op);
 
@@ -4909,6 +5304,7 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
 
   tret = ctype_unknown;
   te1 = exprNode_getType (e1);
+
   DPRINTF (("te1 = %s / %s", exprNode_unparse (e1), ctype_unparse (te1)));
 
   te2 = exprNode_getType (e2);
@@ -4973,7 +5369,18 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
        case TDIV:              /*                                        */
        case MUL_ASSIGN:        /*    numeric, numeric -> numeric         */
        case DIV_ASSIGN:        /*                                        */
-         
+
+         if (opid == TMULT || opid == MUL_ASSIGN)
+           {
+             ret->val = multiVal_multiply (exprNode_getValue (e1),
+                                           exprNode_getValue (e2));
+           }
+         else
+           {
+             ret->val = multiVal_divide (exprNode_getValue (e1),
+                                         exprNode_getValue (e2));
+           }
+                 
          tret = checkNumerics (tr1, tr2, te1, te2, e1, e2, op);
          break;
          
@@ -4981,7 +5388,18 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
        case TMINUS:            /*    pointer, int     -> pointer          */
        case SUB_ASSIGN:        /*    int, pointer     -> pointer          */
        case ADD_ASSIGN:        /*    numeric, numeric -> numeric          */
-         
+
+         if (opid == TPLUS || opid == ADD_ASSIGN)
+           {
+             ret->val = multiVal_add (exprNode_getValue (e1),
+                                      exprNode_getValue (e2));
+           }
+         else
+           {
+             ret->val = multiVal_subtract (exprNode_getValue (e1),
+                                           exprNode_getValue (e2));
+           }
+
          tr1 = ctype_fixArrayPtr (tr1);
 
          if ((ctype_isRealPointer (tr1) && !exprNode_isNullValue (e1))
@@ -4998,6 +5416,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 +5444,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-2002
+                 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);
 
@@ -5098,68 +5526,63 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
                    (FLG_NULLPOINTERARITH,
                     message ("Pointer arithmetic involving possibly "
                              "null pointer %s: %s", 
-                             exprNode_unparse (e2), 
-                             exprNode_unparse (ret)),
-                    e2->loc);
-               }
-
-             ret->sref = sRef_copy (e2->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 (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);
-                               }
-                       }
-                }
+                             exprNode_unparse (e2), 
+                             exprNode_unparse (ret)),
+                    e2->loc);
+               }
 
-           /* end modifications */
+             ret->sref = sRef_copy (e2->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 (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 !) */
+                   
+                   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));
              }
-
+             
              tret = e2->typ;
              ret->sref = e2->sref;
            }
@@ -5170,7 +5593,7 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
          
          break;
 
-       case LEFT_ASSIGN:   /* Shifts: should be unsigned values */
+       case LEFT_ASSIGN:   
        case RIGHT_ASSIGN:
        case LEFT_OP:
        case RIGHT_OP:
@@ -5182,47 +5605,80 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
        case OR_ASSIGN:
          {
            bool reported = FALSE;
-           flagcode code = FLG_BITWISEOPS;
            
-           if (opid == LEFT_OP || opid == LEFT_ASSIGN
-               || opid == RIGHT_OP || opid == RIGHT_ASSIGN) {
-             code = FLG_SHIFTSIGNED;
-           }
+           /*
+           ** Shift Operator 
+           */
 
-           if (!ctype_isUnsigned (tr1)) 
+           if (opid == LEFT_OP || opid == LEFT_ASSIGN
+               || opid == RIGHT_OP || opid == RIGHT_ASSIGN) 
              {
-               if (exprNode_isNonNegative (e1)) {
-                 ;
-               } else {
-                 reported = optgenerror 
-                   (code,
-                    message ("Left operand of %s is not unsigned value (%t): %s",
-                             lltok_unparse (op), te1,
-                             exprNode_unparse (ret)),
-                    e1->loc);
-                 
-                 if (reported) {
-                   te1 = ctype_uint;
+               /*
+               ** evans 2002-01-01: fixed this to follow ISO 6.5.7.
+               */
+               
+               if (!ctype_isUnsigned (tr2)
+                   && !exprNode_isNonNegative (e2))
+                 {
+                   reported = optgenerror 
+                     (FLG_SHIFTNEGATIVE,
+                      message ("Right operand of %s may be negative (%t): %s",
+                               lltok_unparse (op), te2,
+                               exprNode_unparse (ret)),
+                      e2->loc);
                  }
-               }
+               
+               if (!ctype_isUnsigned (tr1)
+                   && !exprNode_isNonNegative (e1))
+                 {
+                   reported = optgenerror 
+                     (FLG_SHIFTIMPLEMENTATION,
+                      message ("Left operand of %s may be negative (%t): %s",
+                               lltok_unparse (op), te1,
+                               exprNode_unparse (ret)),
+                      e1->loc);
+                 }
+               
+               /*
+               ** Should check size of right operand also...
+               */
+               
              }
-           else 
+           else
              {
-               /* right need not be signed for shifts */
-               if (code != FLG_SHIFTSIGNED 
-                   && !ctype_isUnsigned (tr2)) 
+               if (!ctype_isUnsigned (tr1)) 
                  {
-                   if (!exprNode_isNonNegative (e2)) {
+                   if (exprNode_isNonNegative (e1)) {
+                     ;
+                   } else {
                      reported = optgenerror 
-                       (code,
-                        message ("Right operand of %s is not unsigned value (%t): %s",
-                                 lltok_unparse (op), te2,
+                       (FLG_BITWISEOPS,
+                        message ("Left operand of %s is not unsigned value (%t): %s",
+                                 lltok_unparse (op), te1,
                                  exprNode_unparse (ret)),
-                        e2->loc);
+                        e1->loc);
+                     
+                     if (reported) {
+                       te1 = ctype_uint;
+                     }
                    }
                  }
+               else 
+                 {
+                   if (!ctype_isUnsigned (tr2)) 
+                     {
+                       if (!exprNode_isNonNegative (e2)) {
+                         reported = optgenerror 
+                           (FLG_BITWISEOPS,
+                            message ("Right operand of %s is not unsigned value (%t): %s",
+                                     lltok_unparse (op), te2,
+                                     exprNode_unparse (ret)),
+                            e2->loc);
+                       }
+                     }
+                 }
              }
-           
+
            if (!reported) 
              {
                if (!checkIntegral (e1, e2, ret, op)) {
@@ -5251,6 +5707,10 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
        case NE_OP:
        case TLT:               /* comparisons                           */
        case TGT:               /*    numeric, numeric -> bool           */
+
+         DPRINTF (("Here we go: %s / %s",
+                   ctype_unparse (tr1), ctype_unparse (tr2)));
+
          if ((ctype_isReal (tr1) && !ctype_isInt (tr1))
              || (ctype_isReal (tr2) && !ctype_isInt (tr2)))
            {
@@ -5319,6 +5779,9 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
          ** Types should match.
          */
 
+         DPRINTF (("Match types: %s / %s", exprNode_unparse (e1),
+                   exprNode_unparse (e2)));
+
          if (!exprNode_matchTypes (e1, e2))
            {
              hasError = gentypeerror 
@@ -5354,6 +5817,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) && 
@@ -5450,7 +5928,7 @@ exprNode_makeOp (/*@keep@*/ exprNode e1, /*@keep@*/ exprNode e2,
            llfatalbug 
              (cstring_makeLiteral 
               ("There has been a problem in the parser. This is believed to result "
-               "from a problem with bison v. 1.25.  Please try rebuidling LCLint "
+               "from a problem with bison v. 1.25.  Please try rebuidling Splint "
                "using the pre-compiled grammar files by commenting out the "
                "BISON= line in the top-level Makefile."));
          }
@@ -5522,11 +6000,11 @@ void exprNode_checkAssignMod (exprNode e1, exprNode ret)
 }
 
 exprNode
-exprNode_assign (/*@only@*/ exprNode e1,
-                /*@only@*/ exprNode e2, /*@only@*/ lltok op)
+exprNode_assign (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2, /*@only@*/ lltok op)
 {
   bool isalloc = FALSE;
   bool isjustalloc = FALSE;
+  bool noalias = FALSE;
   exprNode ret;
 
   DPRINTF (("%s [%s] <- %s [%s]",
@@ -5538,7 +6016,22 @@ exprNode_assign (/*@only@*/ exprNode e1,
   if (lltok_getTok (op) != TASSIGN) 
     {
       ret = exprNode_makeOp (e1, e2, op);
-    } 
+
+      DPRINTF (("Here goes: %s %s",
+               ctype_unparse (e1->typ),
+               ctype_unparse (e2->typ)));
+
+      if (exprNode_isDefined (e1)
+         && exprNode_isDefined (e2))
+       {
+         if (ctype_isNumeric (e2->typ)
+             || ctype_isNumeric (e1->typ))
+           {
+             /* Its a pointer arithmetic expression like ptr += i */
+             noalias = TRUE;
+           }
+       } 
+    }
   else 
     {
       ret = exprNode_createPartialCopy (e1);
@@ -5622,6 +6115,8 @@ exprNode_assign (/*@only@*/ exprNode e1,
                              sRef_unparse (e1->sref)),
                     g_currentloc);
                }
+
+             exprNode_checkAssignMod (e1, ret); /* evans 2001-07-22 */
            }
        }
       else
@@ -5636,7 +6131,17 @@ exprNode_assign (/*@only@*/ exprNode e1,
              ctype te1 = exprNode_getType (e1);
              ctype te2 = exprNode_getType (e2);
              
-             if (!ctype_forceMatch (te1, te2))
+             if (ctype_isVoid (te2))
+               {
+                 (void) gentypeerror 
+                   (te2, e2, te1, e1,
+                    message ("Assignment of void value to %t: %s %s %s", 
+                             te1, exprNode_unparse (e1),
+                             lltok_unparse (op), 
+                             exprNode_unparse (e2)),
+                    e1->loc);
+               }
+             else if (!ctype_forceMatch (te1, te2))
                {
                  if (exprNode_matchLiteral (te1, e2))
                    {
@@ -5653,12 +6158,25 @@ exprNode_assign (/*@only@*/ exprNode e1,
                         e1->loc);
                    }
                }
+             else
+               {
+                 /* Type checks okay */
+               }
            }
         
          exprNode_mergeUSs (ret, e2);
          exprNode_checkUse (ret, e2->sref, e2->loc);
          
-         doAssign (e1, e2, FALSE); 
+         DPRINTF (("Do assign! %s %s", exprNode_unparse (e1), exprNode_unparse (e2)));
+         if (noalias)
+           {
+             ;
+           }
+         else
+           {
+             doAssign (e1, e2, FALSE); 
+           }
+
          ret->sref = e1->sref;
        }
       else
@@ -5666,7 +6184,7 @@ exprNode_assign (/*@only@*/ exprNode e1,
          if (exprNode_isDefined (e2))
            {
              exprNode_mergeUSs (ret, e2);
-                     exprNode_checkUse (ret, e2->sref, e2->loc);
+             exprNode_checkUse (ret, e2->sref, e2->loc);
            }
        }
 
@@ -5692,11 +6210,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 +6365,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));
        }
     }
   
@@ -6053,6 +6571,7 @@ exprNode_mustBreak (exprNode e)
     {
       return e->mustBreak;
     }
+
   return FALSE;
 }
 
@@ -6175,7 +6694,7 @@ exprNode exprNode_concat (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2)
                {
                  voptgenerror (FLG_CASEBREAK,
                                cstring_makeLiteral 
-                               ("Fall through case (no preceeding break)"),
+                               ("Fall through case (no preceding break)"),
                                e2->loc);
                }
            }
@@ -6191,6 +6710,7 @@ exprNode exprNode_concat (/*@only@*/ exprNode e1, /*@only@*/ exprNode e2)
       usymtab_setMustBreak ();
     }
 
+  DPRINTF (("==> %s", exprNode_unparse (ret)));
   return ret;
 }
 
@@ -6207,7 +6727,7 @@ exprNode exprNode_statement (/*@only@*/ exprNode e, /*@only@*/ lltok t)
 {
   if (!exprNode_isError (e))
     {
-      exprNode_checkStatement(e);
+      exprChecks_checkStatementEffect(e);
     }
 
   return (exprNode_statementError (e, t));
@@ -6262,6 +6782,36 @@ void exprNode_produceGuards (exprNode pred)
     }
 }
 
+exprNode exprNode_compoundStatementExpression (/*@only@*/ lltok tlparen, /*@only@*/ exprNode e)
+{
+  exprNode laststmt;
+
+  DPRINTF (("Compound: %s", exprNode_unparse (e)));
+
+  if (!context_flagOn (FLG_GNUEXTENSIONS, exprNode_loc (e)))
+    {
+      (void) llgenhinterror 
+       (FLG_SYNTAX,
+        message ("Compound statement expressions is not supported by ISO C99"),
+        message ("Use +gnuextensions to allow compound statement expressions (and other GNU language extensions) "
+                 "without this warning"),
+        exprNode_loc (e));
+    }
+
+  /*
+  ** The type of a compoundStatementExpression is the type of the last statement 
+  */
+  
+  llassert (exprNode_isBlock (e));
+  laststmt = exprNode_lastStatement (e);
+
+  DPRINTF (("Last statement: %s / %s", exprNode_unparse (laststmt), ctype_unparse (exprNode_getType (laststmt))));
+  DPRINTF (("e: %s", exprNode_unparse (e)));
+  e->typ = exprNode_getType (laststmt);
+  return exprNode_addParens (tlparen, e);
+}
+
+
 exprNode exprNode_makeBlock (/*@only@*/ exprNode e)
 {
   exprNode ret = exprNode_createPartialCopy (e);
@@ -6273,8 +6823,10 @@ exprNode exprNode_makeBlock (/*@only@*/ exprNode e)
       ret->mustBreak = e->mustBreak;
     }
   
+  DPRINTF (("Block e: %s", exprNode_unparse (e)));
   ret->edata = exprData_makeSingle (e);
   ret->kind = XPR_BLOCK;
+  DPRINTF (("Block: %s", exprNode_unparse (ret)));
   return ret;
 }
 
@@ -6283,6 +6835,12 @@ bool exprNode_isBlock (exprNode e)
   return (exprNode_isDefined (e) 
          && ((e)->kind == XPR_BLOCK));
 }
+
+bool exprNode_isStatement (exprNode e)
+{
+  return (exprNode_isDefined (e) 
+         && ((e)->kind == XPR_STMT));
+}
  
 bool exprNode_isAssign (exprNode e)
 {
@@ -6301,6 +6859,27 @@ bool exprNode_isEmptyStatement (exprNode e)
          && (lltok_isSemi (exprData_getTok (e->edata))));
 }
 
+bool exprNode_isMultiStatement (exprNode e)
+{
+  return (exprNode_isDefined (e)
+         && ((e->kind == XPR_FOR)
+             || (e->kind == XPR_FORPRED)
+             || (e->kind == XPR_IF)
+             || (e->kind == XPR_IFELSE)
+             || (e->kind == XPR_WHILE)
+             || (e->kind == XPR_WHILEPRED)
+             || (e->kind == XPR_DOWHILE)
+             || (e->kind == XPR_BLOCK)
+             || (e->kind == XPR_STMT)
+             || (e->kind == XPR_STMTLIST)
+             || (e->kind == XPR_SWITCH)));
+}
+
+void exprNode_checkIfPred (exprNode pred)
+{
+  exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred);
+}
+
 exprNode exprNode_if (/*@only@*/ exprNode pred, /*@only@*/ exprNode tclause)
 {
   exprNode ret;
@@ -6334,7 +6913,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
        {
@@ -6350,8 +6929,8 @@ exprNode exprNode_if (/*@only@*/ exprNode pred, /*@only@*/ exprNode tclause)
             message ("Predicate always exits: %s", exprNode_unparse (pred)),
             exprNode_loc (pred));
        }
-
-      exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred);
+      
+      /*! exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred); */ /*@i523@*/
       exprNode_checkUse (pred, pred->sref, pred->loc);
       
       if (!exprNode_isError (tclause))
@@ -6456,7 +7035,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
            {
@@ -6480,7 +7059,7 @@ exprNode exprNode_ifelse (/*@only@*/ exprNode pred,
             exprNode_loc (pred));
        }
       
-      exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred);
+      /*@i3423 exprNode_checkPred (cstring_makeLiteralTemp ("if"), pred);*/
       exprNode_checkUse (ret, pred->sref, pred->loc);
       
       exprNode_mergeCondUSs (ret, tclause, eclause);
@@ -6535,6 +7114,9 @@ checkSwitchExpr (exprNode test, /*@dependent@*/ exprNode e, /*@out@*/ bool *allp
 
   exprNodeSList_elements (el, current)
     {
+      
+      DPRINTF ((message("checkSwitchExpr current = %s ", exprNode_unparse(current) ) ));
+      
       if (exprNode_isDefined (current))
        {
          switch (current->kind)
@@ -6544,7 +7126,7 @@ checkSwitchExpr (exprNode test, /*@dependent@*/ exprNode e, /*@out@*/ bool *allp
              if (hasDefault)
                {
                  voptgenerror 
-                   (FLG_CONTROL,
+                   (FLG_DUPLICATECASES,
                     message ("Duplicate default cases in switch"),
                     exprNode_loc (current));
                }          
@@ -6572,7 +7154,7 @@ checkSwitchExpr (exprNode test, /*@dependent@*/ exprNode e, /*@out@*/ bool *allp
                                  (/*@-usedef@*/usedEnums/*@=usedef@*/, cname))
                                {
                                  voptgenerror
-                                   (FLG_CONTROL,
+                                   (FLG_DUPLICATECASES,
                                     message ("Duplicate case in switch: %s", 
                                              cname),
                                     current->loc);
@@ -6639,6 +7221,7 @@ checkSwitchExpr (exprNode test, /*@dependent@*/ exprNode e, /*@out@*/ bool *allp
                        g_currentloc);
 
          enumNameSList_free (unused);
+         *allpaths = FALSE; /* evans 2002-01-01 */
        }
       else
        {
@@ -6860,7 +7443,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
        {
@@ -6905,7 +7488,7 @@ exprNode exprNode_while (/*@keep@*/ exprNode t, /*@keep@*/ exprNode b)
   if (exprNode_isDefined (t) && exprNode_mustEscape (t))
     {
       voptgenerror
-       (FLG_CONTROL,
+       (FLG_ALWAYSEXITS,
         message ("Predicate always exits: %s", exprNode_unparse (t)),
         exprNode_loc (t));
     }
@@ -6951,12 +7534,15 @@ exprNode exprNode_while (/*@keep@*/ exprNode t, /*@keep@*/ exprNode b)
 exprNode exprNode_doWhile (/*@only@*/ exprNode b, /*@only@*/ exprNode t)
 {
   exprNode ret;
-  
+
+  DPRINTF (("Do while: %s / %s",
+           exprNode_unparse (b), exprNode_unparse (t)));
+
   if (exprNode_isError (t))
     {
       if (exprNode_isError (b))
        {
-         ret = exprNode_createLoc (ctype_unknown, g_currentloc);
+         ret = exprNode_createLoc (ctype_unknown, fileloc_copy (g_currentloc));
        }
       else
        {
@@ -6966,11 +7552,15 @@ exprNode exprNode_doWhile (/*@only@*/ exprNode b, /*@only@*/ exprNode t)
          exprNode_checkUse (ret, b->sref, b->loc);
          ret->exitCode = b->exitCode;
          ret->canBreak = b->canBreak;
-         ret->mustBreak = b->mustBreak;
+         ret->mustBreak = FALSE;
        }
     }
   else
     {
+      DPRINTF (("Do while: %s / %s",
+               exitkind_unparse (t->exitCode),
+               exitkind_unparse (b->exitCode)));
+
       ret = exprNode_createPartialCopy (t);
       exprNode_checkPred (cstring_makeLiteralTemp ("while"), t);
       
@@ -6991,9 +7581,16 @@ exprNode exprNode_doWhile (/*@only@*/ exprNode b, /*@only@*/ exprNode t)
          exprNode_mergeUSs (ret, t);
          exprNode_checkUse (ret, t->sref, t->loc);
 
-         ret->exitCode = b->exitCode;
+         /* evans 2001-10-05: while loop can break */
+         ret->exitCode = exitkind_makeConditional (b->exitCode);
+
+         DPRINTF (("Do while: %s",
+                   exitkind_unparse (ret->exitCode)));
+
          ret->canBreak = b->canBreak;
-         ret->mustBreak = b->mustBreak;
+
+         /* Always FALSE for doWhile loops - break's when test is false */
+         ret->mustBreak = FALSE; /* b->mustBreak; */
        }
     }
   
@@ -7001,7 +7598,78 @@ exprNode exprNode_doWhile (/*@only@*/ exprNode b, /*@only@*/ exprNode t)
 
   ret->kind = XPR_DOWHILE;
   ret->edata = exprData_makePair (t, b);
-    return ret;
+  return ret;
+}
+
+bool exprNode_loopMustExec (exprNode forPred)
+{
+  /*
+  ** Returns true if it is obvious that the loop always executes at least once
+  **
+  ** For now, we only identify the most obvious cases.  Should be true anytime
+  ** we can prove init => !test.
+  */
+
+  if (exprNode_isDefined (forPred))
+    {
+      exprNode init, test, inc;
+      exprData edata;
+
+      llassert (forPred->kind == XPR_FORPRED);
+      
+      edata = forPred->edata;
+      init = exprData_getTripleInit (edata);
+      test = exprData_getTripleTest (edata);
+      inc = exprData_getTripleInc (edata);
+      
+      if (exprNode_isAssign (init))
+       {
+         exprNode loopVar = exprData_getOpA (init->edata);
+         exprNode loopInit = exprData_getOpB (init->edata);
+
+         if (exprNode_isDefined (test) && test->kind == XPR_OP)
+           {
+             exprNode testVar = exprData_getOpA (test->edata);
+             exprNode testVal = exprData_getOpB (test->edata);
+             lltok comp = exprData_getOpTok (test->edata);
+             int opid = lltok_getTok (comp);
+
+             DPRINTF (("Same storage: %s / %s", exprNode_unparse (loopVar),
+                       exprNode_unparse (testVar)));
+             
+             if (exprNode_sameStorage (loopVar, testVar))
+               {
+                 multiVal valinit = exprNode_getValue (loopInit);
+                 multiVal valtest = exprNode_getValue (testVal);
+
+                 DPRINTF (("Values: %s / %s", multiVal_unparse (valinit), 
+                           multiVal_unparse (valtest)));
+
+                 if (multiVal_isInt (valinit) && multiVal_isInt (valtest))
+                   {
+                     long v1 = multiVal_forceInt (valinit);
+                     long v2 = multiVal_forceInt (valtest);
+
+                     DPRINTF (("Here: %ld %ld", v1, v2));
+                     
+                     if ((opid == EQ_OP && v1 < v2)
+                         || (opid == NE_OP && v1 != v2)
+                         || (opid == TLT && v1 <= v2)
+                         || (opid == TGT && v1 >= v2)
+                         || (opid == LE_OP && v1 < v2)
+                         || (opid == GE_OP && v1 > v2))
+                       {
+                         DPRINTF (("mustexec if inc"));
+                         return TRUE;
+                       }
+                   }
+               }
+           }
+       }
+    }
+
+  DPRINTF (("loop must exec: FALSE"));
+  return FALSE;
 }
 
 exprNode exprNode_for (/*@keep@*/ exprNode inc, /*@keep@*/ exprNode body)
@@ -7057,14 +7725,13 @@ exprNode exprNode_for (/*@keep@*/ exprNode inc, /*@keep@*/ exprNode body)
       
       ret->exitCode = exitkind_makeConditional (body->exitCode);
 
-            exprNode_mergeUSs (inc, body);
+      exprNode_mergeUSs (inc, body);
       
       if (exprNode_isDefined (inc))
        {
          exprNode tmp;
 
          context_setMessageAnnote (cstring_makeLiteral ("in post loop increment"));
-     
          
          tmp = exprNode_effect (exprData_getTripleInc (inc->edata));
          exprNode_freeShallow (tmp); 
@@ -7436,7 +8103,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
        {
@@ -7515,6 +8182,10 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val)
   ctype t2 = exprNode_getType (val);
   bool hasError = FALSE;
   
+  DPRINTF (("Check one init: %s / %s",
+           exprNode_unparse (el),
+           exprNode_unparse (val)));
+
   if (ctype_isUnknown (t1))
     {
       voptgenerror (FLG_IMPTYPE,
@@ -7529,12 +8200,43 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val)
   if (exprNode_isDefined (val) && val->kind == XPR_INITBLOCK)
     {
       exprNodeList vals = exprData_getArgs (val->edata);
+      
+      DPRINTF (("Check one init: %s", exprNodeList_unparse (vals)));
+      DPRINTF (("Type: %s", ctype_unparse (t1)));
 
       if (ctype_isRealAP (t1))
        {
          int i = 0;
          int nerrors = 0;
 
+         if (ctype_isFixedArray (t1))
+           {
+             int nelements = long_toInt (ctype_getArraySize (t1));
+             
+             DPRINTF (("Checked array: %s / %d",
+                       ctype_unparse (t1), nelements));
+
+             if (exprNode_isStringLiteral (val))
+               {
+                 exprNode_checkStringLiteralLength (t1, val);
+               }
+             else
+               {
+                 if (exprNodeList_size (vals) != nelements) 
+                   {
+                     hasError = optgenerror 
+                       (exprNodeList_size (vals) > nelements ? FLG_INITSIZE : FLG_INITALLELEMENTS,
+                        message ("Initializer block for "
+                                 "%s has %d element%&, but declared as %s: %q",
+                                 exprNode_unparse (el),
+                                 exprNodeList_size (vals),
+                                 ctype_unparse (t1),
+                                 exprNodeList_unparse (vals)),
+                        val->loc);       
+                   }
+               }
+           }
+         
          exprNodeList_elements (vals, oneval)
            {
              cstring istring = message ("%d", i);
@@ -7645,6 +8347,50 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val)
                } end_exprNodeList_elements;
            }
        }
+      /* evans 2001-12-30: added to fix bug reported by Jim Zelenka */
+      else if (ctype_isUnion (ctype_realType (t1)))
+       {
+         uentryList fields = ctype_getFields (t1);
+         int i = 0;
+
+         /*
+         ** Union initializers set the first member always.
+         */
+
+         DPRINTF (("Union initializer: %s / %s",
+                   exprNode_unparse (el), ctype_unparse (ctype_realType (t1))));
+
+         if (exprNodeList_size (vals) != 1)
+           {
+             hasError = optgenerror 
+               (FLG_TYPE,
+                message ("Initializer block for union "
+                         "%s has %d elements, union initializers should have one element: %q",
+                         exprNode_unparse (el),
+                         exprNodeList_size (vals),
+                         exprNodeList_unparse (vals)),
+                val->loc);       
+           }
+         else
+           {
+             exprNode oneval = exprNodeList_head (vals);
+             uentry thisfield = uentryList_getN (fields, i);
+             exprNode newel =
+               exprNode_fieldAccessAux (exprNode_fakeCopy (el),
+                                        exprNode_loc (el),
+                                        uentry_getName (thisfield));
+             
+             if (exprNode_isDefined (newel))
+               {
+                 if (exprNode_checkOneInit (newel, oneval))
+                   {
+                     hasError = TRUE;
+                   }
+                 
+                 exprNode_freeIniter (newel);
+               }
+           }
+       }
       else
        {
          hasError = optgenerror 
@@ -7677,11 +8423,13 @@ static bool exprNode_checkOneInit (/*@notnull@*/ exprNode el, exprNode val)
   return hasError;
 }
 
-static exprNode 
+static /*@notnull@*/ exprNode 
 exprNode_makeInitializationAux (/*@temp@*/ idDecl t)
 {
   exprNode ret;
 
+  DPRINTF (("Initialization: %s", idDecl_unparse (t)));
+
   if (usymtab_exists (idDecl_observeId (t)))
     {
       uentry ue = usymtab_lookup (idDecl_observeId (t));
@@ -7720,8 +8468,14 @@ 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 +8492,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 +8513,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 ();
@@ -7796,7 +8551,7 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t,
            {
              sRef_setDefState (lhs->sref, SS_PARTIAL, fileloc_undefined);
            }
-
+         
          (void) exprNode_checkOneInit (lhs, e);
 
          if (uentry_isStatic (ue))
@@ -7872,23 +8627,23 @@ exprNode exprNode_iter (/*@observer@*/ uentry name,
 
   if (uentry_isInvalid (end))
     {
-      llerror (FLG_ITER,
+      llerror (FLG_ITERBALANCE,
               message ("Iter %s not balanced with end_%s", iname, iname));
     }
   else
     {
       cstring ename = uentry_getName (end);
 
-      if (!cstring_equalPrefix (ename, "end_"))
+      if (!cstring_equalPrefixLit (ename, "end_"))
        {
-         llerror (FLG_ITER, message ("Iter %s not balanced with end_%s: %s", 
+         llerror (FLG_ITERBALANCE, message ("Iter %s not balanced with end_%s: %s", 
                                      iname, iname, ename));
        }
       else
        {
          if (!cstring_equal (iname, cstring_suffix (ename, 4)))
            {
-             llerror (FLG_ITER, 
+             llerror (FLG_ITERBALANCE
                       message ("Iter %s not balanced with end_%s: %s", 
                                iname, iname, ename));
            }
@@ -7939,7 +8694,7 @@ exprNode_iterNewId (/*@only@*/ cstring s)
   e->isJumpPoint = FALSE;
   e->exitCode = XK_NEVERESCAPE;
 
-  /*> missing fields, detected by lclint <*/
+  /*> missing fields, detected by splint <*/
   e->canBreak = FALSE;
   e->mustBreak = FALSE;
   e->etext = cstring_undefined;
@@ -8015,7 +8770,7 @@ exprNode_iterExpr (/*@returned@*/ exprNode e)
          if (fileloc_isDefined (e->loc))
            {
              voptgenerror
-               (FLG_ITER,
+               (FLG_ITERYIELD,
                 message ("Yield parameter is not simple identifier: %s", 
                          exprNode_unparse (e)),
                 e->loc);
@@ -8023,7 +8778,7 @@ exprNode_iterExpr (/*@returned@*/ exprNode e)
          else
            {
              voptgenerror
-               (FLG_ITER,
+               (FLG_ITERYIELD,
                 message ("Yield parameter is not simple identifier: %s",
                          exprNode_unparse (e)),
                 g_currentloc);
@@ -8066,7 +8821,7 @@ exprNode_iterId (/*@observer@*/ uentry c)
       if (!context_inHeader ())
        {
          if (optgenerror
-             (FLG_ITER,
+             (FLG_ITERYIELD,
               message ("Yield parameter shadows local declaration: %q",
                        uentry_getName (c)),
               fileloc_isDefined (e->loc) ? e->loc : g_currentloc))
@@ -8526,6 +9281,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 +9325,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:
@@ -8778,17 +9535,31 @@ static /*@only@*/ cstring exprNode_doUnparse (exprNode e)
       break;
       
     case XPR_BLOCK:
-      ret = message ("{ %s }", exprNode_unparseFirst (exprData_getSingle (data)));
+      ret = message ("{ %s }", exprNode_unparse (exprData_getSingle (data)));
+      /* evans 2002-02-20 was unparseFirst! */
       break;
 
     case XPR_STMT:
-      ret = cstring_copy (exprNode_unparse (exprData_getUopNode (data)));
+      ret = message ("%s;", exprNode_unparse (exprData_getUopNode (data)));
       break;
 
     case XPR_STMTLIST:
-      ret = message ("%s; %s", 
-                    exprNode_unparse (exprData_getPairA (data)),
-                    exprNode_unparse (exprData_getPairB (data)));
+      if (exprNode_isStatement (exprData_getPairA (data)))
+       {
+         /*
+         ** statement expressions already print the ;
+         */
+
+         ret = message ("%s %s", 
+                        exprNode_unparse (exprData_getPairA (data)),
+                        exprNode_unparse (exprData_getPairB (data)));
+       }
+      else
+       {
+         ret = message ("%s; %s", 
+                        exprNode_unparse (exprData_getPairA (data)),
+                        exprNode_unparse (exprData_getPairB (data)));
+       }
       break;
       
     case XPR_FTDEFAULT:
@@ -8834,7 +9605,14 @@ static /*@only@*/ cstring exprNode_doUnparse (exprNode e)
       break;
 
     case XPR_STRINGLITERAL:
-      ret = message ("\"%s\"", exprData_getLiteral (data));
+      if (ctype_isWideString (e->typ))
+       {
+         ret = message ("L\"%s\"", exprData_getLiteral (data));
+       }
+      else
+       {
+         ret = message ("\"%s\"", exprData_getLiteral (data));
+       }
       break;
 
     case XPR_NUMLIT:
@@ -8963,7 +9741,22 @@ exprNode_matchLiteral (ctype expected, exprNode e)
                }
              else if (ctype_isArrayPtr (expected))
                {
-                 return (val == 0);
+                 /* 
+                 ** evans 2001-10-14: We allow 0 to match any pointer, but only if the type matches or is void *.
+                 */
+
+                 if (val == 0)
+                   {
+                     if (ctype_match (exprNode_getType (e), expected)
+                         || ctype_isVoidPointer (exprNode_getType (e)))
+                       {
+                         return TRUE;
+                       }
+                   }
+                 else
+                   {
+                     return FALSE;
+                   }
                }
              else if (ctype_isAnyFloat (expected))
                {
@@ -9046,6 +9839,10 @@ exprNode_matchTypes (exprNode e1, exprNode e2)
       return TRUE;
     }
 
+  DPRINTF (("Matching literal! %s %s %s %s",
+           ctype_unparse (t1), exprNode_unparse (e2),
+           ctype_unparse (t2), exprNode_unparse (e1)));
+
   return (exprNode_matchLiteral (t1, e2) || exprNode_matchLiteral (t2, e1));
 }
 
@@ -9231,7 +10028,7 @@ exprNode_checkUse (exprNode e, /*@exposed@*/ sRef s, fileloc loc)
          
          while (sRef_isValid (s) && sRef_isKnown (s))
            {
-             ynm readable = sRef_isReadable (s);
+             ynm readable = sRef_isValidLvalue (s);
 
              DPRINTF (("Readable: %s / %s",
                        sRef_unparseFull (s), ynm_unparse (readable)));
@@ -9242,6 +10039,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 +10055,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 +10136,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 +10194,7 @@ exprNode_checkSet (exprNode e, /*@exposed@*/ sRef s)
        }
      
       if (sRef_isMeaningful (s))
-       {
-         
+       {         
          if (sRef_isDead (s))
            {
              sRef base = sRef_getBaseSafe (s);
@@ -9589,7 +10389,7 @@ checkOneArg (uentry ucurrent, /*@notnull@*/ exprNode current,
            }
        }
       
-      checkPassTransfer (current, ucurrent, isSpec, fcn, argno, totargs);
+      transferChecks_passParam (current, ucurrent, isSpec, fcn, argno, totargs);
       exprNode_mergeUSs (fcn, current);
     }
 }
@@ -9756,7 +10556,9 @@ static ctype
       if ((ctype_isRealInt (tr1) || ctype_isReal (tr1)) &&
          (ctype_isRealInt (tr2) || ctype_isReal (tr2)))
        {
-         ;
+         DPRINTF (("No error: [%s] %s / [%s]  %s",
+                   exprNode_unparse (e1), ctype_unparse (tr1),
+                   exprNode_unparse (e2), ctype_unparse (tr2)));
        }
       else
        {
@@ -9964,9 +10766,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))
            {
@@ -10065,6 +10870,10 @@ checkOneRepExpose (sRef ysr, sRef base,
 static void
 doAssign (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2, bool isInit)
 {
+  DPRINTF (("Do assign: %s <- %s",
+           exprNode_unparse (e1), exprNode_unparse (e2)));
+  DPRINTF (("Ctype: %s", ctype_unparse (exprNode_getType (e1))));
+
   if (ctype_isRealFunction (exprNode_getType (e1))
       && !ctype_isRealPointer (exprNode_getType (e1)))
     {
@@ -10174,11 +10983,11 @@ doAssign (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2, bool isInit)
        {
            DPRINTF (("Check init: %s / %s",
                      exprNode_unparse (e1), exprNode_unparse (e2)));
-         checkInitTransfer (e1, e2); 
+         transferChecks_initialization (e1, e2); 
        }
       else
        {
-         checkAssignTransfer (e1, e2); 
+         transferChecks_assign (e1, e2); 
        }
     }
   else
@@ -10212,6 +11021,11 @@ doAssign (/*@notnull@*/ exprNode e1, /*@notnull@*/ exprNode e2, bool isInit)
       }
     }
 
+  if (exprNode_isStringLiteral (e2))
+    {
+      exprNode_checkStringLiteralLength (exprNode_getType (e1), e2);
+    }
+
   if (isInit && sRef_isFileOrGlobalScope (e1->sref))
     {
        ;
@@ -10449,6 +11263,7 @@ long exprNode_getLongValue (exprNode e) {
     }
   else
     {
+      /*@!! BADBRANCH;*/
       value = 0;
     }
   
@@ -10475,8 +11290,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 +11305,8 @@ exprNode exprNode_createNew(ctype c)
 
   return ret;
 }
+
+bool exprNode_isInitBlock (exprNode e)
+{
+  return (exprNode_isDefined(e) && e->kind == XPR_INITBLOCK);
+}
This page took 0.908383 seconds and 4 git commands to generate.