]> andersk Git - splint.git/blobdiff - src/uentry.c
Fix DPRINTF bit rot.
[splint.git] / src / uentry.c
index 06be66a73ca4641f1d7328417c8d42798cc4c39e..6f6c090418b3d845ba98e15c61dbd242a24f8d22 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-2003 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
 */
 /*
 ** uentry.c
 */
 
-# include "lclintMacros.nf"
+# include "splintMacros.nf"
 # include "basic.h"
 # include "structNames.h"
 # include "nameChecks.h"
@@ -43,6 +43,8 @@ static bool uentry_isReallySpecified (uentry p_e) /*@*/ ;
 static void uentry_checkIterArgs (uentry p_ue);
 static cstring uentry_dumpAux (uentry p_v, bool p_isParam);
 
+static void uentry_showWhereLastKind (uentry p_spec) /*@modifies g_warningstream@*/ ; 
+
 static void uentry_combineModifies (uentry p_ue, /*@owned@*/ sRefSet p_sr) 
      /*@modifies p_ue@*/ ;
 
@@ -64,10 +66,8 @@ static void checkVarConformance (/*@notnull@*/ uentry p_old,
                                 bool p_mustConform, bool p_completeConform) 
    /*@modifies p_old, p_unew@*/;
 
-# ifndef NOLCL
 static void uentry_setHasMods (uentry p_ue) /*@modifies p_ue@*/;
 static void uentry_setHasGlobs (uentry p_ue) /*@modifies p_ue@*/;
-# endif
 
 static void uentry_reallyFree (/*@notnull@*/ /*@only@*/ uentry p_e);
 
@@ -84,16 +84,31 @@ static void
   paramTypeError (/*@notnull@*/ uentry p_old, /*@notnull@*/ uentry p_oldCurrent,
                  ctype p_oldType, /*@notnull@*/ uentry p_unew,
                  /*@notnull@*/ uentry p_newCurrent, 
-                 ctype p_newType, int p_paramno) /*@modifies g_msgstream@*/ ;
+                 ctype p_newType, int p_paramno) /*@modifies g_warningstream@*/ ;
 
 static /*@only@*/ /*@notnull@*/ uentry 
   uentry_makeVariableAux (cstring p_n, ctype p_t, /*@keep@*/ fileloc p_f,
                          /*@exposed@*/ sRef p_s, bool p_priv, vkind p_kind);
 
+static /*@only@*/ /*@notnull@*/ uentry 
+  uentry_makeConstantAux (cstring p_n, ctype p_t, 
+                         /*@keep@*/ fileloc p_f, bool p_priv, bool p_macro,
+                         /*@only@*/ multiVal p_m) /*@*/ ;
+
+static void uentry_convertVarFunction (uentry ue) /*@modifies ue@*/
+{
+  if (uentry_isVariable (ue) 
+      && (ctype_isFunction (ctype_realType (uentry_getType (ue)))
+         || ctype_isUnknown (uentry_getType (ue))))
+    {
+      uentry_makeVarFunction (ue);
+    }
+}
+
 static /*@out@*/ /*@notnull@*/ uentry uentry_alloc (void) /*@*/ 
 {
   uentry ue = (uentry) dmalloc (sizeof (*ue));
-  ue->warn = warnClause_undefined; /*@i32@*/
+  ue->warn = warnClause_undefined; 
   nuentries++;
   totuentries++;
   
@@ -101,11 +116,13 @@ static /*@out@*/ /*@notnull@*/ uentry uentry_alloc (void) /*@*/
 }
 
 static cstring uentry_getOptName (uentry p_e) /*@*/ ;
-static void uentry_copyInto (/*@out@*/ /*@unique@*/ uentry p_unew, uentry p_old);
+static void uentry_updateInto (/*@unique@*/ uentry p_unew, uentry p_old) /*@modifies p_unew, p_old@*/ ;
+
 static void uentry_setNullState (/*@notnull@*/ uentry p_ue, nstate p_ns);
 static void uentry_setAliasKind (/*@notnull@*/ uentry p_ue, alkind p_ak);
 static /*@only@*/ /*@null@*/ uinfo uinfo_copy (uinfo p_u, ekind p_kind);
 static void uinfo_free (/*@only@*/ uinfo p_u, ekind p_kind);
+static void ucinfo_free (/*@only@*/ ucinfo p_u);
 static void uvinfo_free (/*@only@*/ uvinfo p_u);
 
 # ifdef DOANNOTS
@@ -552,110 +569,72 @@ static /*@observer@*/ cstring uentry_reDefDecl (uentry old, uentry unew)  /*@*/
     }
 }
 
-
-/*drl7x*/
-/*@only@*/ constraintList uentry_getFcnPreconditions (uentry ue)
+static constraintList uentry_getFunctionConditions (uentry ue, bool isPost)
 {
   if (uentry_isValid (ue))
     {
+      functionConstraint constraint;
+
+      DPRINTF((message ("called uentry_getFcnPostconditions on  %s",
+                        uentry_unparse (ue) ) ) );
+      
+      if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
        {
-         if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
+         DPRINTF((message ("called uentry_getFunctionConditions on nonfunction %s",
+                            uentry_unparse (ue) ) ) );
+         if (!uentry_isFunction (ue) )
            {
-             DPRINTF(( (message( "Function pointer %s not doing  uentry_getFcnPreconditions", uentry_unparse(ue) )) ));
-             //  uentry_makeVarFunction (ue);
+             DPRINTF((message ("called uentry_getFunctionConditions on nonfunction %s",
+                               uentry_unparse (ue) ) ));
+             return constraintList_undefined;
            }
-
-         //llassert (uentry_isFunction (ue));
-         //llassert ((ue->info->fcn->preconditions));
-  //llassert ((ue->info->fcn->preconditions));
-         if (!uentry_isFunction (ue))
-           {
-             DPRINTF( (message ("called uentry_getFcnPreconditions on nonfunction %s",
-                                 uentry_unparse (ue) ) ) );
-                 if (!uentry_isSpecified (ue) )
-                   {
-                     DPRINTF((message ("called uentry_getFcnPreconditions on nonfunction %s",
-                                       uentry_unparse (ue) ) ));
-                     return constraintList_undefined;
-                   }
          
+         
+         return constraintList_undefined;
+       }
+      
+      if (!uentry_isFunction(ue))
+       {
+         
+         DPRINTF((message ("called uentry_getFunctionConditions on non function  %s",
+                            uentry_unparse (ue) ) ) );
+         return constraintList_undefined;
+         
+       }
 
-                 return constraintList_undefined;
-           }
+      llassert (uentry_isFunction (ue));
 
-         if (constraintList_isDefined(ue->info->fcn->preconditions))
-           {
-          return constraintList_copy (ue->info->fcn->preconditions);
-           }
-         else
-           {
-             return NULL;
-           }
+      if (isPost)
+       {
+         constraint = ue->info->fcn->postconditions;
        }
-       
+      else
+       {
+         constraint = ue->info->fcn->preconditions;
+       }
+
+      return functionConstraint_getBufferConstraints (constraint);
     }
   
   return constraintList_undefined;
   
 }
 
-
-
+/*drl7x*/
+/*@only@*/ constraintList uentry_getFcnPreconditions (uentry ue)
+{
+  return uentry_getFunctionConditions (ue, FALSE);
+}
 
 /*drl
   12/28/2000
 */
+
 constraintList uentry_getFcnPostconditions (uentry ue)
 {
-  if (uentry_isValid (ue))
-    {
-      DPRINTF( (message ("called uentry_getFcnPostconditions on  %s",
-                                 uentry_unparse (ue) ) ) );
-       {
-         if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
-           {
-             DPRINTF( (message ("called uentry_getFcnPostconditions on nonfunction %s",
-                                 uentry_unparse (ue) ) ) );
-             if (!uentry_isFunction (ue) )
-               {
-                 DPRINTF((message ("called uentry_getFcnPostconditions on nonfunction %s",
-                                       uentry_unparse (ue) ) ));
-                     return constraintList_undefined;
-                   }
-         
-
-                 return constraintList_undefined;
-           }
-
-         //  llassert (uentry_isFunction (ue));
-         if (!uentry_isFunction(ue) )
-           {
-             
-             DPRINTF( (message ("called uentry_getFcnPostconditions on non function  %s",
-                                 uentry_unparse (ue) ) ) );
-               return constraintList_undefined;
-
-           }
-         if (constraintList_isDefined(ue->info->fcn->postconditions) )
-           {
-             DPRINTF((message ("called uentry_getFcnPostconditions on %s and returned %q",
-                               uentry_unparse (ue),
-                               constraintList_print(ue->info->fcn->postconditions) ) ));
-          return constraintList_copy (ue->info->fcn->postconditions);
-           }
-         else
-           {
-             return NULL;
-           }
-       }
-       
-    }
-  
-  return constraintList_undefined;
-  
+  return uentry_getFunctionConditions (ue, TRUE);
 }
 
-
 static /*@only@*/ fileloc setLocation (void)
 {
   fileloc fl = context_getSaveLocation ();
@@ -670,6 +649,12 @@ static /*@only@*/ fileloc setLocation (void)
     }
 }
 
+static void uentry_setConstantValue (uentry ue, /*@only@*/ multiVal val)
+{
+  llassert (uentry_isEitherConstant (ue));
+  sRef_setValue (ue->sref, val);
+}
+
 /*@notnull@*/ uentry uentry_makeEnumConstant (cstring n, ctype t)
 {
   fileloc loc = setLocation ();
@@ -700,7 +685,6 @@ static /*@only@*/ fileloc setLocation (void)
   return ue;
 }
 
-# ifndef NOLCL
 /*@notnull@*/ uentry uentry_makeSpecEnumConstant (cstring n, ctype t, fileloc loc)
 {
   uentry ue = uentry_makeConstant (n, t, loc);
@@ -708,29 +692,32 @@ static /*@only@*/ fileloc setLocation (void)
   ue->ukind = KENUMCONST;
   return ue;
 }
-# endif
 
 /*@notnull@*/ uentry uentry_makeVariableLoc (cstring n, ctype t)
 {
   return uentry_makeVariable (n, t, setLocation (), FALSE);
 }
 
-# ifndef NOLCL
+bool uentry_isUnnamedVariable (uentry ue)
+{
+  return uentry_isVariable (ue) && cstring_isUndefined (ue->uname);
+}
+
 /*@notnull@*/ /*@only@*/ uentry uentry_makeUnnamedVariable (ctype t)
 {
   return uentry_makeVariable (cstring_undefined, t, setLocation (), FALSE);
 }
-# endif
 
 /*@notnull@*/ uentry uentry_makeIdDatatype (idDecl id)
 {
   ctype ct = idDecl_getCtype (id);
   uentry ue = uentry_makeDatatype (idDecl_observeId (id), ct, 
-                                  MAYBE, MAYBE, setLocation ());
+                                  MAYBE, qual_createUnknown (),
+                                  setLocation ());
 
   uentry_reflectQualifiers (ue, idDecl_getQuals (id));
   
-  if (!ynm_isOn (ue->info->datatype->abs))
+  if (!qual_isEitherAbstract (ue->info->datatype->abs))
     {
       if (ctype_isUnknown (ct))
        {
@@ -754,15 +741,22 @@ void uentry_checkParams (uentry ue)
       if (uentry_isRealFunction (ue))
        {
          uentryList params = uentry_getParams (ue);
+         int paramno = 0;
 
          uentryList_elements (params, current)
            {
+             paramno++;
+
              if (uentry_isValid (current))
                {
                  ctype ct = current->utype;                  
                  
                  if (ctype_isFixedArray (ct))
                    {
+                     DPRINTF (("Array: %s / %s",
+                               ctype_unparse (ct),
+                               ctype_unparse (ctype_baseArrayPtr (ct))));
+
                      if (ctype_isArray (ctype_baseArrayPtr (ct))
                          && !ctype_isFixedArray (ctype_baseArrayPtr (ct)))
                        {
@@ -770,24 +764,48 @@ void uentry_checkParams (uentry ue)
                        }
                      else
                        {
-                         voptgenerror 
-                           (FLG_FIXEDFORMALARRAY,
-                            message ("Function parameter %q declared as "
-                                     "manifest array (size constant is meaningless)",
-                                     uentry_getName (current)),
-                            uentry_whereDeclared (current));
+                         if (uentry_hasName (current))
+                           {
+                             voptgenerror 
+                               (FLG_FIXEDFORMALARRAY,
+                                message ("Function parameter %q declared as "
+                                         "manifest array (size constant is meaningless)",
+                                         uentry_getName (current)),
+                                uentry_whereDeclared (current));
+                           }
+                         else
+                           {
+                             voptgenerror 
+                               (FLG_FIXEDFORMALARRAY,
+                                message ("Unnamed function parameter %d declared as "
+                                         "manifest array (size constant is meaningless)",
+                                         paramno),
+                                uentry_whereDeclared (current));
+                           }
                        }
                    }
                  else 
                    {
                      if (ctype_isArray (ct))
                        {
-                         voptgenerror 
-                           (FLG_FORMALARRAY,
-                            message ("Function parameter %q declared as "
-                                     "array (treated as pointer)", 
-                                     uentry_getName (current)),
-                            uentry_whereDeclared (current));
+                         if (uentry_hasName (current))
+                           {
+                             voptgenerror 
+                               (FLG_FORMALARRAY,
+                                message ("Function parameter %q declared as "
+                                         "array (treated as pointer)", 
+                                         uentry_getName (current)),
+                                uentry_whereDeclared (current));
+                           }
+                         else
+                           {
+                             voptgenerror 
+                               (FLG_FORMALARRAY,
+                                message ("Unnamed function parameter %d declared as "
+                                         "array (treated as pointer)", 
+                                         paramno),
+                                uentry_whereDeclared (current));
+                           }
                        }
                    }
 
@@ -881,7 +899,8 @@ static void reflectImplicitFunctionQualifiers (/*@notnull@*/ uentry ue, bool spe
                        }
                      else 
                        {
-                         if (ctype_isImmutableAbstract (ctype_getReturnType (ue->utype))) 
+                         if (ctype_isImmutableAbstract (ctype_getReturnType (ue->utype))
+                             || ctype_isNumAbstract (ctype_getReturnType (ue->utype)))
                            {
                              ; /* Immutable objects are not shared. */
                            }
@@ -912,7 +931,7 @@ uentry_makeFunctionAux (cstring n, ctype t,
   uentry e = uentry_alloc ();
   ctype ret;
 
-  llassert (warnClause_isUndefined (warn)); /*@i325 remove parameter! */
+  llassert (warnClause_isUndefined (warn)); 
 
   if (ctype_isFunction (t))
     {
@@ -945,7 +964,9 @@ uentry_makeFunctionAux (cstring n, ctype t,
   e->utype = t;
   e->storageclass = SCNONE;
 
-    e->sref = sRef_makeType (ret);
+  e->sref = sRef_makeResult (ret); /* evans 2001-07-19 - was sRef_makeType */
+
+  DPRINTF (("Result: %s", sRef_unparseFull (e->sref)));
 
   if (ctype_isUA (ret))
     {
@@ -1040,18 +1061,24 @@ static void uentry_reflectClauses (uentry ue, functionClauseList clauses)
 
          if (uentry_hasGlobs (ue))
            {
-             voptgenerror 
+             vgenhinterror 
                (FLG_SYNTAX,
                 message
                 ("Multiple globals clauses for %q: %q",
                  uentry_getName (ue),
                  globalsClause_unparse (glc)),
+                cstring_makeLiteral ("Only one globals clause may be used. The second globals clause is ignored."),
                 globalsClause_getLoc (glc));
-             uentry_setGlobals (ue, globalsClause_takeGlobs (glc)); /*@i32@*/
+
+             /*                
+               uentry_setGlobals (ue, globalsClause_takeGlobs (glc)); 
+             */
            }
          else
            {
+             DPRINTF (("Taking globs: %s", globalsClause_unparse (glc)));
              uentry_setGlobals (ue, globalsClause_takeGlobs (glc));
+             DPRINTF (("Taking globs after: %s", globalsClause_unparse (glc)));
            }
        }
       else if (functionClause_isModifies (el))
@@ -1080,16 +1107,54 @@ static void uentry_reflectClauses (uentry ue, functionClauseList clauses)
              **
              */
 
-             uentry_combineModifies (ue, modifiesClause_takeMods (mlc)); /*@i32@*/
+             uentry_combineModifies (ue, modifiesClause_takeMods (mlc)); 
            }
          else
            {
              uentry_setModifies (ue, modifiesClause_takeMods (mlc));
            }
        }
+      else if (functionClause_isEnsures (el))
+       {
+         functionConstraint cl = functionClause_takeEnsures (el);
+         DPRINTF (("Setting post: %s / %s",
+                   uentry_unparse (ue), functionConstraint_unparse (cl)));
+         uentry_setPostconditions (ue, cl);
+       }
+      else if (functionClause_isRequires (el))
+       {
+         functionConstraint cl = functionClause_takeRequires (el);
+         uentry_setPreconditions (ue, cl);
+       }
       else if (functionClause_isState (el))
        {
          stateClause sc = functionClause_takeState (el);
+
+         if (stateClause_isBefore (sc) && stateClause_setsMetaState (sc))
+           {
+             sRefSet rfs = stateClause_getRefs (sc);
+
+             sRefSet_elements (rfs, s)
+               {
+                 if (sRef_isParam (s))
+                   {
+                     /* 
+                     ** Can't use requires on parameters
+                     */
+                     
+                     voptgenerror
+                       (FLG_ANNOTATIONERROR,
+                        message ("Requires clauses for %q concerns parameters %q should be "
+                                 "a parameter annotation instead: %q",
+                                 uentry_unparse (ue),
+                                 sRef_unparse (s),
+                                 stateClause_unparse (sc)),
+                        stateClause_loc (sc));
+                   }
+               } end_sRefSet_elements ;
+           }
+
+         DPRINTF (("State clause: %s", stateClause_unparse (sc)));
          uentry_addStateClause (ue, sc);
        }
       else if (functionClause_isWarn (el))
@@ -1103,6 +1168,7 @@ static void uentry_reflectClauses (uentry ue, functionClauseList clauses)
        }
     } end_functionClauseList_elements ;
 
+  DPRINTF (("Checking all: %s", sRef_unparseFull (ue->sref)));
   stateClauseList_checkAll (ue);
 }
 
@@ -1115,6 +1181,8 @@ static void uentry_reflectClauses (uentry ue, functionClauseList clauses)
                         sRefSet_undefined, warnClause_undefined,
                         setLocation ());
 
+  DPRINTF (("Id function: %s", sRef_unparseFull (ue->sref)));
+
   /*
   ** This makes parameters names print out correctly.
   ** (But we might be a local variable declaration for a function type...)
@@ -1132,10 +1200,13 @@ static void uentry_reflectClauses (uentry ue, functionClauseList clauses)
       leaveFunc = TRUE;
     }
 
+  DPRINTF (("Id function: %s", sRef_unparseFull (ue->sref)));
   uentry_reflectQualifiers (ue, idDecl_getQuals (id));
+  DPRINTF (("Id function: %s", sRef_unparseFull (ue->sref)));
   reflectImplicitFunctionQualifiers (ue, FALSE);
-
+  DPRINTF (("Id function: %s", sRef_unparseFull (ue->sref)));
   uentry_reflectClauses (ue, idDecl_getClauses (id));
+  DPRINTF (("Id function: %s", sRef_unparseFull (ue->sref)));
 
   if (!uentry_isStatic (ue)
       && cstring_equalLit (ue->uname, "main"))
@@ -1244,13 +1315,14 @@ static void uentry_implicitParamAnnots (/*@notnull@*/ uentry e)
 }
 
 static /*@only@*/ /*@notnull@*/ uentry 
-uentry_makeVariableParamAux (cstring n, ctype t, /*@dependent@*/ sRef s, sstate defstate) /*@i32 exposed*/
+uentry_makeVariableParamAux (cstring n, ctype t, /*@dependent@*/ sRef s, 
+                            /*@only@*/ fileloc loc, sstate defstate)
 {
   cstring pname = makeParam (n);
   uentry e;
 
   DPRINTF (("Sref: %s", sRef_unparseFull (s)));
-  e = uentry_makeVariableAux (pname, t, setLocation (), s, FALSE, VKPARAM);
+  e = uentry_makeVariableAux (pname, t, loc, s, FALSE, VKPARAM);
 
   cstring_free (pname);
   DPRINTF (("Param: %s", uentry_unparseFull (e)));
@@ -1268,7 +1340,6 @@ uentry_makeVariableParamAux (cstring n, ctype t, /*@dependent@*/ sRef s, sstate
   return (e);
 }
 
-# ifndef NOLCL
 void
 uentry_setRefCounted (uentry e)
 {
@@ -1278,7 +1349,6 @@ uentry_setRefCounted (uentry e)
       sRef_storeState (e->sref);
     }
 }
-# endif
 
 void
 uentry_setStatic (uentry c)
@@ -1382,9 +1452,9 @@ void checkGlobalsModifies (/*@notnull@*/ uentry ue, sRefSet sr)
 }
 
 uentry
-uentry_makeVariableSrefParam (cstring n, ctype t, /*@exposed@*/ sRef s)
+uentry_makeVariableSrefParam (cstring n, ctype t, /*@only@*/ fileloc loc, /*@exposed@*/ sRef s)
 {
-  return (uentry_makeVariableParamAux (n, t, s, SS_UNKNOWN));
+  return (uentry_makeVariableParamAux (n, t, s, loc, SS_UNKNOWN));
 }
 
 void
@@ -1407,16 +1477,17 @@ uentry_fixupSref (uentry ue)
   
   if (uentry_isVariable (ue))
     {
+      /* removed this: no need to copy? ue->sref = sRef_saveCopyShallow (ue->info->var->origsref); */
       sRef_setDefState (sr, ue->info->var->defstate, fileloc_undefined);
       sRef_setNullState (sr, ue->info->var->nullstate, fileloc_undefined);
     }
 }
 
-static void uentry_addStateClause (uentry ue, stateClause sc)
+static void uentry_addStateClause (/*@notnull@*/ uentry ue, stateClause sc)
 {
   /*
   ** Okay to allow multiple clauses of the same kind.
-  */ /*@i834 is this true?@*/
+  */ 
 
   ue->info->fcn->specclauses = 
     stateClauseList_add (ue->info->fcn->specclauses, sc);
@@ -1484,11 +1555,7 @@ uentry_setModifies (uentry ue, /*@owned@*/ sRefSet sr)
        }
       else
        {
-         if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
-           {
-             uentry_makeVarFunction (ue);
-           }
-         
+         uentry_convertVarFunction (ue);
          llassertfatal (uentry_isFunction (ue));
          llassert (sRefSet_isUndefined (ue->info->fcn->mods));
          
@@ -1561,12 +1628,13 @@ bool uentry_hasWarning (uentry ue)
 
 void uentry_addWarning (uentry ue, /*@only@*/ warnClause warn)
 {
+  llassert (uentry_isValid (ue));
   llassert (warnClause_isUndefined (ue->warn));
   ue->warn = warn;
 }
 
 void
-uentry_setPreconditions (uentry ue, /*@only@*/ constraintList preconditions)
+uentry_setPreconditions (uentry ue, /*@only@*/ functionConstraint preconditions)
 {
   if (sRef_modInFunction ())
     {
@@ -1580,28 +1648,36 @@ uentry_setPreconditions (uentry ue, /*@only@*/ constraintList preconditions)
 
   if (uentry_isValid (ue))
     {
+      uentry_convertVarFunction (ue);
+      llassertfatal (uentry_isFunction (ue));
+      
+      if (functionConstraint_isDefined (ue->info->fcn->preconditions))
+       {
+         /*drl oops this date is wronge...*/
+         /* drl 11-29-2002
+            I changed this so it didn't appear as a Splint bug
+            among other things this gets triggered when there is
+            a function with two requires clauses.  Now Splint
+            prints an error and tries to conjoin the lists.
+         */
+      llparseerror
+       (message ("Duplicate precondition list"
+                 "Attemping the conjoin the requires clauses"
+                 ));
+
+
+         /* should conjoin constraints? */
+         /*@notreached@*/ 
+         ue->info->fcn->preconditions = functionConstraint_conjoin (ue->info->fcn->preconditions, preconditions);
+       }
+      else
        {
-         if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
-           {
-             uentry_makeVarFunction (ue);
-           }
-         
-         llassertfatal (uentry_isFunction (ue));
-         //      llassert (sRefSet_isUndefined (ue->info->fcn->mods));
-       
-         if (constraintList_isDefined(ue->info->fcn->preconditions) )
-           {
-             constraintList_free(ue->info->fcn->preconditions);
-             ue->info->fcn->preconditions = preconditions;
-           }
-         else
-             ue->info->fcn->preconditions = preconditions;
+         ue->info->fcn->preconditions = preconditions;
        }
-       
     }
   else
     {
-      llfatalbug ( (message("uentry_setPreconditions called with invalid uentry") ));
+      llfatalbug ((message("uentry_setPreconditions called with invalid uentry") ));
     }
 }
 
@@ -1610,7 +1686,7 @@ uentry_setPreconditions (uentry ue, /*@only@*/ constraintList preconditions)
   added 12/28/2000
 */
 void
-uentry_setPostconditions (uentry ue, /*@only@*/ constraintList postconditions)
+uentry_setPostconditions (uentry ue, /*@only@*/ functionConstraint postconditions)
 {
   if (sRef_modInFunction ())
     {
@@ -1618,35 +1694,27 @@ uentry_setPostconditions (uentry ue, /*@only@*/ constraintList postconditions)
        (message ("Postcondition list not in function context.  "
                  "A postcondition list can only appear following the parameter list "
                  "in a function declaration or header."));
-
+      
       /*@-mustfree@*/ return; /*@=mustfree@*/ 
     }
 
   if (uentry_isValid (ue))
     {
+      uentry_convertVarFunction (ue);
+      llassertfatal (uentry_isFunction (ue));
+      
+      if (functionConstraint_isUndefined (ue->info->fcn->postconditions))
        {
-         if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
-           {
-             uentry_makeVarFunction (ue);
-           }
-         
-         llassertfatal (uentry_isFunction (ue));
-         //      llassert (sRefSet_isUndefined (ue->info->fcn->mods));
-
-         if (constraintList_isUndefined(ue->info->fcn->postconditions) )
-                 ue->info->fcn->postconditions = postconditions;
-         else
-           {
-           constraintList_free(ue->info->fcn->postconditions);
-           ue->info->fcn->postconditions = postconditions;
-           }       
-
+         ue->info->fcn->postconditions = postconditions;
        }
-       
+      else
+       {
+         ue->info->fcn->postconditions = functionConstraint_conjoin (ue->info->fcn->postconditions, postconditions);
+       }           
     }
   else
     {
-      llfatalbug ( (message("uentry_setPostconditions called with invalid uentry") ));
+      llfatalbug ((message("uentry_setPostconditions called with invalid uentry") ));
     }
 }
 
@@ -2281,6 +2349,7 @@ uentry_reflectOtherQualifier (/*@notnull@*/ uentry ue, qual qel)
       uentry_setNullState (ue, NS_MNOTNULL);
     }
   else if (qual_isAbstract (qel)
+          || qual_isNumAbstract (qel)
           || qual_isConcrete (qel))
     {
       if (!uentry_isDatatype (ue))
@@ -2293,7 +2362,9 @@ uentry_reflectOtherQualifier (/*@notnull@*/ uentry ue, qual qel)
        }
       else
        {
-         ue->info->datatype->abs = ynm_fromBool (qual_isAbstract (qel));
+         ue->info->datatype->abs = qel;
+         DPRINTF (("Setting abstract %s: %s",
+                   uentry_unparse (ue), qual_unparse (qel)));
        }
     }
   else if (qual_isMutable (qel))
@@ -2331,11 +2402,8 @@ uentry_reflectOtherQualifier (/*@notnull@*/ uentry ue, qual qel)
     }
   else if (qual_isNullPred (qel))
     {
-      if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
-       {
-         uentry_makeVarFunction (ue);
-       }
-      
+      uentry_convertVarFunction (ue);
+
       if (uentry_isFunction (ue))
        {
          ctype typ = uentry_getType (ue);
@@ -2430,12 +2498,12 @@ uentry_reflectOtherQualifier (/*@notnull@*/ uentry ue, qual qel)
        {
          if (optgenerror
              (FLG_ANNOTATIONERROR,
-              message ("Meta state anntation %s used in inconsistent context: %q",
+              message ("Attribute annotation %s used in inconsistent context: %q",
                        qual_unparse (qel),
                        uentry_unparse (ue)),
               uentry_whereLast (ue)))
            {
-             /*@i! annotationInfo_showContextError (ainfo, ue); */
+             /* annotationInfo_showContextError (ainfo, ue); */
            }
        }
     }
@@ -2457,6 +2525,9 @@ uentry_reflectQualifiers (uentry ue, qualList q)
 {
   llassert (uentry_isValid (ue)); 
 
+  DPRINTF (("Reflect qualifiers: %s / %s",
+           uentry_unparseFull (ue), qualList_unparse (q)));
+
   qualList_elements (q, qel)
     {
       if (qual_isStatic (qel))
@@ -2466,6 +2537,7 @@ uentry_reflectQualifiers (uentry ue, qualList q)
       else if (qual_isUnused (qel))
        {
          uentry_setUsed (ue, fileloc_undefined);         
+         DPRINTF (("Used: %s", uentry_unparseFull (ue)));
        }
       else if (qual_isExternal (qel))
        {
@@ -2777,6 +2849,8 @@ uentry_reflectQualifiers (uentry ue, qualList q)
     } end_qualList_elements;
 
   qualList_clear (q);
+
+  DPRINTF (("Done: %s", sRef_unparseFull (ue->sref)));
 }
        
 bool
@@ -2964,11 +3038,7 @@ static void checkSpecialFunction (/*@notnull@*/ uentry ue)
 void
 uentry_setPrintfLike (uentry ue)
 {
-  if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
-    {
-      uentry_makeVarFunction (ue);
-    }
-  
+  uentry_convertVarFunction (ue);
   llassertfatal (uentry_isFunction (ue));
   ue->info->fcn->specialCode = SPC_PRINTFLIKE;
   checkSpecialFunction (ue);
@@ -2977,11 +3047,7 @@ uentry_setPrintfLike (uentry ue)
 void
 uentry_setScanfLike (uentry ue)
 {
-  if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
-    {
-      uentry_makeVarFunction (ue);
-    }
-  
+  uentry_convertVarFunction (ue);
   llassertfatal (uentry_isFunction (ue));
   ue->info->fcn->specialCode = SPC_SCANFLIKE;
   checkSpecialFunction (ue);
@@ -2990,11 +3056,7 @@ uentry_setScanfLike (uentry ue)
 void
 uentry_setMessageLike (uentry ue)
 {
-  if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
-    {
-      uentry_makeVarFunction (ue);
-    }
-  
+  uentry_convertVarFunction (ue);  
   llassertfatal (uentry_isFunction (ue));
   ue->info->fcn->specialCode = SPC_MESSAGELIKE;
   checkSpecialFunction (ue);
@@ -3010,39 +3072,48 @@ uentry_isSpecialFunction (uentry ue)
 /*@notnull@*/ uentry uentry_makeParam (idDecl t, int i)
 {
   ctype ct = idDecl_getCtype (t);
-  ctype base = ct;
-  sRef pref = sRef_makeParam (i, ct);
-  uentry ue = uentry_makeVariableSrefParam (idDecl_observeId (t), ct, pref);
+  fileloc loc = setLocation ();
+  sRef pref = sRef_makeParam (i, ct, stateInfo_makeLoc (loc, SA_CREATED));
+  uentry ue = uentry_makeVariableSrefParam (idDecl_observeId (t), ct, loc, pref);
 
+  DPRINTF (("Make param: %s", uentry_unparseFull (ue)));
+  DPRINTF (("Base: %s [%d]", ctype_unparse (ct), ctype_isFixedArray (ct)));
   uentry_reflectQualifiers (ue, idDecl_getQuals (t));
   uentry_implicitParamAnnots (ue);
 
-  /* Parameter type [][] or [x][] is invalid */
+  if (ctype_isArray (ct)) 
+    {
+      /* Parameter type [][] or [x][] is invalid, but [][x] is okay */
+      ctype base = ctype_baseArrayPtr (ct);
 
-  while (ctype_isFixedArray (base)) {
-    base = ctype_baseArrayPtr (base);
-  }
-  
-  if (ctype_isIncompleteArray (base)) {
-    base = ctype_baseArrayPtr (base);
-
-    if (ctype_isArray (base)) {
-      if (!uentry_hasName (ue)) {
-       (void) optgenerror (FLG_INCOMPLETETYPE, 
-                           message ("Unnamed function parameter %d is incomplete type (inner array must have bounds): %s",
-                                    i + 1,
-                                    ctype_unparse (ct)),
-                           uentry_whereLast (ue));
-      } else {
-       (void) optgenerror (FLG_INCOMPLETETYPE, 
-                           message ("Function parameter %q is incomplete type (inner array must have bounds): %s",
-                                    uentry_getName (ue),
-                                    ctype_unparse (ct)),
-                           uentry_whereLast (ue));
-      }
+      DPRINTF (("Check array: %s / Base: %s", ctype_unparse (ct),
+               ctype_unparse (base)));
+      
+      if (ctype_isIncompleteArray (base)) 
+       {
+         if (!uentry_hasName (ue)) 
+           {
+             voptgenerror 
+               (FLG_INCOMPLETETYPE, 
+                message ("Unnamed function parameter %d is incomplete type "
+                         "(inner array must have bounds): %s",
+                         i + 1,
+                         ctype_unparse (ct)),
+                uentry_whereLast (ue));
+           } 
+         else 
+           {
+             voptgenerror 
+               (FLG_INCOMPLETETYPE, 
+                message ("Function parameter %q is incomplete type "
+                         "(inner array must have bounds): %s",
+                         uentry_getName (ue),
+                         ctype_unparse (ct)),
+                uentry_whereLast (ue));
+           }
+       }
     }
-  }
-
+  
   DPRINTF (("Param: %s", uentry_unparseFull (ue)));
   return ue;
 }
@@ -3059,7 +3130,7 @@ uentry_isSpecialFunction (uentry ue)
     {
       fileloc loc = setLocation ();
       uentry ue = uentry_makeVariable (idDecl_observeId (t), ct, loc, FALSE);
-      
+
       uentry_reflectQualifiers (ue, idDecl_getQuals (t));
 
       if (!uentry_isExtern (ue))
@@ -3071,20 +3142,18 @@ uentry_isSpecialFunction (uentry ue)
     }
 }
 
-# ifndef NOLCL
-/*@notnull@*/ uentry uentry_makeVariableParam (cstring n, ctype t)
+/*@notnull@*/ uentry uentry_makeVariableParam (cstring n, ctype t, fileloc loc)
 {
-  return (uentry_makeVariableParamAux (n, t, sRef_makeType (t), SS_DEFINED));
+  return (uentry_makeVariableParamAux (n, t, sRef_makeType (t), fileloc_copy (loc), SS_DEFINED));
 }
-# endif
 
 /*
 ** constants
 */
 
-/*@only@*/ /*@notnull@*/ 
+static /*@only@*/ /*@notnull@*/ 
 uentry uentry_makeConstantAux (cstring n, ctype t, 
-                              /*@keep@*/ fileloc f, bool priv,
+                              /*@keep@*/ fileloc f, bool priv, bool macro,
                               /*@only@*/ multiVal m)
 {
   uentry e = uentry_alloc ();
@@ -3094,7 +3163,7 @@ uentry uentry_makeConstantAux (cstring n, ctype t,
   e->utype = t;
   e->storageclass = SCNONE;
 
-  e->warn = warnClause_undefined; /*@i32 warnings for constants? */
+  e->warn = warnClause_undefined; /* Don't support warnings for constants */
 
   e->sref  = sRef_makeConst (t);
 
@@ -3107,8 +3176,8 @@ uentry uentry_makeConstantAux (cstring n, ctype t,
 
   e->info = (uinfo) dmalloc (sizeof (*e->info));
   e->info->uconst = (ucinfo) dmalloc (sizeof (*e->info->uconst));
-  e->info->uconst->val = m;
   e->info->uconst->access = typeIdSet_undefined;
+  e->info->uconst->macro = macro;
 
   uentry_setSpecDef (e, f);
 
@@ -3117,12 +3186,27 @@ uentry uentry_makeConstantAux (cstring n, ctype t,
       sRef_setDefNull (e->sref, uentry_whereDeclared (e)); 
     }
 
+  uentry_setConstantValue (e, m);
+
   return (e);
 }
 
 /*@notnull@*/ uentry uentry_makeConstant (cstring n, ctype t, fileloc f)
 {
-  return (uentry_makeConstantAux (n, t, f, FALSE, multiVal_unknown ()));
+  uentry ue = uentry_makeConstantAux (n, t, f, FALSE, FALSE, multiVal_unknown ());
+  return ue;
+}
+
+/*@notnull@*/ uentry uentry_makeConstantValue (cstring n, ctype t, fileloc f, bool priv, multiVal val)
+{
+  uentry ue = uentry_makeConstantAux (n, t, f, priv, FALSE, val);
+  return ue;
+}
+
+/*@notnull@*/ uentry uentry_makeMacroConstant (cstring n, ctype t, fileloc f)
+{
+  uentry ue = uentry_makeConstantAux (n, t, f, FALSE, TRUE, multiVal_unknown ());
+  return ue;
 }
 
 /*@notnull@*/ uentry uentry_makeIdConstant (idDecl t)
@@ -3133,9 +3217,10 @@ uentry uentry_makeConstantAux (cstring n, ctype t,
 
   llassert (fileloc_isUndefined (ue->whereDeclared));
   ue->whereDeclared = setLocation ();
-
   uentry_reflectQualifiers (ue, idDecl_getQuals (t));
 
+  DPRINTF (("Constant: %s", uentry_unparseFull (ue)));
+  DPRINTF (("Value: %s", multiVal_unparse (uentry_getConstantValue (ue))));
   return ue;
 }
 
@@ -3223,14 +3308,14 @@ void uentry_setCheckedStrict (uentry ue)
 }
 
 static /*@only@*/ /*@notnull@*/ 
-  uentry uentry_makeVariableAux (cstring n, ctype t, 
-                                fileloc f,
-                                /*@exposed@*/ sRef s,
-                                bool priv, vkind kind)
+uentry uentry_makeVariableAux (cstring n, ctype t, 
+                              fileloc f,
+                              /*@exposed@*/ sRef s,
+                              bool priv, vkind kind)
 {
   uentry e = uentry_alloc ();
   ctype rt = t;
-
+  
   DPRINTF (("Make variable: %s %s %s", n, ctype_unparse (t), sRef_unparse (s)));
 
   e->ukind = KVAR;
@@ -3239,7 +3324,7 @@ static /*@only@*/ /*@notnull@*/
 
   e->storageclass = SCNONE;
 
-  e->warn = warnClause_undefined; /*@i32 warnings for variable @*/
+  e->warn = warnClause_undefined; /* Don't support warnings for variables yet @*/
 
   e->sref  = s;
 
@@ -3254,6 +3339,7 @@ static /*@only@*/ /*@notnull@*/
   e->info->var = (uvinfo) dmalloc (sizeof (*e->info->var));
   e->info->var->kind = kind;
 
+  /* removed: e->info->var->origsref = sRef_saveCopy (e->sref); */
   e->info->var->checked = CH_UNKNOWN;
 
   DPRINTF (("Here we are: %s", sRef_unparseFull (e->sref)));
@@ -3271,28 +3357,27 @@ static /*@only@*/ /*@notnull@*/
       sRef_setStateFromType (e->sref, rt);
     }
 
-  DPRINTF (("Here we are: %s", sRef_unparseFull (e->sref)));
   e->info->var->defstate = sRef_getDefState (e->sref);  
   e->info->var->nullstate = sRef_getNullState (e->sref);
 
-/* start modifications */
-/* This function sets the uentry for a pointer or array variable declaration,
-   it allocates memory and sets the fields. We check if the type of the variable
-   is a pointer or array and allocate a `bbufinfo' struct accordingly */
-
-  if( ctype_isArray (t) || ctype_isPointer(t)) {
-    /*@i222@*/e->info->var->bufinfo = dmalloc( sizeof(*e->info->var->bufinfo) );
-     e->info->var->bufinfo->bufstate = BB_NOTNULLTERMINATED;
-     /*@access sRef@*/ /*i@222*/
-     /* It probably isn't necessary to violate the abstraction here
-      I'll fix this later
-     */
-     s->bufinfo.bufstate = BB_NOTNULLTERMINATED;
-     /*@noaccess sRef@*/
-  } else {
-     e->info->var->bufinfo = NULL;
-  }/* end else */
-/* end modification */
+  /* start modifications */
+  /* This function sets the uentry for a pointer or array variable declaration,
+     it allocates memory and sets the fields. We check if the type of the variable
+     is a pointer or array and allocate a `bbufinfo' struct accordingly */
+  
+  if (ctype_isArray (t) || ctype_isPointer(t))
+    {
+      e->info->var->bufinfo = dmalloc (sizeof (*e->info->var->bufinfo));
+      e->info->var->bufinfo->bufstate = BB_NOTNULLTERMINATED;
+      sRef_setNotNullTerminatedState (s);
+    } 
+  else 
+    {
+      e->info->var->bufinfo = NULL;
+    }/* end else */
+  /* end modification */
+
+  DPRINTF (("New variable: %s", sRef_unparseFull (e->sref)));
 
   return (e);
 }
@@ -3335,15 +3420,17 @@ void uentry_makeVarFunction (uentry ue)
   ak = sRef_getOrigAliasKind (ue->sref);
   ek = sRef_getOrigExKind (ue->sref);
 
+  llassert (uentry_isVariable (ue));
   oldInfo = ue->info->var;
 
-  llassert (ctype_isUnknown (ue->utype) || ctype_isFunction (ue->utype));
+  DPRINTF (("ue: %s", uentry_unparseFull (ue)));
+  llassert (ctype_isUnknown (ue->utype) || ctype_isFunction (ctype_realType (ue->utype)));
 
   /*
-  ** expanded macro is marked used (until I write a pre-processor)
+  ** expanded macro is marked used 
   */
 
-  ue->used |= (oldInfo->kind == VKEXPMACRO);
+  ue->used = ue->used || (oldInfo->kind == VKEXPMACRO);
 
   ue->ukind = KFCN;
   ue->info->fcn = (ufinfo) dmalloc (sizeof (*ue->info->fcn));
@@ -3359,13 +3446,12 @@ void uentry_makeVarFunction (uentry ue)
   ue->info->fcn->defparams = uentryList_undefined;
 
   /*drl*/
-  ue->info->fcn->preconditions = constraintList_undefined;
+  ue->info->fcn->preconditions = functionConstraint_undefined;
   /*end */
 
   /*drl 12/28/2000*/
-  ue->info->fcn->postconditions = constraintList_undefined;
+  ue->info->fcn->postconditions = functionConstraint_undefined; 
   /*end */
-
   
   if (ctype_isFunction (ue->utype))
     {
@@ -3427,8 +3513,7 @@ void uentry_makeVarFunction (uentry ue)
 
   if (oldInfo->kind == VKEXPMACRO)
     {
-      fileloc_free (loc);
-      ue->whereDeclared = fileloc_undefined;
+      ;
     }
   else
     {
@@ -3439,39 +3524,130 @@ void uentry_makeVarFunction (uentry ue)
   uvinfo_free (oldInfo);
 }
 
-void
-uentry_setGlobals (uentry ue, /*@owned@*/ globSet globs)
+void uentry_makeConstantFunction (uentry ue)
 {
+  alkind ak;
+  exkind ek;
+  ucinfo oldInfo;
+  fileloc loc;
+
   llassert (uentry_isValid (ue));
+  llassert (!sRef_modInFunction ());
 
-  if (uentry_isIter (ue))
-    {
-      llassert (globSet_isUndefined (ue->info->iter->globs));
-      ue->info->iter->globs = globs;
-    }
-  else
-    {
-      if (uentry_isVariable (ue) && ctype_isFunction (uentry_getType (ue)))
-       {
-         uentry_makeVarFunction (ue);
-       }
-      
-      llassert (uentry_isFunction (ue));
-      llassert (!ue->info->fcn->hasGlobs 
-               && globSet_isUndefined (ue->info->fcn->globs));
-      
-      ue->info->fcn->hasGlobs = TRUE;
-      globSet_markImmutable (globs);
-      /*@-mustfree@*/ ue->info->fcn->globs = globs;
-      /*@=mustfree@*/
+  ak = sRef_getOrigAliasKind (ue->sref);
+  ek = sRef_getOrigExKind (ue->sref);
+
+  llassert (uentry_isConstant (ue));
+  oldInfo = ue->info->uconst;
+
+  llassert (ctype_isUnknown (ue->utype) || ctype_isFunction (ue->utype));
+
+  /*
+  ** expanded macro is marked used (until I write a pre-processor)
+  */
+
+  ue->ukind = KFCN;
+  ue->info->fcn = (ufinfo) dmalloc (sizeof (*ue->info->fcn));
+  ue->info->fcn->exitCode = XK_UNKNOWN;
+  ue->info->fcn->nullPred = qual_createUnknown ();
+  ue->info->fcn->specialCode = SPC_NONE;
+  ue->info->fcn->access = typeIdSet_undefined;
+  ue->info->fcn->hasGlobs = FALSE;
+  ue->info->fcn->globs = globSet_undefined;
+  ue->info->fcn->hasMods = FALSE;
+  ue->info->fcn->mods = sRefSet_undefined;
+  ue->info->fcn->specclauses = NULL;
+  ue->info->fcn->defparams = uentryList_undefined;
+
+  /*drl*/
+  ue->info->fcn->preconditions = functionConstraint_undefined;
+  /*end */
+
+  /*drl 12/28/2000*/
+  ue->info->fcn->postconditions = functionConstraint_undefined;
+  /*end */
+
+  
+  if (ctype_isFunction (ue->utype))
+    {
+      ue->sref = sRef_makeType (ctype_getReturnType (ue->utype)); 
+    }
+  else
+    {
+      ue->sref = sRef_makeType (ctype_unknown); 
     }
 
-  /*@i23 ??? 
-  if (globSet_hasStatic (globs))
+  if (sRef_isRefCounted (ue->sref))
     {
-      context_recordFileGlobals (globs);
+      ak = AK_NEWREF;
+    }
+  else
+    {
+      if (alkind_isUnknown (ak))
+       {
+         if (exkind_isKnown (ek))
+           {
+             DPRINTF (("imp dep: %s", uentry_unparseFull (ue)));
+             ak = AK_IMPDEPENDENT;
+           }
+         else 
+           {
+             if (context_getFlag (FLG_RETIMPONLY))
+               {
+                 if (ctype_isFunction (ue->utype)
+                     && ctype_isVisiblySharable 
+                     (ctype_realType (ctype_getReturnType (ue->utype))))
+                   {
+                     if (uentryList_hasReturned (uentry_getParams (ue)))
+                       {
+                         ;
+                       }
+                     else
+                       {
+                         if (ctype_isImmutableAbstract (ctype_getReturnType (ue->utype))) 
+                           {
+                             ;
+                           }
+                         else 
+                           {
+                             ak = AK_IMPONLY;
+                           }
+                       }
+                   }
+               }
+           }
+       }
+    }
+
+  loc = ue->whereDeclared;
+
+  sRef_setAliasKind (ue->sref, ak, loc);
+  sRef_setExKind (ue->sref, ek, loc);
+
+  fileloc_free (ue->whereDefined);
+  ue->whereDefined = fileloc_undefined;
+  ucinfo_free (oldInfo);
+}
+
+void
+uentry_setGlobals (uentry ue, /*@only@*/ globSet globs)
+{
+  llassert (uentry_isValid (ue));
+
+  globSet_markImmutable (globs);
+
+  if (uentry_isIter (ue))
+    {
+      ue->info->iter->globs = globSet_unionFree (ue->info->iter->globs, globs);
+    }
+  else
+    {
+      uentry_convertVarFunction (ue);
+      llassert (uentry_isFunction (ue));
+
+      ue->info->fcn->hasGlobs = TRUE;
+      ue->info->fcn->globs = globSet_unionFree (ue->info->fcn->globs, globs);
     }
-  */
 
   if (context_getFlag (FLG_GLOBALSIMPMODIFIESNOTHING))
     {
@@ -3510,7 +3686,7 @@ void uentry_addAccessType (uentry ue, typeId tid)
                       /*@only@*/ warnClause warn,
                       fileloc f)
 {
-  llassert (warnClause_isUndefined (warn)); /*@i325 remove parameter! */
+  llassert (warnClause_isUndefined (warn));
   return (uentry_makeFunctionAux (n, t, 
                                  ((typeId_isInvalid (access)) ? typeIdSet_emptySet () 
                                   : typeIdSet_single (access)),
@@ -3519,7 +3695,6 @@ void uentry_addAccessType (uentry ue, typeId tid)
                                  FALSE, FALSE));
 }
 
-# ifndef NOLCL
 /*@notnull@*/ uentry 
   uentry_makePrivFunction2 (cstring n, ctype t, 
                            typeIdSet access, 
@@ -3548,7 +3723,6 @@ void uentry_addAccessType (uentry ue, typeId tid)
   reflectImplicitFunctionQualifiers (ue, TRUE);
   return (ue);
 }
-# endif
 
 uentry uentry_makeExpandedMacro (cstring s, fileloc f)
 {
@@ -3587,7 +3761,6 @@ bool uentry_isForward (uentry e)
   return FALSE;
 }
 
-# ifndef NOLCL
 /*@notnull@*/ uentry 
 uentry_makeTypeListFunction (cstring n, typeIdSet access, fileloc f)
 {
@@ -3608,7 +3781,6 @@ uentry_makeUnspecFunction (cstring n, ctype t,
   reflectImplicitFunctionQualifiers (ue, TRUE);
   return ue;
 }
-# endif
 
 /*
 ** datatypes
@@ -3617,7 +3789,7 @@ uentry_makeUnspecFunction (cstring n, ctype t,
 /* is exported for use by usymtab_interface */
 
 /*@notnull@*/ uentry 
-  uentry_makeDatatypeAux (cstring n, ctype t, ynm mut, ynm abstract, 
+  uentry_makeDatatypeAux (cstring n, ctype t, ynm mut, qual abstract, 
                          fileloc f, bool priv)
 {
   uentry e = uentry_alloc ();
@@ -3639,7 +3811,7 @@ uentry_makeUnspecFunction (cstring n, ctype t,
 
   uentry_setSpecDef (e, f);
 
-  e->warn = warnClause_undefined; /*@i634@*/ 
+  e->warn = warnClause_undefined; 
   e->uses = filelocList_new ();
   e->isPrivate = priv;
   e->hasNameError = FALSE;
@@ -3658,7 +3830,7 @@ uentry_makeUnspecFunction (cstring n, ctype t,
       uentry_setDefined (e, f);
     }
 
-  if (ynm_isOn (abstract) && !(uentry_isCodeDefined (e)))
+  if (qual_isAbstract (abstract) && !(uentry_isCodeDefined (e)))
     {
       sRef_setNullState (e->sref, NS_ABSNULL, uentry_whereDeclared (e));
     }
@@ -3667,12 +3839,12 @@ uentry_makeUnspecFunction (cstring n, ctype t,
 }
 
 /*@notnull@*/ uentry
-  uentry_makeDatatype (cstring n, ctype t, ynm mut, ynm abstract, fileloc f)
+  uentry_makeDatatype (cstring n, ctype t, ynm mut, qual abstract, fileloc f)
 {
   return (uentry_makeDatatypeAux (n, t, mut, abstract, f, FALSE));
 }
 
-/*@notnull@*/ uentry uentry_makeBoolDatatype (ynm abstract)
+/*@notnull@*/ uentry uentry_makeBoolDatatype (qual abstract)
 {
   uentry ret = uentry_makeDatatypeAux (context_getBoolName (),
                                       ctype_bool, NO, abstract, 
@@ -3703,7 +3875,7 @@ static /*@only@*/ /*@notnull@*/ uentry
 
   uentry_setSpecDef (e, f);
 
-  e->warn = warnClause_undefined; /*@i452@*/
+  e->warn = warnClause_undefined; 
   e->uses = filelocList_new ();
   e->isPrivate = FALSE;
   e->hasNameError = FALSE;
@@ -3748,8 +3920,8 @@ uentry_makeEndIterAux (cstring n, typeIdSet access, /*@only@*/ fileloc f)
   e->info->enditer = (ueinfo) dmalloc (sizeof (*e->info->enditer));
 
   e->info->enditer->access = access;
+  e->warn = warnClause_undefined; 
 
-  e->warn = warnClause_undefined; /*@i452@*/
   return (e);
 }
 
@@ -3793,10 +3965,10 @@ static /*@only@*/ /*@notnull@*/ uentry
 
   e->info = (uinfo) dmalloc (sizeof (*e->info));
   e->info->datatype = (udinfo) dmalloc (sizeof (*e->info->datatype));
-  e->info->datatype->abs = NO;
+  e->info->datatype->abs = qual_createUnknown ();
   e->info->datatype->mut = (kind == KENUMTAG) ? NO : MAYBE;
   e->info->datatype->type = t;
-  e->warn = warnClause_undefined; /*@i452@*/
+  e->warn = warnClause_undefined;
 
   if (uentry_isDeclared (e))
     {
@@ -3835,7 +4007,6 @@ uentry_makeUnionTag (cstring n, ctype t, fileloc loc)
   return (ret);
 }
 
-# ifndef NOLCL
 uentry
 uentry_makeEnumTag (cstring n, ctype t, fileloc loc)
 {
@@ -3845,7 +4016,6 @@ uentry_makeEnumTag (cstring n, ctype t, fileloc loc)
   cstring_free (ename);
   return ret;
 }
-# endif
 
 uentry
 uentry_makeUnionTagLoc (cstring n, ctype t)
@@ -4030,14 +4200,14 @@ uentry_compare (uentry u1, uentry u2)
     {
     case KINVALID:
     case KELIPSMARKER:
-      /* bug detected by lclint:  
+      /* bug detected by splint:  
       ** uentry.c:753,14: Return value type bool does not match declared type int: TRUE 
       */
       return 0;
     case KENUMCONST:
     case KCONST:
-      return (multiVal_compare (u1->info->uconst->val,
-                               u2->info->uconst->val));
+      return (multiVal_compare (uentry_getConstantValue (u1),
+                               uentry_getConstantValue (u2)));
     case KSTRUCTTAG: 
     case KUNIONTAG: 
     case KENUMTAG: 
@@ -4055,7 +4225,7 @@ uentry_compare (uentry u1, uentry u2)
       ** Functions are never equivalent
       */
       
-      if ((int) u1 < (int) u2)
+      if (u1 - u2 < 0) /* evans 2001-08-21: was: ((int) u1 < (int) u2), changed to remove gcc warning */
        {
          return -1;
        }
@@ -4081,7 +4251,7 @@ uentry_compare (uentry u1, uentry u2)
                                    u2->info->datatype->type));
       COMPARERETURN (ynm_compare (u1->info->datatype->mut,
                                  u2->info->datatype->mut));
-      return (ynm_compare (u1->info->datatype->abs, u2->info->datatype->abs));
+      return (generic_compare (u1->info->datatype->abs, u2->info->datatype->abs));
     }
   
   BADEXIT;
@@ -4152,13 +4322,13 @@ static uentry
   e->used = FALSE;
   e->lset = FALSE;
 
-  e->warn = warnClause_undefined; /*@i452@*/
+  e->warn = warnClause_undefined; 
 
   e->info = (uinfo) dmalloc (sizeof (*e->info));
   e->info->uconst = (ucinfo) dmalloc (sizeof (*e->info->uconst));
-  e->info->uconst->val = m;
   e->info->uconst->access = access;
-
+  e->info->uconst->macro = FALSE; /* fix this when macro info added to library */
+  uentry_setConstantValue (e, m);
   sRef_storeState (e->sref);
 
   return (e);
@@ -4200,7 +4370,7 @@ static /*@only@*/ uentry
   e->lset = FALSE;
 
   e->uses = filelocList_new ();
-  e->warn = warnClause_undefined; /*@i452@*/
+  e->warn = warnClause_undefined; 
 
   e->info = (uinfo) dmalloc (sizeof (*e->info));
   e->info->var = (uvinfo) dmalloc (sizeof (*e->info->var));
@@ -4224,7 +4394,7 @@ static /*@only@*/ uentry
 }
 
 static /*@only@*/ uentry  
-uentry_makeDatatypeBase (/*@only@*/ cstring name, ctype ct, ynm abstract, 
+uentry_makeDatatypeBase (/*@only@*/ cstring name, ctype ct, qual abstract, 
                         ynm mut, ctype rtype, alkind ak, exkind exp, 
                         sstate defstate, nstate isnull,
                         /*@only@*/ fileloc loc)
@@ -4262,7 +4432,7 @@ uentry_makeDatatypeBase (/*@only@*/ cstring name, ctype ct, ynm abstract,
 
   sRef_setDefState (e->sref, defstate, loc);
 
-  if (ynm_isOn (abstract) && ctype_isUnknown (ct) && isnull == NS_UNKNOWN)
+  if (qual_isEitherAbstract (abstract) && ctype_isUnknown (ct) && isnull == NS_UNKNOWN)
     {
       isnull = NS_ABSNULL;
     }
@@ -4285,9 +4455,7 @@ uentry_makeDatatypeBase (/*@only@*/ cstring name, ctype ct, ynm abstract,
   
   e->isPrivate = FALSE;
   e->hasNameError = FALSE;
-
-  e->warn = warnClause_undefined; /*@i452@*/
-
+  e->warn = warnClause_undefined; 
   e->used = FALSE;
   e->lset = FALSE;
   e->uses = filelocList_new ();
@@ -4305,7 +4473,6 @@ uentry_makeDatatypeBase (/*@only@*/ cstring name, ctype ct, ynm abstract,
   return (e);
 }
 
-# ifndef NOLCL
 static void uentry_setHasGlobs (uentry ue)
 {
   llassert (uentry_isFunction (ue));
@@ -4319,7 +4486,6 @@ static void uentry_setHasMods (uentry ue)
 
   ue->info->fcn->hasMods = TRUE;
 }
-# endif
 
 bool uentry_hasGlobs (uentry ue)
 {
@@ -4336,6 +4502,13 @@ bool uentry_hasStateClauseList (uentry ue)
   return (uentry_isFunction (ue) && stateClauseList_isDefined (ue->info->fcn->specclauses));
 }
 
+bool uentry_hasConditions (uentry ue)
+{
+  return (uentry_isFunction (ue) 
+         && (functionConstraint_isDefined (ue->info->fcn->preconditions)
+             || functionConstraint_isDefined (ue->info->fcn->postconditions)));
+}
+
 stateClauseList uentry_getStateClauseList (uentry ue)
 {
   if (!uentry_isFunction (ue))
@@ -4488,11 +4661,11 @@ static /*@only@*/ uentry
   e->used = FALSE;
   e->lset = FALSE;
   e->uses = filelocList_new ();
-  e->warn = warnClause_undefined; /*@i452@*/
+  e->warn = warnClause_undefined; 
 
   e->info = (uinfo) dmalloc (sizeof (*e->info));
   e->info->datatype = (udinfo) dmalloc (sizeof (*e->info->datatype));
-  e->info->datatype->abs  = NO;
+  e->info->datatype->abs  = qual_createUnknown ();
   e->info->datatype->mut  = MAYBE;
   e->info->datatype->type = rtype;
 
@@ -4533,7 +4706,7 @@ static uentry
   e->used = FALSE;
   e->lset = FALSE;
   e->uses = filelocList_new ();
-  e->warn = warnClause_undefined; /*@i452@*/
+  e->warn = warnClause_undefined; 
 
   e->info = (uinfo) dmalloc (sizeof (*e->info));
   e->info->iter = (uiinfo) dmalloc (sizeof (*e->info->iter));
@@ -4577,7 +4750,7 @@ static uentry
   e->used = FALSE;
   e->lset = FALSE;
   e->uses = filelocList_new ();
-  e->warn = warnClause_undefined; /*@i452@*/
+  e->warn = warnClause_undefined; 
 
   e->info = (uinfo) dmalloc (sizeof (*e->info));
   e->info->enditer = (ueinfo) dmalloc (sizeof (*e->info->enditer));
@@ -4689,7 +4862,7 @@ uentry_undump (ekind kind, fileloc loc, char **s)
          break;
        case KDATATYPE: 
          {
-           ynm abstract;
+           qual abstract;
            ynm mut;
            ctype rtype;
            sstate defstate;
@@ -4697,7 +4870,7 @@ uentry_undump (ekind kind, fileloc loc, char **s)
            alkind aliased;
            exkind exp;
 
-           advanceField (s); abstract = ynm_fromCodeChar (reader_loadChar (s));
+           advanceField (s); abstract = qual_abstractFromCodeChar (reader_loadChar (s));
            advanceField (s); mut = ynm_fromCodeChar (reader_loadChar (s));
            advanceField (s); defstate = sstate_fromInt (reader_getInt (s));      
            advanceField (s); isnull = nstate_fromInt (reader_getInt (s));      
@@ -4966,7 +5139,7 @@ uentry_dumpAux (uentry v, bool isParam)
        else
          {
            sdump = message ("%d@%d@%d@%d@%d",  
-                    (int) dss,
+                            (int) dss,
                             (int) nst,
                             (int) alk,
                             (int) exk,
@@ -4999,9 +5172,9 @@ uentry_dumpAux (uentry v, bool isParam)
                ctype_unparse (v->utype), (int) v->utype));
       */
 
-      return (message ("%q@%s@%s@%d@%d@%d@%d@%q#%s", 
+      return (message ("%q@%c@%s@%d@%d@%d@%d@%q#%s", 
                       ctype_dump (v->utype),
-                      ynm_unparseCode (v->info->datatype->abs),
+                      qual_abstractCode (v->info->datatype->abs),
                       ynm_unparseCode (v->info->datatype->mut),
                       (int) sRef_getDefState (v->sref),
                       (int) sRef_getNullState (v->sref),
@@ -5096,7 +5269,7 @@ uentry_dumpAux (uentry v, bool isParam)
       {
        cstring sdump;
 
-       if (multiVal_isUnknown (v->info->uconst->val)
+       if (multiVal_isUnknown (uentry_getConstantValue (v))
            && typeIdSet_isEmpty (uentry_accessType (v))
            && (sRef_getNullState (v->sref) == NS_UNKNOWN))
          {
@@ -5105,7 +5278,7 @@ uentry_dumpAux (uentry v, bool isParam)
        else
          {
            sdump = message ("@%q@%q@%d",
-                            multiVal_dump (v->info->uconst->val),
+                            multiVal_dump (uentry_getConstantValue (v)),
                             typeIdSet_dump (uentry_accessType (v)),
                             (int) sRef_getNullState (v->sref));
          }
@@ -5170,8 +5343,8 @@ uentry_unparseFull (uentry v)
     {
       cstring res;
 
-      res = message ("[%w] %s %s: %s [spec: %q; decl: %q; def: %q]",
-                    (unsigned long) v, ekind_unparse (v->ukind), v->uname,
+      res = message ("[%p] %s %s: %s [spec: %q; decl: %q; def: %q]",
+                    v, ekind_unparse (v->ukind), v->uname,
                     ctype_unparse (v->utype),
                     fileloc_unparse (uentry_whereSpecified (v)),
                     fileloc_unparse (uentry_whereDeclared (v)),
@@ -5187,18 +5360,20 @@ uentry_unparseFull (uentry v)
                         (ctype_isDefined (v->info->datatype->type) 
                          ? v->info->datatype->type : ctype_unknown),
                         ynm_unparse (v->info->datatype->mut),
-                        ynm_unparse (v->info->datatype->abs),
+                        qual_unparse (v->info->datatype->abs),
                         sRef_unparseState (v->sref));
        }
       else if (uentry_isFunction (v))
        {
          res = message ("%q / sref: %q / mods: %q / "
-                        "globs: %q / clauses: %q",
+                        "globs: %q / clauses: %q / pre: %q / post: %q",
                         res,
                         sRef_unparseFull (v->sref),
                         sRefSet_unparse (v->info->fcn->mods),
                         globSet_unparse  (v->info->fcn->globs),
-                        stateClauseList_unparse (v->info->fcn->specclauses));
+                        stateClauseList_unparse (v->info->fcn->specclauses),
+                        functionConstraint_unparse (v->info->fcn->preconditions),
+                        functionConstraint_unparse (v->info->fcn->postconditions));
        }
       else if (uentry_isIter (v))
        {
@@ -5219,6 +5394,12 @@ uentry_unparseFull (uentry v)
          DPRINTF (("sref: %s", sRef_unparseDebug (v->sref)));
          /* DPRINTF (("sref: %s", sRef_unparseDeep (v->sref)));           */
        }
+      else if (uentry_isConstant (v))
+       {
+         res = message ("%q = %q / %q",
+                        res, multiVal_unparse (uentry_getConstantValue (v)),
+                        sRef_unparseFull (v->sref));
+       }
       else
        {
          res = message ("%q :: %q", res, uentry_unparse (v));
@@ -5319,10 +5500,10 @@ uentry_setAbstract (uentry e)
   typeId oldid;
 
   llassert (uentry_isDatatype (e) 
-           && (ynm_isMaybe (e->info->datatype->abs)));
+           && (qual_isUnknown (e->info->datatype->abs)));
 
   oldid = ctype_typeId (e->info->datatype->type);
-  e->info->datatype->abs = YES;
+  e->info->datatype->abs = qual_createAbstract ();
   e->info->datatype->type = ctype_createAbstract (oldid);
 }
 
@@ -5330,32 +5511,42 @@ void
 uentry_setConcrete (uentry e)
 {
   llassert (uentry_isDatatype (e) 
-           && (ynm_isMaybe (e->info->datatype->abs)));
+           && (qual_isUnknown (e->info->datatype->abs)
+               || qual_isConcrete (e->info->datatype->abs)));
 
-  e->info->datatype->abs = NO;
+  e->info->datatype->abs = qual_createConcrete ();
 }
 
 bool
 uentry_isAbstractDatatype (uentry e)
 {
   return (uentry_isDatatype (e) 
-         && (ynm_isOn (e->info->datatype->abs)));
+         && (qual_isEitherAbstract (e->info->datatype->abs)));
 }
 
 bool
 uentry_isMaybeAbstract (uentry e)
 {
   return (uentry_isDatatype (e) 
-         && (ynm_isMaybe (e->info->datatype->abs)));
+         && (!qual_isConcrete (e->info->datatype->abs)));
 }
 
 bool
 uentry_isMutableDatatype (uentry e)
 {
-  bool res = uentry_isDatatype (e) 
-    && (ynm_toBoolRelaxed (e->info->datatype->mut));
-  
-  return res;
+  if (uentry_isDatatype (e))
+    {
+      if (ctype_isNumAbstract (e->info->datatype->type)) 
+       {
+         return FALSE;
+       }
+      else
+       {
+         return ynm_toBoolRelaxed (e->info->datatype->mut);
+       }
+    }
+
+  return FALSE;
 }
 
 bool
@@ -5562,29 +5753,42 @@ uentry_getGlobs (uentry l)
       return globSet_undefined;
     }
 
-  if (l->ukind != KFCN)
+  if (uentry_isFunction (l))
+    {
+      return l->info->fcn->globs;
+    }
+  else if (uentry_isIter (l))
+    {
+      return l->info->iter->globs;
+    }
+  else if (uentry_isEndIter (l))
+    {
+      return globSet_undefined;
+    }
+  else
     {
-      if (l->ukind != KITER && l->ukind != KENDITER)
+      if (l->ukind == KVAR)
        {
-         if (l->ukind == KVAR)
-           {
-             llbug (message ("Bad call to uentry_getGlobs (var): %q (%s)", 
+         llcontbug (message ("Bad call to uentry_getGlobs (var): %q (%s)", 
                              uentry_unparse (l), 
                              ekind_unparse (l->ukind)));
-           }
-         else
-           {
-             llbug (message ("Bad call to uentry_getGlobs: %q (%s)", 
+       }
+      else
+       {
+         llcontbug (message ("Bad call to uentry_getGlobs: %q (%s)", 
                              uentry_unparse (l), 
                              ekind_unparse (l->ukind)));
-           }
        }
+
       return globSet_undefined;
     }
-
-  return l->info->fcn->globs;
 }
 
+# ifdef WIN32
+/* Make Microsoft VC++ happy */
+# pragma warning (disable : 4715) 
+# endif
+
 /*@observer@*/ sRefSet
 uentry_getMods (uentry l)
 {
@@ -5596,22 +5800,35 @@ uentry_getMods (uentry l)
       return sRefSet_undefined; 
     }
 
-  return l->info->fcn->mods;
+  if (uentry_isFunction (l))
+    {
+      return l->info->fcn->mods;
+    }
+  else if (uentry_isIter (l))
+    {
+      return l->info->iter->mods;
+    }
+  else if (uentry_isEndIter (l))
+    {
+      return sRefSet_undefined;
+    }
+  else
+    {
+      BADBRANCH;
+    }
 }
 
 ekind
 uentry_getKind (uentry e)
 {
   llassert (uentry_isValid (e));
-
   return (e->ukind);
 }
 
 /*@observer@*/ multiVal uentry_getConstantValue (uentry e)
 {
-  llassert (uentry_isEitherConstant (e));
-
-  return (e->info->uconst->val);
+  llassert (uentry_isEitherConstant (e)); 
+  return (sRef_getValue (e->sref));
 }
 
 /*@observer@*/ uentryList
@@ -5639,7 +5856,13 @@ uentry_getParams (uentry l)
       {
        ctype ct = l->utype;
 
-       llassert (ctype_isFunction (ct));
+       /*drl 12/10/2002 changed to fix bug involving multiple redefines of library functions in macros.  Bug was reported by  Malcolm Parsons
+
+       Old code was  simplly llassert (ctype_isFunction (ct) );
+       */
+       
+       llassert (ctype_isFunction (ct) || context_inMacro() );
+       
        return (ctype_argsFunction (ct));
       }
     BADDEFAULT;
@@ -5995,7 +6218,9 @@ uentry_setDefined (uentry e, fileloc f)
 bool
 uentry_isCodeDefined (uentry e)
 {
-  return (uentry_isValid (e) && fileloc_isDefined (e->whereDefined));
+  llassert (uentry_isValid (e));
+
+  return (fileloc_isDefined (e->whereDefined));
 }
 
 bool
@@ -6021,6 +6246,29 @@ sRef uentry_getSref (uentry e)
 
 sRef uentry_getOrigSref (uentry e)
 {
+  /* evans 2003-04-12 - removed for now */
+  /* evans 2001-09-09 - need to fix this 
+  if (uentry_isValid (e))
+    {
+      if (uentry_isVariable (e))
+       {
+         return e->info->var->origsref;
+       }
+      else
+       {
+         sRef sr = sRef_copy (uentry_getSref (e));
+         
+         sRef_resetState (sr);
+         sRef_clearDerived (sr);
+         return (sr);
+       }
+    }
+  else
+    {
+      return sRef_undefined;
+    }
+  */
+
   if (uentry_isValid (e))
     {
       sRef sr = sRef_copy (uentry_getSref (e));
@@ -6073,15 +6321,11 @@ uentry_resetParams (uentry ue, /*@only@*/ uentryList pn)
   
   llassert (uentry_isValid (ue));
 
-  rct = ctype_realType (ue->utype);
-
-  if (uentry_isVariable (ue) && (ctype_isFunction (rct) || ctype_isUnknown (rct)))
-    {
-      uentry_makeVarFunction (ue);
-    }
-
+  uentry_convertVarFunction (ue);
   llassert (uentry_isFunction (ue));
 
+  rct = ctype_realType (ue->utype);
+
   if (ctype_isFunction (rct))
     {
       rettype = ctype_getReturnType (rct);
@@ -6093,7 +6337,6 @@ uentry_resetParams (uentry ue, /*@only@*/ uentryList pn)
 void
 uentry_setRefParam (uentry e)
 {
-  
   if (!uentry_isVar (e))
     {
       llbug (message ("uentry_setParam: not variable: %q", uentry_unparse (e)));
@@ -6204,14 +6447,18 @@ uentry_getAbstractType (uentry e)
 ctype uentry_getRealType (uentry e)
 {
   ctype ct;
-  typeId uid = USYMIDINVALID;
+  typeId uid = typeId_invalid;
 
   if (uentry_isInvalid (e))
     {
       return ctype_unknown;
     }
-
-  llassertprint (uentry_isDatatype (e), ("not datatype: %s", uentry_unparse (e)));
+  
+  if (!uentry_isDatatype (e))
+    {
+      /* This shouldn't happen, except when types are redeclared in strange ways */
+      return ctype_unknown;
+    }
 
   if (uentry_isAnyTag (e))
     {
@@ -6246,9 +6493,9 @@ ctype uentry_getRealType (uentry e)
   
   if (ctype_isUA (ct))
     {
-      usymId iid = ctype_typeId (ct);
+      typeId iid = ctype_typeId (ct);
       
-      if (usymId_equal (iid, uid))
+      if (typeId_equal (iid, uid))
        {         
          llcontbug (message ("uentry_getRealType: recursive type! %s",
                              ctype_unparse (ct)));
@@ -6277,7 +6524,7 @@ ctype uentry_getRealType (uentry e)
 ctype uentry_getForceRealType (uentry e)
 {
   ctype   ct;
-  typeId uid = USYMIDINVALID;
+  typeId uid = typeId_invalid;
 
   if (uentry_isInvalid (e))
     {
@@ -6311,9 +6558,9 @@ ctype uentry_getForceRealType (uentry e)
   
   if (ctype_isUA (ct))
     {
-      usymId iid = ctype_typeId (ct);
+      typeId iid = ctype_typeId (ct);
       
-      if (usymId_equal (iid, uid))
+      if (typeId_equal (iid, uid))
        {         
          llcontbug (message ("uentry_getRealType: recursive type! %s",
                              ctype_unparse (ct)));
@@ -6359,13 +6606,21 @@ uentry uentry_nameCopy (cstring name, uentry e)
 }
 
 void
-uentry_setDatatype (uentry e, usymId uid)
+uentry_setDatatype (uentry e, typeId uid)
 {
   llassert (uentry_isDatatype (e));
 
   if (uentry_isAbstractType (e))
     {
-      e->info->datatype->type = ctype_createAbstract (uid);
+      if (qual_isNumAbstract (e->info->datatype->abs)) 
+       {
+         e->info->datatype->type = ctype_createNumAbstract (uid);
+       }
+      else
+       {
+         llassert (qual_isAbstract (e->info->datatype->abs));
+         e->info->datatype->type = ctype_createAbstract (uid);
+       }
     }
   else
     {
@@ -6392,12 +6647,13 @@ uentry_setSpecDef (/*@special@*/ uentry e, /*@keep@*/ fileloc f)
       e->whereDeclared  = f;
       e->whereDefined  = fileloc_undefined;
     }
+
+  llassert (fileloc_storable (f));
 }
 
 static void
 ucinfo_free (/*@only@*/ ucinfo u)
 {
-  multiVal_free (u->val);
   sfree (u);
 }
 
@@ -6405,9 +6661,7 @@ static void
 uvinfo_free (/*@only@*/ uvinfo u)
 {
   /*drl7x added 6/29/01 */
-  /*free null terminated stuff */
-  /*@i22*/
-  //  free(u->bufinfo);
+  free (u->bufinfo); /* evans - 2001-07-19 fixed this bug */
   sfree (u);
 }
 
@@ -6442,10 +6696,8 @@ static /*@only@*/ ucinfo
 ucinfo_copy (ucinfo u)
 {
   ucinfo ret = (ucinfo) dmalloc (sizeof (*ret));
-  
-  ret->val = multiVal_copy (u->val);
   ret->access = u->access;
-
+  ret->macro = u->macro;
   return ret;
 }
 
@@ -6459,6 +6711,7 @@ uvinfo_copy (uvinfo u)
   ret->defstate = u->defstate;
   ret->checked = u->checked;
 
+
   /* drl added 07-02-001 */
   /* copy null terminated information */
 
@@ -6506,20 +6759,8 @@ ufinfo_copy (ufinfo u)
   ret->defparams = u->defparams;
   ret->specclauses = stateClauseList_copy (u->specclauses);
 
-  /*drl 11 30 2000 */
-  /* change 6/8/01 */
-
-  if (constraintList_isDefined(u->preconditions))
-    ret->preconditions = constraintList_copy(u->preconditions);
-  else
-    ret->preconditions = NULL;
-  /* end drl */
-
-    if (constraintList_isDefined(u->postconditions))
-    ret->postconditions = constraintList_copy(u->postconditions);
-  else
-    ret->postconditions = NULL;
-  /* end drl */
+  ret->preconditions = functionConstraint_copy (u->preconditions);
+  ret->postconditions = functionConstraint_copy (u->postconditions);
   
   return ret;
 }
@@ -6612,7 +6853,7 @@ uentry_reallyFree (/*@notnull@*/ /*@only@*/ uentry e)
 
   nuentries--;
   sfree (e);
-  }
+}
 
 extern void uentry_markOwned (/*@owned@*/ uentry u)
 {
@@ -6654,7 +6895,7 @@ KindConformanceError (/*@unique@*/ uentry old, uentry unew, bool mustConform)
   llassert (uentry_isValid (old));
   llassert (uentry_isValid (unew));
 
-  if (uentry_isEitherConstant (unew)
+  if ((uentry_isEitherConstant (unew) || uentry_isDatatype (unew))
       && (fileloc_isPreproc (uentry_whereDeclared (old))
          || ctype_isUnknown (old->utype))
       && !uentry_isSpecified (old))
@@ -6682,9 +6923,9 @@ KindConformanceError (/*@unique@*/ uentry old, uentry unew, bool mustConform)
                                    uentry_getName (unew),
                                    ekind_unparseLong (unew->ukind),
                                    unew->utype),
-                          uentry_whereDeclared (unew)))
+                          uentry_whereLast (unew)))  /* evans 2001-12-30: was uentry_whereDeclared */
                        {
-                         uentry_showWhereLast (old);
+                         uentry_showWhereLastKind (old);
                        }
                    }
                  else
@@ -6701,9 +6942,9 @@ KindConformanceError (/*@unique@*/ uentry old, uentry unew, bool mustConform)
                                uentry_getName (unew),
                                ekind_unparseLong (unew->ukind),
                                unew->utype),
-                      uentry_whereDeclared (unew)))
+                      uentry_whereLast (unew))) /* evans 2001-12-30: was uentry_whereDeclared */
                    {
-                     uentry_showWhereLast (old);
+                     uentry_showWhereLastKind (old);
                    }
                }
            }
@@ -6711,21 +6952,24 @@ KindConformanceError (/*@unique@*/ uentry old, uentry unew, bool mustConform)
            {
              llassert (uentry_isDeclared (unew));
 
+             DPRINTF (("Old: \n\t%s", uentry_unparseFull (old)));
+             DPRINTF (("New: \n\t%s", uentry_unparseFull (unew)));
+
              if (optgenerror
                  (FLG_INCONDEFS,
                   message ("%s %q inconsistently redeclared as %s",
                            ekind_capName (old->ukind),
                            uentry_getName (unew),
                            ekind_unparseLong (unew->ukind)),
-                  uentry_whereDeclared (unew)))
+                  uentry_whereLast (unew))) /* evans 2001-12-30: was uentry_whereDeclared */
                {
-                 uentry_showWhereLast (old);
+                 uentry_showWhereLastKind (old);
                }
            }
        }
     }
 
-  uentry_copyInto (old, unew);
+  uentry_updateInto (old, unew);
 }
 
 /*
@@ -6743,7 +6987,7 @@ uentry_showWhereLast (uentry spec)
     {
       if (fileloc_isDefined (spec->whereDefined)
          && !fileloc_isLib (spec->whereDefined)
-         && !fileloc_isPreproc (spec->whereDefined))
+         /*!! && !fileloc_isPreproc (spec->whereDefined) */ )
        {
          llgenindentmsg (message ("Previous definition of %q: %t", 
                                   uentry_getName (spec),
@@ -6779,6 +7023,54 @@ uentry_showWhereLast (uentry spec)
     }
 }
 
+static void
+uentry_showWhereLastKind (uentry spec)
+{
+  if (uentry_isValid (spec))
+    {
+      if (fileloc_isDefined (spec->whereDefined)
+         && !fileloc_isLib (spec->whereDefined)
+         /*!! && !fileloc_isPreproc (spec->whereDefined) */ )
+       {
+         llgenindentmsg (message ("Previous definition of %q as %s: %t", 
+                                  uentry_getName (spec),
+                                  ekind_unparseLong (spec->ukind),
+                                  uentry_getType (spec)),
+                         uentry_whereDefined (spec));
+       }
+      else if (uentry_isDeclared (spec))
+       {
+         llgenindentmsg (message ("Previous declaration of %q as %s: %t", 
+                                  uentry_getName (spec),
+                                  ekind_unparseLong (spec->ukind),
+                                  uentry_getType (spec)),
+                         uentry_whereDeclared (spec));
+       }
+      else if (uentry_isSpecified (spec))
+       {
+         if (uentry_hasName (spec))
+           {
+             llgenindentmsg (message ("Specification of %q as %s: %t", 
+                                      uentry_getName (spec),
+                                      ekind_unparseLong (spec->ukind),
+                                      uentry_getType (spec)),
+                             uentry_whereSpecified (spec));
+           }
+         else
+           {
+             llgenindentmsg (message ("Specification as %s: %t",
+                                      ekind_unparseLong (spec->ukind),
+                                      uentry_getType (spec)),
+                             uentry_whereSpecified (spec));
+           }
+       }
+      else
+       {
+         /* nothing to show */
+       }
+    }
+}
+
 void
 uentry_showDefSpecInfo (uentry ce, fileloc fwhere)
 {
@@ -7075,9 +7367,10 @@ checkEnumConformance (/*@notnull@*/ uentry old, /*@notnull@*/ uentry unew)
       if (optgenerror 
          (FLG_MATCHFIELDS,
           message ("Enum %q declared with members { %q } but "
-                   "specified with members { %q }",
+                   "%s with members { %q }",
                    uentry_getName (old), 
                    enumNameList_unparse (enew),
+                   uentry_specOrDefName (old),
                    enumNameList_unparse (eold)),
           uentry_whereDeclared (unew)))
        {
@@ -7152,6 +7445,10 @@ paramTypeError (uentry old, uentry oldCurrent, ctype oldType,
   
   if (hasError)
     {
+      DPRINTF (("Here: %s / %s",
+               uentry_unparseFull (oldCurrent),
+               uentry_unparseFull (newCurrent)));
+
       if (!uentry_isUndefined (oldCurrent))
        {
          if (!uentry_isUndefined (newCurrent) 
@@ -7404,10 +7701,6 @@ void checkDefState (/*@notnull@*/ uentry old, /*@notnull@*/ uentry unew,
       && newState != SS_UNKNOWN 
       && newState != SS_DEFINED)
     {
-      DPRINTF (("Where declared: %s / %s",
-               fileloc_unparse (uentry_whereDeclared (unew)),
-               bool_unparse (fileloc_isXHFile (uentry_whereDeclared (unew)))));
-
       if (mustConform)
        {
          if (optgenerror 
@@ -7701,22 +7994,46 @@ checkMetaState (/*@notnull@*/ uentry old, /*@notnull@*/ uentry unew,
                        }
                      else
                        {
-                         if (mustConform 
-                             && optgenerror 
-                             (FLG_INCONDEFS,
-                              message ("%s %q inconsistently %rdeclared %s %s, %s as %s",
-                                       uentry_ekindName (unew),
-                                       uentry_getName (unew),
-                                       uentry_isDeclared (old),
-                                       fcnErrName (unew),
-                                       metaStateInfo_unparseValue (msinfo, 
-                                                                   stateValue_getValue (newval)),
-                                       uentry_specOrDefName (old),
-                                       metaStateInfo_unparseValue (msinfo,
-                                                                   stateValue_getValue (oldval))),
-                              uentry_whereDeclared (unew)))
+                         if (!stateValue_isError (newval) 
+                             && !stateValue_isImplicit (newval))
                            {
-                             uentry_showWhereSpecified (old);
+                             if (uentry_hasName (unew)
+                                 || !sRef_isParam (uentry_getSref (unew)))
+                               {
+                                 if (mustConform 
+                                     && optgenerror 
+                                     (FLG_INCONDEFS,
+                                      message ("%s %q inconsistently %rdeclared %s %q, %s as %q",
+                                               uentry_ekindName (unew),
+                                               uentry_getName (unew),
+                                               uentry_isDeclared (old),
+                                               fcnErrName (unew),
+                                               stateValue_unparseValue (newval, msinfo),
+                                               uentry_specOrDefName (old),
+                                               stateValue_unparseValue (oldval, msinfo)),
+                                      uentry_whereDeclared (unew)))
+                                   {
+                                     uentry_showWhereSpecified (old);
+                                   }
+                               }
+                             else
+                               {
+                                 if (mustConform 
+                                     && optgenerror 
+                                     (FLG_INCONDEFS,
+                                      message ("%s %d inconsistently %rdeclared %s %q, %s as %q",
+                                               uentry_ekindName (unew),
+                                               sRef_getParam (uentry_getSref (unew)),
+                                               uentry_isDeclared (old),
+                                               fcnErrName (unew),
+                                               stateValue_unparseValue (newval, msinfo),
+                                               uentry_specOrDefName (old),
+                                               stateValue_unparseValue (oldval, msinfo)),
+                                      uentry_whereDeclared (unew)))
+                                   {
+                                     uentry_showWhereSpecified (old);
+                                   }
+                               }
                            }
                        }
                      
@@ -8002,6 +8319,29 @@ void uentry_checkMatchParam (uentry u1, uentry u2, int paramno, exprNode e)
     }
 }
 
+static void uentry_convertIntoFunction (/*@notnull@*/ uentry old)
+{
+  /*
+  ** Convert old into a function
+  */
+  
+  old->ukind = KFCN;
+  old->utype = ctype_unknown;
+  old->info->fcn = (ufinfo) dmalloc (sizeof (*old->info->fcn));
+  old->info->fcn->hasMods = FALSE;
+  old->info->fcn->hasGlobs = FALSE;
+  old->info->fcn->exitCode = XK_UNKNOWN;
+  old->info->fcn->nullPred = qual_createUnknown ();
+  old->info->fcn->specialCode = SPC_NONE;
+  old->info->fcn->access = typeIdSet_undefined;
+  old->info->fcn->globs = globSet_undefined;
+  old->info->fcn->defparams = uentryList_undefined;
+  old->info->fcn->mods = sRefSet_undefined;
+  old->info->fcn->specclauses = NULL;
+  old->info->fcn->preconditions = NULL;
+  old->info->fcn->postconditions = NULL;
+}
+
 static void
 checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old,
                          /*@notnull@*/ uentry unew, 
@@ -8010,7 +8350,7 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old,
   uentryList oldParams  = uentry_getParams (old);
   uentryList newParams  = uentry_getParams (unew);
   ctype      newType    = unew->utype;
-  ctype      oldType    = old->utype;
+  ctype      oldType    = ctype_realType (old->utype);
   ctype      oldRetType = ctype_unknown;
   ctype      newRetType = ctype_unknown;
 
@@ -8021,7 +8361,7 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old,
   if (uentry_isForward (old))
     {
       mustConform = FALSE;
-      uentry_copyInto (old, unew);
+      uentry_updateInto (old, unew);
       return;
     }
 
@@ -8031,15 +8371,31 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old,
   
   if (ctype_isKnown (oldType))
     {
-      llassert (ctype_isFunction (oldType));
+      if (ctype_isFunction (oldType))
+       {
+         oldRetType = ctype_getReturnType (oldType);
+       }
+      else
+       {
+         if (optgenerror 
+             (FLG_INCONDEFS,
+              message ("%s %q declared as function, but previously declared as %s",
+                       ekind_capName (unew->ukind),
+                       uentry_getName (unew),
+                       ekind_unparseLong (old->ukind)),
+              uentry_whereDeclared (unew)))
+           {
+             uentry_showWhereLast (old);
+           }
 
-      oldRetType = ctype_getReturnType (oldType);
+         uentry_convertIntoFunction (old);
+         return;
+       }
     }
 
   if (ctype_isKnown (newType))
     {
       llassert (ctype_isFunction (newType));
-
       newRetType = ctype_getReturnType (newType);
     }
 
@@ -8199,7 +8555,7 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old,
                      cstring nnamefix;
 
                      if (cstring_isDefined (pfx)
-                         && cstring_equalPrefix (oldname, cstring_toCharsSafe (pfx)))
+                         && cstring_equalPrefix (oldname, pfx))
                        {
                          oname = cstring_suffix (oldname, cstring_length (pfx));
                        }
@@ -8209,7 +8565,7 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old,
                        /*@-branchstate@*/ } /*@=branchstate@*/
 
                      if (cstring_isDefined (pfx)
-                         && cstring_equalPrefix (nname, cstring_toCharsSafe (pfx)))
+                         && cstring_equalPrefix (nname, pfx))
                        {
                          nnamefix = cstring_suffix (nname, cstring_length (pfx));
                        }
@@ -8304,7 +8660,7 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old,
 
              paramno++;  
              /*
-              ** Forgot this!  detected by lclint:
+              ** Forgot this!  detected by splint:
               ** uentry.c:1257,15: Suspected infinite loop
               */
            }
@@ -8346,24 +8702,20 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old,
            }
          */
 
-         /*@i23 need checking @*/ 
-
+         /* need to add some checking @*/ 
          old->info->fcn->specclauses = unew->info->fcn->specclauses;
        }
       else
        {
-         /*@i43 should be able to append? @*/
+         /* should be able to append? */
 
          stateClauseList_checkEqual (old, unew);
          stateClauseList_free (unew->info->fcn->specclauses);
          unew->info->fcn->specclauses = stateClauseList_undefined;
          /*@-branchstate@*/ 
        }
-      /*@=branchstate@*/ /*@i23 shouldn't need this@*/
     }
-
-  DPRINTF (("After state: %s",
-           uentry_unparseFull (old)));
+  /*@=branchstate@*/ /* shouldn't need this */
 
   if (fileloc_isUndefined (old->whereDeclared))
     {
@@ -8377,7 +8729,8 @@ checkFunctionConformance (/*@unique@*/ /*@notnull@*/ uentry old,
     {
       /* no change */
     }
-}
+  /*@-compmempass@*/
+} /*@=compmempass@*/ /* I think this is a spurious warning */
 
 void
 uentry_mergeConstantValue (uentry ue, /*@only@*/ multiVal m)
@@ -8387,7 +8740,8 @@ uentry_mergeConstantValue (uentry ue, /*@only@*/ multiVal m)
   llassert (uentry_isValid (ue));
   llassert (uentry_isEitherConstant (ue));
 
-  uval = ue->info->uconst->val;
+  DPRINTF (("Constant value: %s / %s", uentry_unparse (ue), multiVal_unparse (m)));
+  uval = uentry_getConstantValue (ue);
 
   if (multiVal_isDefined (uval))
     {
@@ -8411,8 +8765,7 @@ uentry_mergeConstantValue (uentry ue, /*@only@*/ multiVal m)
     }
   else
     {
-      ue->info->uconst->val = m;
-      multiVal_free (uval);
+      uentry_setConstantValue (ue, m);
     }
 }
 
@@ -8594,10 +8947,10 @@ uentry_checkDatatypeConformance (/*@notnull@*/ uentry old,
        }
     }
   
-  if (unew->info->datatype->abs != MAYBE)
+  if (!qual_isUnknown (unew->info->datatype->abs))
     {
-      if (ynm_isOff (old->info->datatype->abs)
-         && ynm_isOn (unew->info->datatype->abs))
+      if (qual_isConcrete (old->info->datatype->abs)
+         && qual_isEitherAbstract (unew->info->datatype->abs))
        {
          if (!ctype_isDirectBool (old->utype))
            {
@@ -8613,8 +8966,8 @@ uentry_checkDatatypeConformance (/*@notnull@*/ uentry old,
                }
            }
        }
-      else if (ynm_isOn (old->info->datatype->abs)
-              && ynm_isOff (unew->info->datatype->abs))
+      else if (qual_isEitherAbstract (old->info->datatype->abs)
+              && qual_isConcrete (unew->info->datatype->abs))
        {
          if (!ctype_isDirectBool (old->utype))
            {
@@ -8637,7 +8990,7 @@ uentry_checkDatatypeConformance (/*@notnull@*/ uentry old,
     }
   else 
     {
-      if (ynm_isOn (old->info->datatype->abs))
+      if (qual_isEitherAbstract (old->info->datatype->abs))
        {
          old->sref = unew->sref;
          unew->info->datatype->mut = old->info->datatype->mut;
@@ -8686,7 +9039,7 @@ uentry_checkDatatypeConformance (/*@notnull@*/ uentry old,
     }
   else
     {
-      if (ynm_isOn (old->info->datatype->abs))
+      if (qual_isEitherAbstract (old->info->datatype->abs))
        {
          if (ynm_isOn (old->info->datatype->mut) && ynm_isOff (unew->info->datatype->mut))
            {
@@ -8729,14 +9082,14 @@ uentry_checkConstantConformance (/*@notnull@*/ uentry old,
                                 bool mustConform, 
                                 /*@unused@*/ bool completeConform)
 {
-  multiVal oldVal = old->info->uconst->val;
-  multiVal newVal = unew->info->uconst->val;
+  multiVal oldval = uentry_getConstantValue (old);
+  multiVal newval = uentry_getConstantValue (unew);
   
-  if (multiVal_isDefined (oldVal))
+  if (multiVal_isDefined (oldval))
     {
-      if (multiVal_isDefined (newVal))
+      if (multiVal_isDefined (newval))
        {
-         if (!multiVal_equiv (oldVal, newVal))
+         if (!multiVal_equiv (oldval, newval))
            {
              if (mustConform
                  && optgenerror 
@@ -8745,15 +9098,14 @@ uentry_checkConstantConformance (/*@notnull@*/ uentry old,
                            ekind_capName (unew->ukind),
                            uentry_getName (unew), 
                            uentry_isDeclared (old),
-                           multiVal_unparse (newVal)),
+                           multiVal_unparse (newval)),
                   uentry_whereDeclared (unew)))
                {
-                 uentry_showWhereLastExtra (old, multiVal_unparse (oldVal));
+                 uentry_showWhereLastExtra (old, multiVal_unparse (oldval));
                }
            }
          
-         unew->info->uconst->val = multiVal_copy (oldVal);
-         multiVal_free (newVal);
+         uentry_setConstantValue (unew, multiVal_copy (oldval));
        }
       else
        {
@@ -8762,7 +9114,7 @@ uentry_checkConstantConformance (/*@notnull@*/ uentry old,
     }
   else
     {
-      old->info->uconst->val = multiVal_copy (newVal);
+      uentry_setConstantValue (old, multiVal_copy (newval));
     }
 }
 
@@ -8796,14 +9148,14 @@ uentry_checkConformance (/*@unique@*/ /*@notnull@*/ uentry old,
          ** When a function is defined with an unparam macro
          */
 
-         uentry_copyInto (old, unew);
+         uentry_updateInto (old, unew);
          return;
        }
 
       if (uentry_isExpandedMacro (old) 
          && uentry_isEitherConstant (unew))
        {
-         uentry_copyInto (old, unew);
+         uentry_updateInto (old, unew);
          return;
        }
 
@@ -8830,7 +9182,7 @@ uentry_checkConformance (/*@unique@*/ /*@notnull@*/ uentry old,
                    }
                }
 
-             uentry_copyInto (old, unew);
+             uentry_updateInto (old, unew);
              return;
            }
          else
@@ -8867,7 +9219,7 @@ uentry_checkConformance (/*@unique@*/ /*@notnull@*/ uentry old,
                                                              old->whereDefined);
                        }
 
-                     uentry_copyInto (old, unew);
+                     uentry_updateInto (old, unew);
                      old->used = unew->used = TRUE;
                      return;
                    }
@@ -9034,6 +9386,84 @@ uentry_checkConformance (/*@unique@*/ /*@notnull@*/ uentry old,
   sRef_storeState (unew->sref);
 }
 
+static void uentry_mergeConstraints (uentry spec, uentry def)
+{
+  if (uentry_isFunction (def))
+    {
+      DPRINTF (("Here: %s / %s",
+               uentry_unparseFull (spec),
+               uentry_unparseFull (def)));
+      /* evans 2001-07-21 */
+      llassert (uentry_isFunction (spec));
+
+      if (functionConstraint_isDefined (def->info->fcn->preconditions))
+       {
+         if (fileloc_isXHFile (uentry_whereLast (def)))
+           {
+             llassert (uentry_isFunction (spec));
+             spec->info->fcn->preconditions = functionConstraint_conjoin (spec->info->fcn->preconditions,
+                                                                          def->info->fcn->preconditions);
+           }
+         else if (fileloc_equal (uentry_whereLast (spec), uentry_whereLast (def)))
+           {
+             ;
+           }
+         else
+           {
+             /* Check if the constraints are identical */
+
+             if (optgenerror 
+                 (FLG_INCONDEFS,
+                  message
+                  ("Preconditions for %q redeclared. Dropping previous precondition: %q",
+                   uentry_getName (spec),
+                   functionConstraint_unparse (spec->info->fcn->preconditions)),
+                  uentry_whereLast (def)))
+               {
+                 uentry_showWhereSpecified (spec);
+               }
+
+             functionConstraint_free (spec->info->fcn->preconditions);
+             spec->info->fcn->preconditions = def->info->fcn->preconditions;
+           }
+         
+         def->info->fcn->preconditions = functionConstraint_undefined;
+       }
+
+      if (functionConstraint_isDefined (def->info->fcn->postconditions))
+       {
+         if (fileloc_isXHFile (uentry_whereLast (def)))
+           {
+             llassert (uentry_isFunction (spec));
+             DPRINTF (("Post: %s /++/ %s",
+                       functionConstraint_unparse (spec->info->fcn->postconditions),
+                       functionConstraint_unparse (def->info->fcn->postconditions)));
+             spec->info->fcn->postconditions = functionConstraint_conjoin (spec->info->fcn->postconditions,
+                                                                           def->info->fcn->postconditions);
+             def->info->fcn->postconditions = functionConstraint_undefined;
+             DPRINTF (("Conjoined post: %s", functionConstraint_unparse (spec->info->fcn->postconditions)));
+           }
+         else
+           {
+             if (optgenerror 
+                 (FLG_INCONDEFS,
+                  message
+                  ("Postconditions for %q redeclared. Dropping previous postcondition: %q",
+                   uentry_getName (spec),
+                   functionConstraint_unparse (spec->info->fcn->postconditions)),
+                  uentry_whereLast (def)))
+               {
+                 uentry_showWhereSpecified (spec);
+               }
+             
+             functionConstraint_free (spec->info->fcn->postconditions);
+             spec->info->fcn->postconditions = def->info->fcn->postconditions;
+             def->info->fcn->postconditions = functionConstraint_undefined;
+           }
+       }
+    }
+}
+
 /*
 ** modifies spec to reflect def, reports any inconsistencies
 */
@@ -9044,11 +9474,27 @@ uentry_mergeEntries (uentry spec, /*@only@*/ uentry def)
   llassert (uentry_isValid (spec));
   llassert (uentry_isValid (def));
   llassert (cstring_equal (spec->uname, def->uname));
+
+  if (uentry_isFunction (def))
+    {
+      if (uentry_isConstant (spec))
+       {
+         llassert (ctype_isUnknown (spec->utype) || ctype_isFunction (spec->utype));
+         uentry_makeConstantFunction (spec);
+       }
+      else
+       {
+         uentry_convertVarFunction (spec);
+       }
+
+      llassert (uentry_isFunction (spec));
+    }
   
-  DPRINTF (("Merge entries: %s / %s",
-           uentry_unparseFull (spec),
+  DPRINTF (("Merge entries: %s / %s", uentry_unparseFull (spec),
            uentry_unparseFull (def)));
 
+  uentry_mergeConstraints (spec, def);
+
   uentry_checkConformance (spec, def, TRUE, 
                           context_getFlag (FLG_NEEDSPEC));
 
@@ -9161,7 +9607,7 @@ uentry_checkDecl (void)
 void
 uentry_mergeDefinition (uentry old, /*@only@*/ uentry unew)
 {
-  fileloc olddef = uentry_whereDeclared (old);
+  fileloc olddef = uentry_whereDeclared (old); 
   fileloc unewdef = uentry_whereDeclared (unew);
   bool mustConform;
   bool wasForward;
@@ -9170,15 +9616,10 @@ uentry_mergeDefinition (uentry old, /*@only@*/ uentry unew)
            uentry_unparseFull (old),
            uentry_unparseFull (unew)));
  
-  if (uentry_isExtern (unew))
-    {
-      uentry_setUsed (old, unewdef);
-    }
-
   wasForward = 
     fileloc_isUndefined (olddef) 
-      && fileloc_isDefined (uentry_whereDefined (old)) 
-       && !uentry_isExpandedMacro (old);
+    && fileloc_isDefined (uentry_whereDefined (old)) 
+    && !uentry_isExpandedMacro (old);
   
   if (!context_getFlag (FLG_INCONDEFSLIB)
       && (fileloc_isLib (olddef) || fileloc_isImport (olddef)))
@@ -9194,6 +9635,45 @@ uentry_mergeDefinition (uentry old, /*@only@*/ uentry unew)
   llassert (uentry_isValid (unew));
   llassert (cstring_equal (old->uname, unew->uname));
 
+  if (uentry_isFunction (unew) && !uentry_isFunction (old))
+    {
+      if (uentry_isConstant (old))
+       {
+         llassert (ctype_isUnknown (old->utype) || ctype_isFunction (old->utype));
+         uentry_makeConstantFunction (old);
+       }
+      else
+       {
+         uentry_convertVarFunction (old);
+       }
+
+      if (!uentry_isFunction (old))
+       {
+         if (optgenerror 
+             (FLG_INCONDEFS,
+              message ("%s %q declared as function, but previously declared as %s",
+                       ekind_capName (unew->ukind),
+                       uentry_getName (unew),
+                       ekind_unparseLong (old->ukind)),
+              uentry_whereDeclared (unew)))
+           {
+             uentry_showWhereLast (old);
+           }
+
+         uentry_convertIntoFunction (old);
+         return;
+       }
+    }
+
+  DPRINTF (("uentry merge: %s / %s",
+           uentry_unparseFull (old),
+           uentry_unparseFull (unew)));
+
+  if (uentry_isExtern (unew))
+    {
+      uentry_setUsed (old, unewdef);
+    }
+
   /*
   ** should check old one was extern!
   */
@@ -9227,7 +9707,8 @@ uentry_mergeDefinition (uentry old, /*@only@*/ uentry unew)
     }
   else
     {
-      if (!uentry_isExtern (unew) && !uentry_isForward (old)
+      if (!uentry_isExtern (unew) 
+         && !uentry_isForward (old)
          && !fileloc_equal (olddef, unewdef)
          && !fileloc_isUndefined (olddef)
          && !fileloc_isUndefined (unewdef)
@@ -9259,7 +9740,7 @@ uentry_mergeDefinition (uentry old, /*@only@*/ uentry unew)
                  /*
                  if (uentry_isDatatype (old) || uentry_isAnyTag (old))
                    {
-                     uentry_copyInto (old, unew);
+                     uentry_updateInto (old, unew);
                      old->sref = sRef_saveCopy (old->sref);
                    }
                    */
@@ -9297,13 +9778,25 @@ uentry_mergeDefinition (uentry old, /*@only@*/ uentry unew)
                }
              else
                {
-                 uentry_setDefined (old, unewdef);
+                 uentry_setDeclared (old, unewdef); /* evans 2001-07-23 was setDefined */
                }
            }
        }
     }
 
+  DPRINTF (("uentry merge: %s / %s",
+           uentry_unparseFull (old),
+           uentry_unparseFull (unew)));
+
+  uentry_mergeConstraints (old, unew);
+  DPRINTF (("uentry merge: %s / %s",
+           uentry_unparseFull (old),
+           uentry_unparseFull (unew)));
+
   uentry_checkConformance (old, unew, mustConform, FALSE);
+  DPRINTF (("uentry merge: %s / %s",
+           uentry_unparseFull (old),
+           uentry_unparseFull (unew)));
 
   old->used = old->used || unew->used;
   old->uses = filelocList_append (old->uses, unew->uses);
@@ -9318,6 +9811,8 @@ uentry_mergeDefinition (uentry old, /*@only@*/ uentry unew)
                                          fileloc_undefined);
     }
 
+  DPRINTF (("here: %s", uentry_unparseFull (old)));
+
   /*
   ** No redeclaration errors for functions here, since we
   ** don't know if this is the definition of the function.
@@ -9409,6 +9904,7 @@ uentry_mergeDefinition (uentry old, /*@only@*/ uentry unew)
       uentry_checkName (old);
     }
 
+  DPRINTF (("After: %s", uentry_unparseFull (old)));
   llassert (!ctype_isUndefined (old->utype));
 }
 
@@ -9455,39 +9951,101 @@ uentry_sameKind (uentry u1, uentry u2)
   return FALSE;
 }
    
-static void uentry_copyInto (/*@unique@*/ uentry unew, uentry old)
+static void uentry_updateInto (/*@unique@*/ uentry unew, uentry old)
 {
+  ekind okind;
   llassert (uentry_isValid (unew));
   llassert (uentry_isValid (old));
 
+  DPRINTF (("Update into: %s / %s", uentry_unparseFull (unew), uentry_unparseFull (old)));
+  okind = unew->ukind;
   unew->ukind = old->ukind;
-  unew->uname = cstring_copy (old->uname);
+  llassert (cstring_equal (unew->uname, old->uname));
   unew->utype = old->utype;
 
-  unew->whereSpecified = fileloc_copy (old->whereSpecified);
-  unew->whereDefined = fileloc_copy (old->whereDefined);
-  unew->whereDeclared = fileloc_copy (old->whereDeclared);
+  if (fileloc_isDefined (unew->whereSpecified) 
+      && !fileloc_isDefined (old->whereSpecified))
+    {
+      ; /* Keep the old value */
+    }
+  else
+    {
+      fileloc_free (unew->whereSpecified);
+      unew->whereSpecified = fileloc_copy (old->whereSpecified);
+    }
+
+  if (fileloc_isDefined (unew->whereDefined) 
+      && !fileloc_isDefined (old->whereDefined))
+    {
+      ; /* Keep the old value */
+    }
+  else
+    {
+      fileloc_free (unew->whereDefined); 
+      unew->whereDefined = fileloc_copy (old->whereDefined);
+    }
+
+  if (fileloc_isDefined (unew->whereDeclared) 
+      && !fileloc_isDefined (old->whereDeclared))
+    {
+      ; /* Keep the old value */
+    }
+  else
+    {
+      fileloc_free (unew->whereDeclared); 
+      unew->whereDeclared = fileloc_copy (old->whereDeclared);
+    }
+
+  DPRINTF (("Update into: %s / %s", uentry_unparseFull (unew), uentry_unparseFull (old)));
 
   unew->sref = sRef_saveCopy (old->sref); /* Memory leak! */
   unew->used = old->used;
   unew->lset = FALSE;
   unew->isPrivate = old->isPrivate;
   unew->hasNameError = old->hasNameError;
-  unew->uses = filelocList_undefined;
+  unew->uses = filelocList_append (unew->uses, old->uses);
+  old->uses = filelocList_undefined;
 
   unew->storageclass = old->storageclass;
+  uinfo_free (unew->info, okind);
   unew->info = uinfo_copy (old->info, old->ukind);
 }
 
-
-uentry
-uentry_copy (uentry e)
+static uentry
+uentry_copyAux (uentry e, bool saveCopy)
 {
+  
   if (uentry_isValid (e))
     {
       uentry enew = uentry_alloc ();
       DPRINTF (("copy: %s", uentry_unparseFull (e)));
-      uentry_copyInto (enew, e);
+      enew->ukind = e->ukind;
+      enew->uname = cstring_copy (e->uname);
+      enew->utype = e->utype;
+      
+      enew->whereSpecified = fileloc_copy (e->whereSpecified);
+      enew->whereDefined = fileloc_copy (e->whereDefined);
+      enew->whereDeclared = fileloc_copy (e->whereDeclared);
+      
+      if (saveCopy)
+       {
+         enew->sref = sRef_saveCopy (e->sref); /* Memory leak! */
+       }
+      else
+       {
+         enew->sref = sRef_copy (e->sref);
+       }
+      
+      enew->used = e->used;
+      enew->lset = FALSE;
+      enew->isPrivate = e->isPrivate;
+      enew->hasNameError = e->hasNameError;
+      enew->uses = filelocList_undefined;
+      
+      enew->storageclass = e->storageclass;
+      enew->info = uinfo_copy (e->info, e->ukind);
+      enew->warn = warnClause_copy (e->warn);
+
       DPRINTF (("Here we are..."));
       DPRINTF (("original: %s", uentry_unparseFull (e)));
       DPRINTF (("copy: %s", uentry_unparse (enew)));
@@ -9500,6 +10058,18 @@ uentry_copy (uentry e)
     }
 }
 
+uentry
+uentry_copy (uentry e)
+{
+  return uentry_copyAux (e, TRUE);
+}
+
+uentry
+uentry_copyNoSave (uentry e)
+{
+  return uentry_copyAux (e, FALSE);
+}
+
 void
 uentry_setState (uentry res, uentry other)
 {
@@ -9551,8 +10121,8 @@ uentry_mergeUses (uentry res, uentry other)
 */
 
 static void
-  branchStateError (/*@notnull@*/ uentry res, /*@notnull@*/ uentry other, 
-                   bool flip, clause cl, fileloc loc)
+branchStateError (/*@notnull@*/ uentry res, /*@notnull@*/ uentry other, 
+                 bool flip, clause cl, fileloc loc)
 {
   if (optgenerror 
       (FLG_BRANCHSTATE,
@@ -9562,25 +10132,50 @@ static void
                sRef_stateAltVerb (res->sref), clause_nameFlip (cl, !flip)),
        loc))
     {
+      DPRINTF (("Here: %s / %s", sRef_unparseFull (res->sref), sRef_unparseFull (other->sref)));
+
       if (sRef_isDead (res->sref))
        {
-         sRef_showStateInfo (res->sref);
+         if (sRef_hasStateInfoLoc (res->sref)) {
+           llgenindentmsg (message ("%s:", clause_nameFlip (cl, flip)), loc);
+           sRef_showStateInfo (res->sref);
+         }
+
+         if (sRef_hasStateInfoLoc (other->sref)) {
+           llgenindentmsg (message ("%s:", clause_nameFlip (cl, !flip)), loc);
+           sRef_showStateInfo (other->sref);
+         }
        }
       else if (sRef_isKept (res->sref))
        {
-         sRef_showAliasInfo (res->sref);
+         if (sRef_hasAliasInfoLoc (res->sref)) {
+           llgenindentmsg (message ("%s:", clause_nameFlip (cl, flip)), loc);
+           sRef_showAliasInfo (res->sref);
+         }
+
+         if (sRef_hasAliasInfoLoc (other->sref)) {
+           llgenindentmsg (message ("%s:", clause_nameFlip (cl, !flip)), loc);
+           sRef_showAliasInfo (other->sref);
+         }
        }
       else /* dependent */
        {
-         sRef_showAliasInfo (res->sref);
-         sRef_showAliasInfo (other->sref);
+         if (sRef_hasAliasInfoLoc (res->sref)) {
+           llgenindentmsg (message ("%s:", clause_nameFlip (cl, flip)), loc);
+           sRef_showAliasInfo (res->sref);
+         }
+
+         if (sRef_hasAliasInfoLoc (other->sref)) {
+           llgenindentmsg (message ("%s:", clause_nameFlip (cl, !flip)), loc);
+           sRef_showAliasInfo (other->sref);
+         }
        }
       
       sRef_setAliasKind (res->sref, AK_ERROR, fileloc_undefined);
     }
 }
 
-static bool incompatibleStates (sRef rs, sRef os)
+static bool uentry_incompatibleMemoryStates (sRef rs, sRef os)
 {
   alkind rk = sRef_getAliasKind (rs);
   alkind ok = sRef_getAliasKind (os);
@@ -9614,11 +10209,27 @@ static void
     {
       if (sRef_isDead (other->sref))
        {
-         sRef_showStateInfo (other->sref);
+         if (sRef_hasStateInfoLoc (other->sref)) {
+           llgenindentmsg (message ("%s:", clause_nameFlip (cl, flip)), loc);
+           sRef_showStateInfo (other->sref);
+         }
+
+         if (sRef_hasStateInfoLoc (res->sref)) {
+           llgenindentmsg (message ("%s:", clause_nameFlip (cl, !flip)), loc);
+           sRef_showStateInfo (res->sref);
+         }
        }
       else /* kept */
        {
-         sRef_showAliasInfo (other->sref);
+         if (sRef_hasAliasInfoLoc (other->sref)) {
+           llgenindentmsg (message ("%s:", clause_nameFlip (cl, flip)), loc);
+           sRef_showAliasInfo (other->sref);
+         }
+
+         if (sRef_hasAliasInfoLoc (res->sref)) {
+           llgenindentmsg (message ("%s:", clause_nameFlip (cl, !flip)), loc);
+           sRef_showAliasInfo (res->sref);
+         }
        }
       
       sRef_setAliasKind (res->sref, AK_ERROR, fileloc_undefined);
@@ -9655,33 +10266,36 @@ static bool uentry_relevantReference (sRef sr, bool flip)
 }
 
 static void
-uentry_mergeAliasStates (uentry res, uentry other, fileloc loc,
-                        bool mustReturn, bool flip, bool opt,
+uentry_mergeAliasStates (/*@notnull@*/ uentry res, /*@notnull@*/ uentry other, 
+                        fileloc loc, bool mustReturn, bool flip, bool opt,
                         clause cl)    
 {
+  sRef rs = res->sref;
+  sRef os = other->sref;
+
   DPRINTF (("Merge alias states: %s / %s",
            uentry_unparseFull (res),
            uentry_unparseFull (other)));
 
-  if (sRef_isValid (res->sref))
+  if (sRef_isValid (rs))
     {
       if (!mustReturn)
        {
-         DPRINTF (("1"));
-         if (incompatibleStates (res->sref, other->sref))
+         if (uentry_incompatibleMemoryStates (rs, os))
            {
-             DPRINTF (("2"));
+             DPRINTF (("Incompatible: \n\t%s / \n\t%s",
+                       sRef_unparseFull (rs), sRef_unparseFull (os)));
 
-             if (sRef_isThroughArrayFetch (res->sref)
+             if (sRef_isThroughArrayFetch (rs)
                  && !context_getFlag (FLG_STRICTBRANCHSTATE))
                {
-                 if (sRef_isKept (res->sref) || sRef_isKept (other->sref))
+                 if (sRef_isKept (rs) || sRef_isKept (os))
                    {
-                     sRef_maybeKill (res->sref, loc);
+                     sRef_maybeKill (rs, loc);
                    }
-                 else if (sRef_isPossiblyDead (other->sref))
+                 else if (sRef_isPossiblyDead (os))
                    {
-                     sRef_maybeKill (res->sref, loc);
+                     sRef_maybeKill (rs, loc);
                    }
                  else
                    {
@@ -9690,56 +10304,56 @@ uentry_mergeAliasStates (uentry res, uentry other, fileloc loc,
                }
              else
                {
-                 if (uentry_relevantReference (other->sref, flip))
+                 if (uentry_relevantReference (os, flip))
                    {
-                     DPRINTF (("4"));
-                     if (sRef_isLocalParamVar (res->sref) 
-                         && (sRef_isLocalState (other->sref) 
-                             || sRef_isDependent (other->sref)))
+                     if (sRef_isLocalParamVar (rs) 
+                         && (sRef_isLocalState (os) 
+                             || sRef_isDependent (os)))
                        {
-                         if (sRef_isDependent (res->sref))
+                         if (sRef_isDependent (rs))
                            {
-                             sRef_setDependent (other->sref, loc);
+                             sRef_setDependent (os, loc);
                            }
                          else
                            {
-                             sRef_setDefState (res->sref, SS_UNUSEABLE, loc);
+                             sRef_setDefState (rs, SS_UNUSEABLE, loc);
                            }
                        }
                      else 
                        {
-                         branchStateError (res, other, flip, cl, loc);
+                         branchStateError (res, other, !flip, cl, loc); /* evans 2002-12-15: changed flip to !flip */
                        }
                    }
                }
              
-             if (sRef_isKept (res->sref))
+             if (sRef_isKept (rs))
                {
-                 sRef_setKept (other->sref, loc);
+                 DPRINTF (("Setting kept: %s", sRef_unparseFull (os)));
+                 sRef_setKept (os, loc);
                }
            }
          else
            {
-             if (incompatibleStates (other->sref, res->sref))
+             if (uentry_incompatibleMemoryStates (os, rs))
                {
-                 if (uentry_relevantReference (res->sref, !flip))
+                 if (uentry_relevantReference (rs, !flip))
                    {
-                     if (sRef_isLocalParamVar (res->sref
-                         && (sRef_isDependent (res->sref)
-                             || sRef_isLocalState (res->sref)))
+                     if (sRef_isLocalParamVar (rs
+                         && (sRef_isDependent (rs)
+                             || sRef_isLocalState (rs)))
                        {
-                         if (sRef_isDependent (other->sref))
+                         if (sRef_isDependent (os))
                            {
-                             sRef_setDependent (res->sref, loc);
+                             sRef_setDependent (rs, loc);
                            }
                          else
                            {
-                             sRef_setDefState (res->sref, SS_UNUSEABLE, loc);
+                             sRef_setDefState (rs, SS_UNUSEABLE, loc);
                            }
                        }
                      else
                        {
-                         if (sRef_isParam (other->sref))
+                         if (sRef_isParam (os))
                            {
                              /* 
                              ** If the local variable associated
@@ -9751,9 +10365,9 @@ uentry_mergeAliasStates (uentry res, uentry other, fileloc loc,
                              uentry uvar = usymtab_lookupSafe (other->uname);
                              
                              if (uentry_isValid (uvar)
-                                 && ((sRef_isDead (other->sref
+                                 && ((sRef_isDead (os
                                       && sRef_isOnly (uvar->sref))
-                                     || (sRef_isDependent (other->sref)
+                                     || (sRef_isDependent (os)
                                          && sRef_isOwned (uvar->sref))))
                                {
                                  /* no error */
@@ -9777,41 +10391,52 @@ uentry_mergeAliasStates (uentry res, uentry other, fileloc loc,
                    }
                }
              
-             if (sRef_isKept (other->sref))
+             if (sRef_isKept (os))
                {
-                 sRef_setKept (res->sref, loc);
+                 sRef_setKept (rs, loc);
                }
            }
          
          if (opt)
            {
              DPRINTF (("Merge opt..."));
-             sRef_mergeOptState (res->sref, other->sref, cl, loc);
+             sRef_mergeOptState (rs, os, cl, loc);
              DPRINTF (("Done!"));
            }
          else
            {
-             sRef_mergeState (res->sref, other->sref, cl, loc);
+             DPRINTF (("Merging states: \n\t%s / \n\t%s", sRef_unparseFull (rs), sRef_unparseFull (os)));
+             sRef_mergeState (rs, os, cl, loc);
+             DPRINTF (("After merging : \n\t%s / \n\t%s", sRef_unparseFull (rs), sRef_unparseFull (os)));
            }
        }
       else
        {
-         if (sRef_isModified (other->sref))
+         if (sRef_isModified (os))
            {
-             sRef_setModified (res->sref);
+             sRef_setModified (rs);
            }
        }
     }
+
+  DPRINTF (("After merge: %s", sRef_unparseFull (res->sref)));
 }
 
 static void
-uentry_mergeValueStates (uentry res, uentry other, fileloc loc)
+uentry_mergeValueStates (/*@notnull@*/ uentry res, /*@notnull@*/ uentry other,
+                        fileloc loc, bool mustReturn, /*@unused@*/ bool flip)
 {
   valueTable rvalues;
   valueTable ovalues;
 
   DPRINTF (("Merge values: %s / %s", sRef_unparseFull (res->sref), sRef_unparseFull (other->sref)));
   
+  if (mustReturn)
+    {
+      return;
+    }
+  /* flip? */
+
   rvalues = sRef_getValueTable (res->sref);
   ovalues = sRef_getValueTable (other->sref);
   
@@ -9826,10 +10451,7 @@ uentry_mergeValueStates (uentry res, uentry other, fileloc loc)
       ** Copy values from other
       */
       
-      /*@i$@#@*/
-      DPRINTF (("Has value table: %s", sRef_unparseFull (other->sref)));
-      DPRINTF (("No value table: %s", sRef_unparseFull (res->sref)));
-      ;
+      /* ??? */
     }
   else
     {
@@ -9862,7 +10484,7 @@ uentry_mergeValueStates (uentry res, uentry other, fileloc loc)
              {
                sRef_setMetaStateValueComplete (res->sref, 
                                                fkey, stateValue_getValue (fval), 
-                                               loc);
+                                               stateValue_getLoc (fval));
                DPRINTF (("Setting res: %s", sRef_unparseFull (res->sref)));
              }
            else if (stateValue_isError (tval)
@@ -9870,6 +10492,11 @@ uentry_mergeValueStates (uentry res, uentry other, fileloc loc)
              {
                DPRINTF (("Other branch is definitely null!"));
              }
+           else if (sRef_isStateUndefined (res->sref)
+                    || sRef_isDead (res->sref))
+             {
+               ; /* Combination state doesn't matter if it is undefined or dead */
+             }
            else 
              {
                DPRINTF (("Check: %s / %s / %s / %s", fkey,
@@ -9895,19 +10522,18 @@ uentry_mergeValueStates (uentry res, uentry other, fileloc loc)
                DPRINTF (("nval: %d / %d / %d", nval,
                          stateValue_getValue (fval), stateValue_getValue (tval)));
 
-               if (cstring_isDefined (msg)) 
+               if (nval == stateValue_error)
                  {
-                   /*@i32 print extra info for assignments@*/
-
                    if (uentry_isGlobalMarker (res))
                      {
                        if (optgenerror 
                            (FLG_STATEMERGE,
                             message
-                            ("Control branches merge with incompatible global states (%s and %s): %s",
+                            ("Control branches merge with incompatible global states (%s and %s)%q",
                              metaStateInfo_unparseValue (minfo, stateValue_getValue (fval)),
                              metaStateInfo_unparseValue (minfo, stateValue_getValue (tval)),
-                             msg),
+                             cstring_isDefined (msg) 
+                             ? message (": %s", msg) : cstring_undefined),
                             loc))
                          {
                            sRef_showMetaStateInfo (res->sref, fkey);
@@ -9919,11 +10545,12 @@ uentry_mergeValueStates (uentry res, uentry other, fileloc loc)
                        if (optgenerror 
                            (FLG_STATEMERGE,
                             message
-                            ("Control branches merge with incompatible states for %q (%s and %s): %s",
+                            ("Control branches merge with incompatible states for %q (%s and %s)%q",
                              uentry_getName (res),
                              metaStateInfo_unparseValue (minfo, stateValue_getValue (fval)),
                              metaStateInfo_unparseValue (minfo, stateValue_getValue (tval)),
-                             msg),
+                             cstring_isDefined (msg) 
+                             ? message (": %s", msg) : cstring_undefined),
                             loc))
                          {
                            sRef_showMetaStateInfo (res->sref, fkey);
@@ -9971,7 +10598,8 @@ uentry_mergeValueStates (uentry res, uentry other, fileloc loc)
 
 
 static void
-uentry_mergeSetStates (uentry res, uentry other, /*@unused@*/ fileloc loc,
+uentry_mergeSetStates (/*@notnull@*/ uentry res,
+                      /*@notnull@*/ uentry other, /*@unused@*/ fileloc loc,
                       bool flip, clause cl)
 {
   if (cl == DOWHILECLAUSE)
@@ -10049,8 +10677,10 @@ uentry_mergeState (uentry res, uentry other, fileloc loc,
            uentry_unparseFull (other)));
   
   uentry_mergeAliasStates (res, other, loc, mustReturn, flip, opt, cl);
-  uentry_mergeValueStates (res, other, loc);
+  uentry_mergeValueStates (res, other, loc, mustReturn, flip);
   uentry_mergeSetStates (res, other, loc, flip, cl);
+
+  DPRINTF (("Merge ==> %s", uentry_unparseFull (res)));
 }
 
 void uentry_setUsed (uentry e, fileloc loc)
@@ -10073,8 +10703,6 @@ void uentry_setUsed (uentry e, fileloc loc)
 
   if (uentry_isValid (e))
     {
-      int dp;
-
       if (warnClause_isDefined (e->warn))
        {
          flagSpec flg = warnClause_getFlag (e->warn);
@@ -10133,9 +10761,9 @@ void uentry_setUsed (uentry e, fileloc loc)
            }
        }
       
-      if ((dp = uentry_directParamNo (e)) >= 0)
+      if (usymId_isValid (usymtab_directParamNo (e)))
        {
-         uentry_setUsed (usymtab_getParam (dp), loc);
+         uentry_setUsed (usymtab_getParam (usymId_toInt (usymtab_directParamNo (e))), loc);
        }
       
       e->used = TRUE;
@@ -10174,7 +10802,7 @@ bool uentry_isReturned (uentry u)
              || u->info->var->kind == VKSEFRETPARAM));
 }
 
-/*@exposed@*/ sRef uentry_returnedRef (uentry u, exprNodeList args)
+/*@exposed@*/ sRef uentry_returnedRef (uentry u, exprNodeList args, fileloc loc)
 {
   llassert (uentry_isRealFunction (u));
 
@@ -10184,11 +10812,15 @@ bool uentry_isReturned (uentry u)
       sRef res = sRef_makeNew (ctype_getReturnType (u->utype), u->sref, u->uname);
 
       DPRINTF (("Returned: %s", sRef_unparseFull (res)));
-      sRef_setAllocated (res, g_currentloc);
+      sRef_setAllocated (res, loc);
 
       DPRINTF (("ensures clause: %s / %s", uentry_unparse (u), 
                stateClauseList_unparse (clauses)));
 
+      /*
+      ** This should be in exprNode_reflectEnsuresClause
+      */
+
       stateClauseList_postElements (clauses, cl)
        {
          if (!stateClause_isGlobal (cl))
@@ -10205,7 +10837,7 @@ bool uentry_isReturned (uentry u)
                      if (modf != NULL)
                        {
                          sRef sr = sRef_fixBase (el, res);
-                         modf (sr, g_currentloc);
+                         modf (sr, loc);
                        }
                    }
                  else
@@ -10215,7 +10847,7 @@ bool uentry_isReturned (uentry u)
                } end_sRefSet_elements ;
            }
        } end_stateClauseList_postElements ;
-
+       
       return res;
     }
   else
@@ -10245,19 +10877,25 @@ bool uentry_isReturned (uentry u)
                      
                      usymtab_addForceMustAlias (tcref, tref); /* evans 2001-05-27 */
 
+                     if (sRef_isNew (tcref))
+                       {
+                         /* tcref->kind = SK_OBJECT; */ /*!! Not new anymore */
+                       }
+
                      if (sRef_isDead (tcref))
                        {
-                         sRef_setDefined (tcref, g_currentloc);
-                         sRef_setOnly (tcref, g_currentloc);
+                         sRef_setDefined (tcref, loc);
+                         sRef_setOnly (tcref, loc);
                        }
                      
                      if (sRef_isRefCounted (tcref))
                        {
                          /* could be a new ref now (but only if its returned) */
-                         sRef_setAliasKindComplete (tcref, AK_ERROR, g_currentloc);
+                         sRef_setAliasKindComplete (tcref, AK_ERROR, loc);
                        }
                      
                      sRef_makeSafe (tcref);
+                     DPRINTF (("Returns tcref / %s", sRef_unparseFull (tcref)));
                      prefs = sRefSet_insert (prefs, tcref);
                    }
                }
@@ -10276,13 +10914,13 @@ bool uentry_isReturned (uentry u)
            }
          else
            {
-             /* should this ever happen? */ /*@i534 evans 2001-05-27 */
+             /* should this ever happen? */
              res = sRefSet_mergeIntoOne (prefs);
            }
          
          if (nstate_isKnown (n))
            {
-             sRef_setNullState (res, n, g_currentloc);
+             sRef_setNullState (res, n, loc);
            }
        }
       else
@@ -10299,7 +10937,7 @@ bool uentry_isReturned (uentry u)
          
          if (sRef_isRefCounted (res))
            {
-             sRef_setAliasKind (res, AK_NEWREF, g_currentloc);
+             sRef_setAliasKind (res, AK_NEWREF, loc);
            }
        }
       
@@ -10310,7 +10948,7 @@ bool uentry_isReturned (uentry u)
          
          if (ctype_isAbstract (ct))
            {
-             sRef_setNotNull (res, g_currentloc);
+             sRef_setNotNull (res, loc);
            }
          else
            {
@@ -10320,18 +10958,18 @@ bool uentry_isReturned (uentry u)
                }
              else
                {
-                 sRef_setNotNull (res, g_currentloc);
+                 sRef_setNotNull (res, loc);
                }
            }
        }
       
       if (sRef_isRefCounted (res))
        {
-         sRef_setAliasKind (res, AK_NEWREF, g_currentloc);
+         sRef_setAliasKind (res, AK_NEWREF, loc);
        }
       else if (sRef_isKillRef (res))
        {
-         sRef_setAliasKind (res, AK_REFCOUNTED, g_currentloc);
+         sRef_setAliasKind (res, AK_REFCOUNTED, loc);
        }
       else
        {
@@ -10344,11 +10982,18 @@ bool uentry_isReturned (uentry u)
        {
          sRef_setAliasKind (res, 
                             alkind_fixImplicit (ak),
-                            g_currentloc);
+                            loc);
        }
       
       sRefSet_free (prefs);
-      
+
+      /*
+      if (sRef_isOnly (res))
+       {
+         sRef_setFresh (res, loc);
+       }
+      */
+
       DPRINTF (("Returns ref: %s", sRef_unparseFull (res)));
       return res;
     }
@@ -10598,13 +11243,15 @@ void uentry_checkName (uentry ue)
     }
 }
 
-/*@exposed@*/ uentry uentry_makeUnrecognized (cstring c, /*@keep@*/ fileloc loc)
+/*@exposed@*/ uentry uentry_makeUnrecognized (cstring c, /*@only@*/ fileloc loc)
 {
   uentry ue;
   fileloc tloc;
 
   /*
-  ** Can't but unrecognized ids in macros in global scope, because srefs will break! */
+  ** Can't but unrecognized ids in macros in global scope, because srefs will break! 
+  */
+
   if (!context_inMacro ())
     {
       sRef_setGlobalScopeSafe ();
@@ -10618,7 +11265,7 @@ void uentry_checkName (uentry ue)
   fileloc_free (tloc);
   uentry_setHasNameError (ue);
   
-  if (context_getFlag (FLG_REPEATUNRECOG))
+  if (context_getFlag (FLG_REPEATUNRECOG) || (context_inOldStyleScope()))
     {
       uentry_markOwned (ue);
     }
@@ -10663,60 +11310,8 @@ bool uentry_isGlobalMarker (uentry ue)
          && (cstring_equal (uentry_rawName (ue), GLOBAL_MARKER_NAME)));
 }
 
-
-//
 /* new start modifications */
 
-/*@ignore@*/
-
-
-
-  
-static  void uentry_testInRange (uentry p_e, uentry cconstant)  {
-  if( uentry_isValid(p_e) ) {
-    if( sRef_isValid (p_e->sref) ) {
-      char * t = cstring_toCharsSafe (uentry_unparse(cconstant) );
-      int index = atoi( t );
-      free (t);
-      //      usymtab_testInRange (p_e->sref, index);
-    }//end if
-  }//endif
-}
-
-
-/*  void uentry_setStringLength (uentry p_e, uentry cconstant)  { */
-/*  if( uentry_isValid(p_e) ) { */
-/*    if( p_e->info != NULL) { */
-/*      if( p_e->info->var != NULL) { */
-/*        char *t =  cstring_toCharsSafe (uentry_unparse(cconstant)); */
-/*        int length = atoi( t ); */
-/*        free (t); */
-/*        p_e->info->var->bufinfo->len = length;  */
-/*        p_e->sref->bufinfo.len = length; */
-/*        printf("Set string length of buff to %d \n",  p_e->sref->bufinfo.size); */
-/*      }//end if */
-/*    }//endif */
-/*  }//end if */
-/*  } */
-
-
-static void uentry_setBufferSize (uentry p_e, exprNode cconstant) {
-if( uentry_isValid(p_e) ) {
-  if( p_e->info != NULL) {
-    if( p_e->info->var != NULL) {
-      int size = atoi(cstring_toCharsSafe(exprNode_unparse(cconstant) ) ); 
-      p_e->info->var->bufinfo->size = size; 
-      p_e->sref->bufinfo.size = size;
-      printf("Set buffer size to %d \n",  p_e->sref->bufinfo.size);
-      //  fprintf(stderr, "For %s and %s\n", uentry_unparse(p_e) );
-      // fprintf(stderr, "and %d\n", size );
-      
-    }//end if
-  }//endif
-}//end if
-}
-
-  
 /* start modifications */
 /*
 requires: p_e is defined, is a ptr/array variable 
@@ -10725,18 +11320,19 @@ effects: sets the state of the variable
 */
 
 
-void uentry_setPossiblyNullTerminatedState (uentry p_e)  {
-  if( uentry_isValid(p_e) ) {
-    if( p_e->info != NULL) {
-      if( p_e->info->var != NULL) {
-         p_e->info->var->bufinfo->bufstate = BB_POSSIBLYNULLTERMINATED;
-         p_e->sref->bufinfo.bufstate = BB_POSSIBLYNULLTERMINATED;
-         return;
-      }/* End if */
-    }/* End if */
-  }/* End if */
+void uentry_setPossiblyNullTerminatedState (uentry p_e)  
+{
+  llassert (uentry_isValid (p_e));
 
-  fprintf(stderr, "uentry:Error in setPossiblyNullTerminatedState\n");
+  if (p_e->info != NULL)
+    {
+      if (p_e->info->var != NULL) 
+       {
+         llassert (p_e->info->var->bufinfo != NULL);
+         p_e->info->var->bufinfo->bufstate = BB_POSSIBLYNULLTERMINATED;
+         sRef_setPossiblyNullTerminatedState (p_e->sref);
+       }
+    }
 }
 
 /*
@@ -10746,80 +11342,121 @@ effects: sets the size of the buffer
 */
 
 void uentry_setNullTerminatedState (uentry p_e)  {
-  if( uentry_isValid(p_e) ) {
-    if( p_e->info != NULL) {
-      if( p_e->info->var != NULL) {
-        p_e->info->var->bufinfo->bufstate = BB_NULLTERMINATED;
-        p_e->sref->bufinfo.bufstate = BB_NULLTERMINATED;
-        return;
-      }//End if
-    }//End if
-  }//End if
+  llassert (uentry_isValid (p_e));
 
-  fprintf(stderr, "uentry:Error in setNullTerminatedState\n");
+  if (p_e->info != NULL)
+    {
+      if (p_e->info->var != NULL)
+       {
+         llassert (p_e->info->var->bufinfo != NULL);
+         p_e->info->var->bufinfo->bufstate = BB_NULLTERMINATED;
+         sRef_setNullTerminatedState (p_e->sref);
+       }
+    }
 }
 
-
 /*
 requires: p_e is defined, is a ptr/array variable 
 modifies: p_e
-effects: sets the state of the variable
+effects: sets the size of the buffer
 */
 
-/*  void uentry_setNotNullTerminatedState (uentry p_e)  { */
-/*    if( uentry_isValid(p_e) ) { */
-/*      if( p_e->info != NULL) { */
-/*        if( p_e->info->var != NULL) { */
-/*          p_e->info->var->bufinfo->bufstate = BB_NOTNULLTERMINATED; */
-/*          p_e->sref->bufinfo.bufstate = BB_NOTNULLTERMINATED; */
-/*          return; */
-/*        }//End if */
-/*      }//End if */
-/*    }//End if */
-
-/*    fprintf(stderr, "uentry:Error in setNotNullTerminatedState\n"); */
-/*  } */
-
+void uentry_setSize (uentry p_e, int size)  
+{
+  if (uentry_isValid (p_e))
+    {
+      if (p_e->info != NULL) 
+       {
+         if (p_e->info->var != NULL) 
+           {
+             llassert (p_e->info->var->bufinfo != NULL);
+             p_e->info->var->bufinfo->size = size;
+             sRef_setSize (p_e->sref, size);
+           }
+       }
+    }
+}
 
 /*
 requires: p_e is defined, is a ptr/array variable 
 modifies: p_e
-effects: sets the size of the buffer
+effects: sets the length of the buffer
 */
 
-void uentry_setSize (uentry p_e, int size)  {
-  if( uentry_isValid(p_e) ) {
-    if( p_e->info != NULL) {
-      if( p_e->info->var != NULL) {
-        p_e->info->var->bufinfo->size = size;
-        p_e->sref->bufinfo.size = size;
-        return;
-      }//End if
-    }//End if
-  }//End if
+void uentry_setLen (uentry p_e, int len)  
+{
+  if (uentry_isValid (p_e)) 
+    {
+      if (p_e->info != NULL
+         && p_e->info->var != NULL) 
+       {
+         llassert (p_e->info->var->bufinfo != NULL);
+         p_e->info->var->bufinfo->len = len;
+         sRef_setLen (p_e->sref, len);
+       }
+    }
+}
+
+/*@=type*/
 
-  fprintf(stderr, "uentry:Error in setSize\n");
+bool uentry_hasMetaStateEnsures (uentry e)
+{
+  if (uentry_isValid (e) && uentry_isFunction (e))
+    {
+      return functionConstraint_hasMetaStateConstraint (e->info->fcn->postconditions);
+    }
+  else
+    {
+      return FALSE;
+    }
 }
 
+metaStateConstraintList uentry_getMetaStateEnsures (uentry e)
+{
+  llassert (uentry_isValid (e) && uentry_isFunction (e));
+  return functionConstraint_getMetaStateConstraints (e->info->fcn->postconditions);
+}
+
+
+bool uentry_hasBufStateInfo (uentry ue)
+{
+  llassert (uentry_isValid (ue));
+  return (ue->info->var->bufinfo != NULL);
+}
+
+bool uentry_isNullTerminated (uentry ue)
+{
+  llassert (uentry_hasBufStateInfo (ue));
+  llassert (ue->info->var->bufinfo != NULL);
+  return ue->info->var->bufinfo->bufstate == BB_NULLTERMINATED;
+}
+
+bool uentry_isPossiblyNullTerminated (uentry ue)
+{
+  llassert (uentry_hasBufStateInfo (ue));
+  llassert (ue->info->var->bufinfo != NULL);
+  return (ue->info->var->bufinfo->bufstate == BB_POSSIBLYNULLTERMINATED);
+}
+
+bool uentry_isNotNullTerminated (uentry ue)
+{
+  llassert (uentry_hasBufStateInfo (ue));
+  llassert (ue->info->var->bufinfo != NULL);
+  return (ue->info->var->bufinfo->bufstate == BB_NOTNULLTERMINATED);
+}
+
+# ifdef DEBUGSPLINT
 
 /*
-requires: p_e is defined, is a ptr/array variable 
-modifies: p_e
-effects: sets the length of the buffer
+** For debugging only
 */
 
- void uentry_setLen (uentry p_e, int len)  {
-  if( uentry_isValid(p_e) ) {
-    if( p_e->info != NULL) {
-      if( p_e->info->var != NULL) {
-        p_e->info->var->bufinfo->len = len;
-        p_e->sref->bufinfo.len = len;
-        return;
-      }//End if
-    }//End if
-  }//End if
-
-  fprintf(stderr, "uentry:Error in setLen\n");
+void uentry_checkValid (uentry ue)
+{
+  if (uentry_isValid (ue))
+    {
+      sRef_checkCompletelyReasonable (ue->sref);
+    }
 }
-/*@end@*/
-/*@=type*/
+
+# endif
This page took 0.199096 seconds and 4 git commands to generate.