Fixed problem with resetting null state after error for constants.

Added anytype constant to support /*@alt anytype@*/ properly.

diff --git a/configure b/configure
index f230cb57ace7cceb4f9787041bc32045af7cd94d..53d362d0fb82e219114825fcc375fef4954d4de5 100755 (executable)
--- a/configure
+++ b/configure
@@ -3249,7 +3249,7 @@ s/^[^=]*=[        ]*$//;
 }'
 fi
 
-DEFS=-DHAVE_CONFIG_H
+DEFS=-DHAVE_CONFIG_H 
 
 : ${CONFIG_STATUS=./config.status}
 ac_clean_files_save=$ac_clean_files

diff --git a/src/Headers/lctype.h b/src/Headers/lctype.h
index 135d9eaa8bab43ee2a8fa84a675d2c7c509a3adc..a58ebaa1c62815f99403f4122bc8ab7f6ccd0a18 100644 (file)
--- a/src/Headers/lctype.h
+++ b/src/Headers/lctype.h
@@ -73,6 +73,7 @@ typedef enum
        
 typedef enum 
 { 
+  CTK_ANYTYPE = -4,
   CTK_UNKNOWN = -3,
   CTK_INVALID = -2, 
   CTK_DNE = -1,
@@ -97,6 +98,9 @@ extern int ctkind_toInt (ctkind p_x);
 /*@constant ctype ctype_dne; @*/
 # define ctype_dne        ((ctype) CTK_DNE)
 
+/*@constant ctype ctype_anytype; @*/
+# define ctype_anytype    ((ctype) CTK_ANYTYPE)
+
 /*@constant ctype ctype_unknown; @*/
 # define ctype_unknown    CTX_UNKNOWN
 
@@ -343,6 +347,9 @@ extern bool ctype_isUndefined (ctype p_c) /*@*/ ;
 extern bool ctype_isUnknown (ctype p_c) /*@*/;
 # define ctype_isUnknown(c)       ((c) == CTX_UNKNOWN)
 
+extern bool ctype_isAnytype (ctype p_c) /*@*/;
+# define ctype_isAnytype(c)       ((c) == ctype_anytype)
+
 extern bool ctype_isBogus (/*@sef@*/ ctype p_c) /*@*/ ;
 # define ctype_isBogus(c)         (ctype_isUndefined(c) || ctype_isUnknown(c))
 

diff --git a/src/Headers/llerror.h b/src/Headers/llerror.h
index e54c01d6a79ed70ca1d52144d8962c3e02f2f47b..cf212956bc7d25bdd81bed9805d114d075a94f10 100644 (file)
--- a/src/Headers/llerror.h
+++ b/src/Headers/llerror.h
@@ -32,7 +32,10 @@ extern /*@noreturnwhenfalse@*/ void llassertretnull (/*@sef@*/ bool p_test);
           llbuglit ("llassert failed: " #tst); \
        }} while (FALSE)
 
-extern /*@noreturnwhenfalse@*/ void llassertretval (/*@sef@*/ bool p_test, /*@sef@*/ void *p_val);
+typedef void *tx_voidptr;
+
+extern /*@noreturnwhenfalse@*/ void 
+llassertretval (/*@sef@*/ bool p_test, /*@sef@*/ /*@null@*/ tx_voidptr /*@alt anytype@*/ p_val); 
 # define llassertretval(tst,val) \
     do { if (!(tst)) { \
            if (context_getFlag (FLG_TRYTORECOVER)) checkParseError (); \

diff --git a/src/Headers/sRef.h b/src/Headers/sRef.h
index d21416b96d093f2041627defbb4c59b0f81b8836..25eee4d97c897d10262f3c50da8a8696003d0d26 100644 (file)
--- a/src/Headers/sRef.h
+++ b/src/Headers/sRef.h
@@ -702,7 +702,7 @@ sRef_aliasSetCompleteAlkParam (void (p_predf) (sRef, alkind, fileloc), sRef p_s,
      /*@modifies p_s@*/ ;
 
 # ifdef DEBUGSPLINT
-extern void sRef_checkCompletelyReasonable (sRef p_s) /*@*/ ;
+extern void sRef_checkCompletelyReasonable (sRef p_s) /*@modifies g_errorstream@*/ ;
 # endif
 
 # else

diff --git a/src/aliasTable.c b/src/aliasTable.c
index 8a94f2dccfb34c8cfea7acc2656c4d9cc5312939..3246c697593e1d4ee7da49f0a9eaa8fea97a6034 100644 (file)
--- a/src/aliasTable.c
+++ b/src/aliasTable.c
@@ -834,11 +834,11 @@ void aliasTable_checkValid (aliasTable t)
 {
   aliasTable_elements (t, key, value)
     {
-      (void) sRef_isCompletelyReasonable (key);
+      sRef_checkCompletelyReasonable (key);
 
       sRefSet_elements (value, sr) 
        {
-         (void) sRef_isCompletelyReasonable (sr);
+         sRef_checkCompletelyReasonable (sr);
        } end_sRefSet_elements ;
     } end_aliasTable_elements ;
 }

diff --git a/src/cgrammar.c.der b/src/cgrammar.c.der
index a8917c31d1927fc29d28943f5f94b969fce01dc1..45de7c5223749ee5097082056612b732b4fd305e 100644 (file)
--- a/src/cgrammar.c.der
+++ b/src/cgrammar.c.der
@@ -4367,7 +4367,7 @@ case 367:
 { yyval.typequal = yyvsp[-1].typequal; ;
     break;}
 case 374:
-{ yyval.ctyp = ctype_unknown; ;
+{ yyval.ctyp = ctype_anytype; ;
     break;}
 case 375:
 { yyval.ctyp = ctype_anyintegral; ;

diff --git a/src/cgrammar.y b/src/cgrammar.y
index 5c4f2d8cebf4a6bb51313191a87637f1b7291de7..ae113f38eaac0b3dbd1db6a19d7540da20e8d34a 100644 (file)
--- a/src/cgrammar.y
+++ b/src/cgrammar.y
@@ -1231,14 +1231,14 @@ typeSpecifier
  | CGFLOAT NotType
  | CDOUBLE NotType
  | CVOID NotType 
- | QANYTYPE NotType              { $$ = ctype_unknown; }
+ | QANYTYPE NotType              { $$ = ctype_anytype; }
  | QINTEGRALTYPE NotType         { $$ = ctype_anyintegral; }
  | QUNSIGNEDINTEGRALTYPE NotType { $$ = ctype_unsignedintegral; }
  | QSIGNEDINTEGRALTYPE NotType   { $$ = ctype_signedintegral; }
  | typeName NotType     
  | suSpc NotType 
  | enumSpc NotType
- | typeModifier NotType { $$ = ctype_fromQual ($1); }
+ | typeModifier NotType           { $$ = ctype_fromQual ($1); }
 
 completeType
  : IsType completeTypeSpecifier IsType

diff --git a/src/constraintList.c b/src/constraintList.c
index 2ae629e5c326a991bbe5b8ecc5d3aa92408177d9..fe65c3c9ea05650b5bd70d3bb181359f081ec15b 100644 (file)
--- a/src/constraintList.c
+++ b/src/constraintList.c
@@ -64,7 +64,7 @@
   s->nspace = constraintListBASESIZE;
   s->elements = (constraint *)
     dmalloc (sizeof (*s->elements) * constraintListBASESIZE);
-
+  
   return (s);
 }
 

diff --git a/src/context.c b/src/context.c
index 07de91c98f02c5981eb52bc2a3b45bcb4ddb7007..cae02cfc677a21731bd1ac6b3b9585292018a8fd 100644 (file)
--- a/src/context.c
+++ b/src/context.c
@@ -1106,6 +1106,7 @@ context_setModeAux (cstring s, bool warn)
          FLG_SHIFTIMPLEMENTATION,
          FLG_BUFFEROVERFLOWHIGH,
          FLG_BUFFEROVERFLOW,
+         FLG_LITERALOVERSIZE,
          INVALID_FLAG 
        } ;
 
@@ -1134,6 +1135,7 @@ context_setModeAux (cstring s, bool warn)
          FLG_CHARINTLITERAL,
          FLG_ZEROBOOL,
          FLG_BUFFEROVERFLOWHIGH,
+         FLG_LITERALOVERSIZE,
          INVALID_FLAG 
          } ;
 
@@ -1183,6 +1185,8 @@ context_setModeAux (cstring s, bool warn)
          FLG_EVALORDER, FLG_USEDEF, 
          FLG_NESTEDEXTERN, 
 
+         FLG_LITERALOVERSIZE, FLG_LITERALUNDERSIZE,
+
          /* warn use flags */
          FLG_MULTITHREADED, FLG_PORTABILITY, FLG_SUPERUSER, FLG_IMPLEMENTATIONOPTIONAL,
          FLG_BUFFEROVERFLOWHIGH,
@@ -1307,6 +1311,8 @@ context_setModeAux (cstring s, bool warn)
 
          FLG_COMPDEF, FLG_COMPMEMPASS, FLG_UNIONDEF,
 
+         FLG_LITERALOVERSIZE, FLG_LITERALUNDERSIZE,
+
          /* memtrans flags */
          FLG_EXPOSETRANS,
          FLG_OBSERVERTRANS,

diff --git a/src/ctype.c b/src/ctype.c
index 3384cb65e4b2878801883a24a544b2afdfb86859..6a309aca62cb8c131e0b41133bd005cc4ccf0f94 100644 (file)
--- a/src/ctype.c
+++ b/src/ctype.c
@@ -1815,6 +1815,10 @@ ctype_unparse (ctype c)
     {
       return cstring_makeLiteralTemp ("?");
     }
+  else if (ctype_isAnytype (c))
+    {
+      return cstring_makeLiteralTemp ("<any>");
+    }
   else
     {
       /*@-modobserver@*/
@@ -1911,6 +1915,7 @@ ctype_getBaseType (ctype c)
 
   switch (ctentry_getKind (cte))
     {
+    case CTK_ANYTYPE:
     case CTK_UNKNOWN:
     case CTK_INVALID:
     case CTK_PLAIN:
@@ -2533,8 +2538,18 @@ ctype ctype_combine (ctype dominant, ctype modifier)
   
 ctype ctype_resolve (ctype c)
 {
-  if (ctype_isUnknown (c)) return ctype_int;
-  return c;
+  if (ctype_isUnknown (c)) 
+    {
+      return ctype_int;
+    }
+  else if (c == ctype_anytype)
+    {
+      return ctype_unknown;
+    }
+  else
+    {
+      return c;
+    }
 }
 
 ctype ctype_fromQual (qual q)

diff --git a/src/exprData.c b/src/exprData.c
index 2c18d5fca93c63a2f09d40ee236025687ba859bd..13e2fc8a43530bc873da60840d049a30dbd49a66 100644 (file)
--- a/src/exprData.c
+++ b/src/exprData.c
@@ -295,32 +295,31 @@ void exprData_free (/*@only@*/ exprData data, exprKind kind)
 
 /*@exposed@*/ exprNode exprData_getOpB (exprData data) /*@*/
 {
-  llassert (data != exprData_undefined);
+  llassertretval (data != exprData_undefined, exprNode_undefined);
   return (data->op->b);
 }
 
 /*@observer@*/ lltok exprData_getOpTok (exprData data) /*@*/
 {
-  llassert (data != exprData_undefined);
+  llassertretval (data != exprData_undefined, exprNode_undefined);
   return (data->op->op);
 }
 
 /*@exposed@*/ exprNode exprData_getPairA (exprData data) /*@*/
 {
-  llassert (data != exprData_undefined);
+  llassertretval (data != exprData_undefined, exprNode_undefined);
   return (data->pair->a);
 }
 
 /*@exposed@*/ exprNode exprData_getPairB (exprData data) /*@*/
 {
-  llassert (data != exprData_undefined);
+  llassertretval (data != exprData_undefined, exprNode_undefined);
   return (data->pair->b);
 }
 
-
 /*@exposed@*/ uentry exprData_getIterSname (exprData data) /*@*/
 {
-  llassert (data != exprData_undefined);
+  llassertretval (data != exprData_undefined, uentry_undefined);
   return (data->iter->sname);
 }
 
@@ -332,19 +331,19 @@ void exprData_free (/*@only@*/ exprData data, exprKind kind)
 
 /*@exposed@*/ exprNode exprData_getIterBody (exprData data) /*@*/
 {
-  llassert (data != exprData_undefined);
+  llassertretval (data != exprData_undefined, exprNode_undefined);
   return (data->iter->body);
 }
 
 /*@exposed@*/ uentry exprData_getIterEname (exprData data) /*@*/
 {
-  llassert (data != exprData_undefined);
+  llassertretval (data != exprData_undefined, uentry_undefined);
   return (data->iter->ename);
 }
 
 /*@exposed@*/ exprNode exprData_getFcn (exprData data) /*@*/
 {
-  llassert (data != exprData_undefined);
+  llassertretval (data != exprData_undefined, exprNode_undefined);
   return (data->call->fcn);
 }
 

diff --git a/src/exprNode.c b/src/exprNode.c
index ffdb4c0c4c4b802887cf8d2c58ff83f8c3b1dab4..dc2104f6bd94bf04117cf78d49e849ca7eaf895e 100644 (file)
--- a/src/exprNode.c
+++ b/src/exprNode.c
@@ -82,8 +82,7 @@ static /*@observer@*/ cstring exprNode_rootVarName (exprNode p_e);
 static /*@exposed@*/ exprNode 
   exprNode_lastStatement (/*@returned@*/ exprNode p_e);
 
-static /*@null@*/ sRef defref = sRef_undefined;
-static /*@only@*/ exprNode mustExitNode = exprNode_undefined;
+static /*@only@*/ exprNode s_mustExitNode = exprNode_undefined;
 
 static int checkArgsReal (uentry p_fcn, /*@dependent@*/ exprNode p_f, 
                          uentryList p_cl, 
@@ -138,8 +137,6 @@ void exprNode_initMod (void)
   ctypeType = ctype_unknown;
   filelocType = ctype_unknown;
 
-  defref = sRef_undefined;
-  
   if (usymtab_existsType (cstring_makeLiteralTemp ("cstring")))
     {
       cstringType = usymtab_lookupAbstractType (cstring_makeLiteralTemp ("cstring"));
@@ -217,7 +214,7 @@ void exprNode_initMod (void)
 void
 exprNode_destroyMod (void) 
    /*@globals killed regArg, killed outArg, killed outStringArg,
-             killed mustExitNode, initMod @*/
+             killed s_mustExitNode, initMod @*/
 {
   if (initMod)
     {
@@ -225,7 +222,7 @@ exprNode_destroyMod (void)
       uentry_free (outArg);
       uentry_free (outStringArg);
       
-      exprNode_free (mustExitNode);
+      exprNode_free (s_mustExitNode);
       initMod = FALSE;
     /*@-branchstate@*/ 
     } 
@@ -234,7 +231,7 @@ exprNode_destroyMod (void)
 
 static void exprNode_resetSref (/*@notnull@*/ exprNode e)
 {
-  e->sref = defref;
+  e->sref = sRef_undefined;
 }
 
 exprNode exprNode_fakeCopy (exprNode e)
@@ -439,7 +436,7 @@ static /*@notnull@*/ /*@special@*/ exprNode
   e->typ = c;
   e->kind = XPR_EMPTY;
   e->val = multiVal_undefined;
-  e->sref = defref;
+  e->sref = sRef_undefined;
   e->etext = cstring_undefined;
   e->loc = fileloc_undefined;
   e->guards = guardSet_undefined;
@@ -459,13 +456,13 @@ static /*@notnull@*/ /*@special@*/ exprNode
 
 /*@observer@*/ exprNode exprNode_makeMustExit (void)
 {
-  if (exprNode_isUndefined (mustExitNode))
+  if (exprNode_isUndefined (s_mustExitNode))
     {
-      mustExitNode = exprNode_createPlain (ctype_unknown);
-      mustExitNode->exitCode = XK_MUSTEXIT;
+      s_mustExitNode = exprNode_createPlain (ctype_unknown);
+      s_mustExitNode->exitCode = XK_MUSTEXIT;
     }
 
-  return mustExitNode;
+  return s_mustExitNode;
 }
 
 
@@ -551,7 +548,7 @@ static /*@notnull@*/ /*@special@*/ exprNode
     }
 
   ret->kind = XPR_EMPTY;
-  ret->sref = defref;
+  ret->sref = sRef_undefined;
   ret->etext = cstring_undefined;
   ret->exitCode = XK_NEVERESCAPE;
   ret->canBreak = FALSE;
@@ -603,7 +600,7 @@ static /*@notnull@*/ /*@special@*/ exprNode
   
   ret->val = multiVal_undefined;
   ret->kind = XPR_EMPTY;
-  ret->sref = defref;
+  ret->sref = sRef_undefined;
   ret->etext = cstring_undefined;
   ret->exitCode = XK_NEVERESCAPE;
   ret->canBreak = FALSE;
@@ -640,7 +637,7 @@ static /*@notnull@*/ /*@special@*/ exprNode
       ret->msets = sRefSet_undefined;
 
       ret->kind = XPR_EMPTY;
-      ret->sref = defref;
+      ret->sref = sRef_undefined;
       ret->etext = cstring_undefined;
       ret->exitCode = XK_NEVERESCAPE;
       ret->canBreak = FALSE;
@@ -885,7 +882,7 @@ exprNode exprNode_fromUIO (cstring c)
     }
 
   e->loc = loc; /* save loc was mangled */
-  e->sref = defref;
+  e->sref = sRef_undefined;
 
   if (usymtab_exists (c))
     {
@@ -1020,8 +1017,7 @@ exprNode exprNode_createId (/*@observer@*/ uentry c)
       e->canBreak = FALSE;
       e->mustBreak = FALSE;
       
-      exprNode_defineConstraints(e);
-
+      exprNode_defineConstraints (e);
       return e;
     }
   else
@@ -2049,7 +2045,7 @@ checkScanfArgs (/*@notnull@*/ /*@dependent@*/ exprNode f, uentry fcn,
                        }
                      else
                        {
-                                                 /* a->sref = defref; */
+                                                 /* a->sref = sRef_undefined; */
                        }
                    }
                }
@@ -3891,7 +3887,7 @@ functionCallSafe (/*@only@*/ /*@notnull@*/ exprNode f,
     }
   else
     {
-      ret->sref = defref;
+      ret->sref = sRef_undefined;
       exprNode_checkSetAny (ret, uentry_rawName (le));
     }
 
@@ -4992,28 +4988,15 @@ exprNode_cast (/*@only@*/ lltok tok, /*@only@*/ exprNode e, /*@only@*/ qtype q)
   ret->kind = XPR_CAST;
   ret->edata = exprData_makeCast (tok, e, q);
 
-  if (ctype_isRealSU (ctype_getBaseType (sRef_getType (e->sref))))
+  ret->sref = sRef_copy (e->sref);
+  
+  if (!sRef_isConst (e->sref))
     {
-      /* 
-      ** This is a bit of a hack to avoid a problem
-      ** when the code does,
-      **          (some other struct) x
-      **          ...
-      **          x->field
-      */
-
-      ret->sref = sRef_copy (e->sref);
       usymtab_addForceMustAlias (ret->sref, e->sref);
-      sRef_setTypeFull (ret->sref, c);
-      DPRINTF (("Cast: %s -> %s", sRef_unparseFull (e->sref),
-               sRef_unparseFull (ret->sref)));
-    }
-  else
-    {
-      ret->sref = e->sref;
-      sRef_setTypeFull (ret->sref, c);
-      DPRINTF (("Cast 2: -> %s", sRef_unparseFull (ret->sref)));
     }
+  
+  sRef_setTypeFull (ret->sref, c);
+  DPRINTF (("Cast 2: -> %s", sRef_unparseFull (ret->sref)));
 
   /*
   ** we allow
@@ -8505,7 +8488,6 @@ exprNode_makeInitializationAux (/*@temp@*/ idDecl t)
 
   exprData_free (ret->edata, ret->kind); 
   ret->edata = exprData_undefined;
-
   ret->exitCode = XK_NEVERESCAPE;
   ret->mustBreak = FALSE;
   ret->kind = XPR_INIT;
@@ -8526,14 +8508,15 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t,
   uentry ue = usymtab_lookup (idDecl_observeId (t));
   exprNode ret = exprNode_makeInitializationAux (t);
   fileloc loc = exprNode_loc (e);
-  
+
+  DPRINTF (("initialization: %s = %s", idDecl_unparse (t), exprNode_unparse (e)));
+
   if (exprNode_isError (e)) 
     {
       e = exprNode_createUnknown ();
-      idDecl_free (t);
-
       /* error: assume initializer is defined */
       sRef_setDefined (ret->sref, g_currentloc); 
+      ret->edata = exprData_makeInit (t, e);
     }
   else
     {
@@ -8549,6 +8532,7 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t,
 
       exprData_free (ret->edata, ret->kind);
       ret->edata = exprData_makeInit (t, e);
+      DPRINTF (("ret: %s", exprNode_unparse (ret)));
 
       exprNode_checkUse (ret, e->sref, e->loc);
       
@@ -8600,15 +8584,80 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t,
        {
          sRef_setDefState (ret->sref, SS_PARTIAL, fileloc_undefined);
        }
+# if 0
+      if (exprNode_isStringLiteral (e)
+         && (ctype_isArray (ct))
+         && (ctype_isChar (ctype_realType (ctype_baseArrayPtr (ct)))))
+       {
+         /*
+         ** If t is a char [], the literal is copied.
+         */
+
+         cstring slit;
 
-      doAssign (ret, e, TRUE);
+         if (multiVal_isDefined (e->val))
+           {
+             slit = multiVal_forceString (e->val);
+           }
+         else
+           {
+             slit = cstring_undefined;
+           }
+
+         sRef_setDefState (ret->sref, SS_DEFINED, e->loc);
+         ret->val = multiVal_copy (e->val);
+
+         if (cstring_isDefined (slit))
+           {
+             if (ctype_isFixedArray (ct))
+               {
+                 long int alength = ctype_getArraySize (ct);
+                 
+                 if (alength < cstring_length (slit) + 1)
+                   {
+                     voptgenerror
+                       (FLG_LITERALOVERSIZE,
+                        ("Array initialized to string literal bigger than allocated size (literal is %d chars long (plus one for nul terminator), array size is %d): %s", 
+                         cstring_length (slit),
+                         alength,
+                         exprNode_unparse (e)),
+                        e->loc);
+                   }
+                 else if (alength > cstring_length (slit))
+                   {
+                     voptgenerror
+                       (FLG_LITERALUNDERSIZE,
+                        ("Array initialized to string literal smaller than allocated size (literal is %d chars long (plus one for nul terminator), array size is %d), could waste storage: %s", 
+                         cstring_length (slit),
+                         alength,
+                         exprNode_unparse (e)),
+                        e->loc);
+                   }
+                 else
+                   {
+                     ;
+                   }
+               }
+             else
+               {                 
+                 sRef_setNullTerminatedState (ret->sref);
+                 sRef_setSize (ret->sref, cstring_length (slit) + 1);
+                 sRef_setLen (ret->sref, cstring_length (slit) + 1);
+               }
+           }
+       }
+      else
+# endif
+       {
+         doAssign (ret, e, TRUE);
+       }
 
       if (uentry_isStatic (ue))
        {
          sRef_setDefState (ret->sref, SS_DEFINED, fileloc_undefined);
        }
     }
-
+  
   if (context_inIterDef ())
     {
       /* should check if it is yield */
@@ -8620,6 +8669,15 @@ exprNode exprNode_makeInitialization (/*@only@*/ idDecl t,
     }
 
   exprNode_mergeUSs (ret, e);
+  DPRINTF (("Ret: %s %p %p",
+           exprNode_unparse (ret),
+           ret->requiresConstraints,
+           ret->ensuresConstraints));
+
+  DPRINTF (("Ret: %s %s %s",
+           exprNode_unparse (ret),
+           constraintList_unparse (ret->requiresConstraints),
+           constraintList_unparse (ret->ensuresConstraints)));
   return ret;
 }
   
@@ -8703,7 +8761,7 @@ exprNode_iterNewId (/*@only@*/ cstring s)
   e->kind = XPR_VAR;
   e->val = multiVal_unknown ();
   e->guards = guardSet_new ();
-  e->sref = defref;
+  e->sref = sRef_undefined;
   e->isJumpPoint = FALSE;
   e->exitCode = XK_NEVERESCAPE;
 
@@ -8894,8 +8952,7 @@ exprNode exprNode_iterStart (/*@observer@*/ uentry name, /*@only@*/ exprNodeList
 {
   if (exprNode_isDefined (e))
     {
-      /*@access sRef@*/
-      if (e->sref == defref) /*@noaccess sRef@*/
+      if (sRef_isInvalid (e->sref))
        {
          /*@-mods@*/
          e->sref = sRef_makeUnknown (); 

diff --git a/src/flags.def b/src/flags.def
index 1bba23bc5cacc762046b5d39124fc5e7084d6136..c52720b9bf4922d42d502bd9f292879b072f0088 100644 (file)
--- a/src/flags.def
+++ b/src/flags.def
@@ -1845,7 +1845,6 @@ static flaglist flags =
     "A possibly non-nullterminated string/memory is used/referenced as a nullterminated one.",
     0, 0
   },
-
   {
     FK_BOUNDS, FK_MEMORY, specialFlag,
     "bounds",
@@ -1853,6 +1852,22 @@ static flaglist flags =
     "memory bounds checking (sets boundsread and boundswrite)",
     "Memory read or write may be out of bounds of allocated storage.", 0, 0
   },
+  {
+    FK_BOUNDS, FK_MEMORY, modeFlag,
+    "literaloversize",
+    FLG_LITERALOVERSIZE,
+    "string literal is too large for allocated array",
+    "String literal is too large for allocated array.", 0, 0
+  },
+  {
+    FK_BOUNDS, FK_MEMORY, modeFlag,
+    "literalundersize",
+    FLG_LITERALUNDERSIZE,
+    "string literal is smaller than allocated array (space may be wasted)",
+    "More storage is allocated for a string literal than the length of the literal. "
+    "If the array is not set later, this is a waste of storage.",
+    0, 0
+  },
   {
     FK_BOUNDS, FK_MEMORY, plainFlag,
     "boundsread",

diff --git a/src/osd.c b/src/osd.c
index 16f020dd881cfc357d98e0d551c4358185badea9..9af9d100282934657127474b9e1e402408e2e3fb 100644 (file)
--- a/src/osd.c
+++ b/src/osd.c
@@ -1041,7 +1041,7 @@ cstring osd_outputPath (cstring filename)
   int unmatched_slash_count = 0;
   size_t filename_len = cstring_length (filename);
   
-  llassertretval (filename_len > 0, /*@-type@*/ filename /*@=type@*/);
+  llassertretval (filename_len > 0, filename);
 
   /*@access cstring@*/
   path_p = filename;

diff --git a/src/qtype.c b/src/qtype.c
index 6c28397b26b5915d59f84816c7ce6c1e757cd572..5a4a20be653099fe592668388dfee3bd5e032656 100644 (file)
--- a/src/qtype.c
+++ b/src/qtype.c
@@ -122,6 +122,8 @@ qtype qtype_mergeImplicitAlt (/*@returned@*/ qtype q1, /*@only@*/ qtype q2)
 
 qtype qtype_mergeAlt (/*@returned@*/ qtype q1, /*@only@*/ qtype q2)
 {
+  DPRINTF (("Merge alt: %s + %s", qtype_unparse (q1), qtype_unparse (q2)));
+
   if (qtype_isDefined (q1) && qtype_isDefined (q2))
     {
       if (context_getFlag (FLG_IMPCONJ))
@@ -132,7 +134,6 @@ qtype qtype_mergeAlt (/*@returned@*/ qtype q1, /*@only@*/ qtype q2)
        {
          q1->type = ctype_makeExplicitConj (q1->type, q2->type);
        }
-
       
       if (!qualList_isEmpty (q2->quals))
        {

diff --git a/src/sRef.c b/src/sRef.c
index 9a4b5d327e75cca177799c0a11131debcc12e8da..030e5c223e1e6ba85d7f824632dba86899c863e9 100644 (file)
--- a/src/sRef.c
+++ b/src/sRef.c
@@ -163,7 +163,6 @@ static /*@nullwhentrue@*/ bool sRef_isUnreasonable (sRef s) /*@*/
 
 static void sRef_checkMutable (/*@unused@*/ sRef s)
 {
-  /*@i235@*/
   if (sRef_isReasonable (s) && s->immut)
     {
       llcontbug (message ("Modification to sRef marked immutable: %q", 
@@ -5602,34 +5601,35 @@ void sRef_setNullUnknown (sRef s, fileloc loc)
 
 void sRef_setNullError (sRef s)
 {
-  if (sRef_isReasonable (s))
+  if (sRef_isReasonable (s) && !sRef_isConst (s))
     {
       sRef_setNullStateAux (s, NS_UNKNOWN, fileloc_undefined);
     }
 }
 
-void sRef_setNullErrorLoc (sRef s, /*@unused@*/ fileloc loc)
+void sRef_setNullErrorLoc (sRef s, fileloc loc)
 {
-  sRef_setNullError (s);
+  if (sRef_isReasonable (s) && !sRef_isConst (s))
+    {
+      sRef_setNullStateAux (s, NS_UNKNOWN, loc);
+    }
 }
 
 void sRef_setOnly (sRef s, fileloc loc)
 {
-  sRef_checkMutable (s);
-
   if (sRef_isReasonable (s) && s->aliaskind != AK_ONLY)
     {
+      sRef_checkMutable (s);
       s->aliaskind = AK_ONLY;
       s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
-          }
+    }
 }
 
 void sRef_setDependent (sRef s, fileloc loc)
 {
-  sRef_checkMutable (s);
-
   if (sRef_isReasonable (s) && !sRef_isConst (s) && (s->aliaskind != AK_DEPENDENT))
     {
+      sRef_checkMutable (s);
       DPRINTF (("Setting dependent: %s", sRef_unparseFull (s)));
       s->aliaskind = AK_DEPENDENT;
       s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
@@ -5638,10 +5638,9 @@ void sRef_setDependent (sRef s, fileloc loc)
 
 void sRef_setOwned (sRef s, fileloc loc)
 {
-  sRef_checkMutable (s);
-
   if (sRef_isReasonable (s) && !sRef_isConst (s) && (s->aliaskind != AK_OWNED))
     {
+      sRef_checkMutable (s);
       s->aliaskind = AK_OWNED;
       s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
     }
@@ -5649,16 +5648,15 @@ void sRef_setOwned (sRef s, fileloc loc)
 
 void sRef_setKept (sRef s, fileloc loc)
 {
-  sRef_checkMutable (s);
-
   if (sRef_isReasonable (s) && !sRef_isConst (s) && (s->aliaskind != AK_KEPT))
     {
       sRef base = sRef_getBaseSafe (s);  
-      
+ 
       while (sRef_isReasonable (base) && sRef_isKnown (base))
        {
          if (base->defstate == SS_DEFINED) 
            {
+             sRef_checkMutable (base);
              base->defstate = SS_PDEFINED; 
              base = sRef_getBaseSafe (base); 
            }
@@ -5668,6 +5666,7 @@ void sRef_setKept (sRef s, fileloc loc)
            }
        }
 
+      sRef_checkMutable (s);
       s->aliaskind = AK_KEPT;
       s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
     }
@@ -5701,10 +5700,9 @@ void sRef_setDependentComplete (sRef s, fileloc loc)
 
 void sRef_setFresh (sRef s, fileloc loc)
 {
-  sRef_checkMutable (s);
-
-  if (sRef_isReasonable (s))
+  if (sRef_isReasonable (s) && !sRef_isConst (s))
     {
+      sRef_checkMutable (s);
       s->aliaskind = AK_FRESH;
       s->aliasinfo = stateInfo_updateLoc (s->aliasinfo, loc);
     }
@@ -5713,16 +5711,17 @@ void sRef_setFresh (sRef s, fileloc loc)
 void sRef_kill (sRef s, fileloc loc)
 {
   DPRINTF (("Kill: %s", sRef_unparseFull (s)));
-  sRef_checkMutable (s);
 
   if (sRef_isReasonable (s) && !sRef_isShared (s) && !sRef_isConst (s))
     {
       sRef base = sRef_getBaseSafe (s);  
-      
+      sRef_checkMutable (s);
+       
       while (sRef_isReasonable (base) && sRef_isKnown (base))
        {
          if (base->defstate == SS_DEFINED) 
            {
+             sRef_checkMutable (base);
              base->defstate = SS_PDEFINED; 
              base = sRef_getBaseSafe (base); 
            }
@@ -5742,17 +5741,16 @@ void sRef_kill (sRef s, fileloc loc)
 
 void sRef_maybeKill (sRef s, fileloc loc)
 {
-  sRef_checkMutable (s);
-
   if (sRef_isReasonable (s))
     {
       sRef base = sRef_getBaseSafe (s);  
-
+      sRef_checkMutable (s);
             
       while (sRef_isReasonable (base) && sRef_isKnown (base))
        {
          if (base->defstate == SS_DEFINED || base->defstate == SS_RELDEF)
            {
+             sRef_checkMutable (base);
              base->defstate = SS_PDEFINED; 
              base = sRef_getBaseSafe (base); 
            }
@@ -6104,20 +6102,18 @@ void sRef_free (/*@only@*/ sRef s)
 
 void sRef_setType (sRef s, ctype t)
 {
-  sRef_checkMutable (s);
-
   if (sRef_isReasonable (s))
     {
+      sRef_checkMutable (s); 
       s->type = t;
     }
 }
 
 void sRef_setTypeFull (sRef s, ctype t)
 {
-  sRef_checkMutable (s);
-
   if (sRef_isReasonable (s))
     {
+      sRef_checkMutable (s);
       s->type = t;
 
       sRefSet_allElements (s->deriv, current)
@@ -10063,28 +10059,37 @@ void sRef_setNotNullTerminatedState(sRef p_s) {
 }
 
 void sRef_setLen(sRef p_s, int len) {
-   if( sRef_isReasonable (p_s) && sRef_isNullTerminated(p_s)) {
-      p_s->bufinfo.len = len;
-   } else {
-      llfatalbug( message("sRef_setLen passed a invalid sRef\n"));
-   }
+   if (sRef_isReasonable (p_s) && sRef_isNullTerminated(p_s)) 
+     {
+       p_s->bufinfo.len = len;
+     } 
+   else 
+     {
+       llfatalbug( message("sRef_setLen passed an invalid sRef\n"));
+     }
 }
     
 
 void sRef_setSize(sRef p_s, int size) {
-   if( sRef_isValid(p_s)) {
+   if( sRef_isValid(p_s)) 
+     {
        p_s->bufinfo.size = size;
-   } else {
-      llfatalbug( message("sRef_setSize passed a invalid sRef\n"));
-   }
+     } 
+   else
+     {
+       llfatalbug( message("sRef_setSize passed a invalid sRef\n"));
+     }
 }
 
 void sRef_resetLen(sRef p_s) {
-       if (sRef_isReasonable (p_s)) {
-               p_s->bufinfo.len = 0;
-       } else {
-               llfatalbug (message ("sRef_setLen passed an invalid sRef\n"));
-       }
+  if (sRef_isReasonable (p_s)) 
+    {
+      p_s->bufinfo.len = 0;
+    }
+  else
+    {
+      llfatalbug (message ("sRef_setLen passed an invalid sRef\n"));
+    }
 }
 
 /*drl7x 11/28/2000 */

diff --git a/src/uentry.c b/src/uentry.c
index 10ba8d080ca6923c360238923c5278a9f37d1917..787341666e4aff0fa785adf0cd6dd22885c0c494 100644 (file)
--- a/src/uentry.c
+++ b/src/uentry.c
@@ -3152,17 +3152,20 @@ uentry uentry_makeConstantAux (cstring n, ctype t,
 
 /*@notnull@*/ uentry uentry_makeConstant (cstring n, ctype t, fileloc f)
 {
-  return (uentry_makeConstantAux (n, t, f, FALSE, 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)
 {
-  return (uentry_makeConstantAux (n, t, f, priv, FALSE, val));
+  uentry ue = uentry_makeConstantAux (n, t, f, priv, FALSE, val);
+  return ue;
 }
 
 /*@notnull@*/ uentry uentry_makeMacroConstant (cstring n, ctype t, fileloc f)
 {
-  return (uentry_makeConstantAux (n, t, f, FALSE, TRUE, multiVal_unknown ()));
+  uentry ue = uentry_makeConstantAux (n, t, f, FALSE, TRUE, multiVal_unknown ());
+  return ue;
 }
 
 /*@notnull@*/ uentry uentry_makeIdConstant (idDecl t)
@@ -5373,8 +5376,9 @@ uentry_unparseFull (uentry v)
        }
       else if (uentry_isConstant (v))
        {
-         res = message ("%q = %q",
-                        res, multiVal_unparse (uentry_getConstantValue (v)));
+         res = message ("%q = %q / %q",
+                        res, multiVal_unparse (uentry_getConstantValue (v)),
+                        sRef_unparseFull (v->sref));
        }
       else
        {
@@ -11426,7 +11430,7 @@ void uentry_checkValid (uentry ue)
 {
   if (uentry_isValid (ue))
     {
-      (void) sRef_isCompletelyReasonable (ue->sref);
+      sRef_checkCompletelyReasonable (ue->sref);
     }
 }
 

diff --git a/src/usymtab.c b/src/usymtab.c
index 179723c65f9d324a66d8750c3a5a945a2f1b2963..14f0a9457145f517ba2e040cdeae82ac9cb00e86 100644 (file)
--- a/src/usymtab.c
+++ b/src/usymtab.c
@@ -5907,7 +5907,7 @@ usymtab_printComplete ()
          for (i = looplow; i < s->nentries; i++)
            {
              printf ("%s%3d %s\n", ind, i, 
-                     cstring_toCharsSafe (uentry_unparse (s->entries[i])));
+                     cstring_toCharsSafe (uentry_unparseFull (s->entries[i])));
            }
        }
       else
@@ -5916,7 +5916,7 @@ usymtab_printComplete ()
          for (i = 0; i < s->nentries; i++)
            {
              printf ("%s%3d %s\n", ind, i, 
-                    cstring_toCharsSafe (uentry_unparse (s->entries[i])));
+                    cstring_toCharsSafe (uentry_unparseFull (s->entries[i])));
            }
        }