Changed checking of complete descruction so +strictdestroy is no

[splint.git] / src / sRef.c

diff --git a/src/sRef.c b/src/sRef.c
index f0a6818e28309d146069dd7938b24667401bebf4..83f370530166341bb33fba79a5aca1db5048a285 100644 (file)
--- a/src/sRef.c
+++ b/src/sRef.c
@@ -1,6 +1,6 @@
 /*
-** LCLint - annotation-assisted static program checker
-** Copyright (C) 1994-2001 University of Virginia,
+** Splint - annotation-assisted static program checker
+** Copyright (C) 1994-2002 University of Virginia,
 **         Massachusetts Institute of Technology
 **
 ** This program is free software; you can redistribute it and/or modify it
@@ -19,7 +19,7 @@
 **
 ** 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 more information: http://www.splint.org
 */
 /*
 ** storeRef.c
@@ -80,6 +80,18 @@ static bool sRef_isDeepUnionField (sRef p_s);
 static void sRef_addDeriv (/*@notnull@*/ sRef p_s, /*@notnull@*/ /*@exposed@*/ sRef p_t);
 static bool sRef_checkModify (sRef p_s, sRefSet p_sl) /*@*/ ;
 
+/*
+** If s is definitely null, it has no memory state.
+*/
+
+static void sRef_resetAliasKind (/*@notnull@*/ sRef s) /*@modifies s->aliaskind@*/
+{
+  if (s->nullstate == NS_DEFNULL)
+    {
+      /* s->aliaskind = AK_ERROR; */
+    }
+}
+
 static void sRef_checkMutable (/*@unused@*/ sRef s)
 {
   /*@i235@*/
@@ -3384,7 +3396,7 @@ sRef_getRootBaseAux (sRef s, int depth)
                ("Warning: reference base limit exceeded for %q. "
                 "This either means there is a variable with at least "
                 "%d indirections from this reference, or "
-                "there is a bug in LCLint.",
+                "there is a bug in Splint.",
                 sRef_unparse (s),
                 MAXBASEDEPTH),
                g_currentloc);
@@ -3714,6 +3726,10 @@ sRef_mergeStateAux (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other,
   llassertfatal (sRef_isValid (res));
   llassertfatal (sRef_isValid (other));
   
+  DPRINTF (("Merge aux: %s / %s",
+           bool_unparse (sRef_isDefinitelyNull (res)),
+           bool_unparse (sRef_isDefinitelyNull (other))));
+
   sRef_checkMutable (res);
   sRef_checkMutable (other);
 
@@ -4581,10 +4597,17 @@ bool sRef_hasNoStorage (sRef s)
 
 bool sRef_isStrictReadable (sRef s)
 {
-  return (ynm_toBoolStrict (sRef_isReadable (s)));
+  return (ynm_toBoolStrict (sRef_isValidLvalue (s)));
 }
 
-ynm sRef_isReadable (sRef s)
+/*
+** Is this what is does?
+** Returns YES if s can be used as an rvalue,
+**         MAYBE if its not clear
+**         NO if s cannot be safely used as an rvalue.
+*/
+
+ynm sRef_isValidLvalue (sRef s)
 {
   sstate ss;
 
@@ -4594,9 +4617,9 @@ ynm sRef_isReadable (sRef s)
   
   if (sRef_isConj (s) && s->defstate == SS_UNKNOWN)
     {
-      if (ynm_toBoolStrict (sRef_isReadable (sRef_getConjA (s))))
+      if (ynm_toBoolStrict (sRef_isValidLvalue (sRef_getConjA (s))))
        {
-         if (ynm_toBoolStrict (sRef_isReadable (sRef_getConjB (s))))
+         if (ynm_toBoolStrict (sRef_isValidLvalue (sRef_getConjB (s))))
            {
              return YES;
            }
@@ -4604,7 +4627,7 @@ ynm sRef_isReadable (sRef s)
        }
       else
        {
-         if (ynm_toBoolStrict (sRef_isReadable (sRef_getConjB (s))))
+         if (ynm_toBoolStrict (sRef_isValidLvalue (sRef_getConjB (s))))
            {
              return MAYBE;
            }
@@ -4628,9 +4651,9 @@ ynm sRef_isReadable (sRef s)
                            || ss == SS_FIXED 
                            || ss == SS_RELDEF 
                            || ss == SS_PDEFINED 
-                           || ss == SS_PARTIAL
+                           || ss == SS_PARTIAL 
                            || ss == SS_SPECIAL
-                           || ss == SS_ALLOCATED
+                           || ss == SS_ALLOCATED 
                            || ss == SS_KILLED /* evans 2001-05-26: added this for killed globals */
                            || ss == SS_UNKNOWN));
     }
@@ -4647,7 +4670,7 @@ static /*@exposed@*/ sRef whatUndefined (/*@exposed@*/ sRef fref, int depth)
                ("Warning: check definition limit exceeded, checking %q. "
                 "This either means there is a variable with at least "
                 "%d indirections apparent in the program text, or "
-                "there is a bug in LCLint.",
+                "there is a bug in Splint.",
                 sRef_unparse (fref),
                 MAXDEPTH),
                g_currentloc);
@@ -5150,7 +5173,29 @@ void sRef_setPartialDefinedComplete (sRef s, fileloc loc)
 
 void sRef_setDefinedComplete (sRef s, fileloc loc)
 {
+  sRef_innerAliasSetComplete (sRef_setDefined, s, loc);
+}
+
+void sRef_setDefinedCompleteDirect (sRef s, fileloc loc)
+{
+  sRefSet aliases;
+  
+  aliases = usymtab_allAliases (s);
   DPRINTF (("Set defined complete: %s", sRef_unparseFull (s)));
+  DPRINTF (("All aliases: %s", sRefSet_unparseFull (aliases)));
+  
+  sRef_setDefined (s, loc);
+
+  sRefSet_realElements (aliases, current)
+    {
+      if (sRef_isValid (current))
+       {
+         current = sRef_updateSref (current);
+         sRef_setDefined (current, loc);
+       }
+    } end_sRefSet_realElements;
+  
+  sRefSet_free (aliases);
   sRef_innerAliasSetComplete (sRef_setDefined, s, loc);
 }
 
@@ -5354,7 +5399,8 @@ void sRef_setNullStateAux (/*@notnull@*/ sRef s, nstate ns, fileloc loc)
   DPRINTF (("Set null state: %s / %s", sRef_unparse (s), nstate_unparse (ns)));
   sRef_checkMutable (s);
   s->nullstate = ns;
-  
+  sRef_resetAliasKind (s);
+
   if (fileloc_isDefined (loc))
     {
       s->nullinfo = stateInfo_updateLoc (s->nullinfo, loc);
@@ -5373,6 +5419,7 @@ void sRef_setNullStateN (sRef s, nstate n)
 {
   sRef_checkMutable (s);
   s->nullstate = n;
+  sRef_resetAliasKind (s);
 }
 
 void sRef_setNullState (sRef s, nstate n, fileloc loc)
@@ -5383,8 +5430,8 @@ void sRef_setNullState (sRef s, nstate n, fileloc loc)
     }
 }
 
-void sRef_setNullTerminatedStateInnerComplete (sRef s, struct s_bbufinfo b, /*@unused@*/ fileloc loc) {
-   
+void sRef_setNullTerminatedStateInnerComplete (sRef s, struct s_bbufinfo b, /*@unused@*/ fileloc loc) 
+{
   switch (b.bufstate) {
      case BB_NULLTERMINATED:
          sRef_setNullTerminatedState (s);
@@ -7976,7 +8023,7 @@ bool sRef_isJustAllocated (sRef s)
 static bool
 sRef_isAllocatedStorage (sRef s)
 {
-  if (sRef_isValid (s) && ynm_toBoolStrict (sRef_isReadable (s)))
+  if (sRef_isValid (s) && ynm_toBoolStrict (sRef_isValidLvalue (s)))
     {
       return (ctype_isVisiblySharable (sRef_getType (s)));
     }
@@ -8438,7 +8485,6 @@ sRef_innerAliasSetComplete (void (predf) (sRef, fileloc), sRef s, fileloc loc)
       inner = s->info->field->rec;
       aliases = usymtab_allAliases (inner);
       ct = sRef_getType (inner);
-
       
       sRefSet_realElements (aliases, current)
        {
@@ -8500,8 +8546,7 @@ sRef_innerAliasSetCompleteParam (void (predf) (sRef, sRef), sRef s, sRef t)
       inner = s->info->ref;
       aliases = usymtab_allAliases (inner);
       ct = sRef_getType (inner);
-      
-      
+            
       sRefSet_realElements (aliases, current)
        {
          if (sRef_isValid (current))
@@ -8782,6 +8827,8 @@ static void
 
   sRef_checkMutable (res);
 
+  DPRINTF (("Combine alias kinds: \n\t%s / \n\t%s",
+           sRef_unparseFull (res), sRef_unparseFull (other)));
   if (alkind_equal (ares, aother)
       || aother == AK_UNKNOWN
       || aother == AK_ERROR)
@@ -8794,12 +8841,14 @@ static void
       res ->aliaskind = AK_ERROR; 
     }
   else if (ares == AK_UNKNOWN || ares == AK_ERROR
-          || sRef_isStateUndefined (res))
+          || sRef_isStateUndefined (res)
+          || sRef_isDefinitelyNull (res))
     { 
       res->aliasinfo = stateInfo_update (res->aliasinfo, other->aliasinfo);
       res->aliaskind = aother;  
     }
-  else if (sRef_isStateUndefined (other))
+  else if (sRef_isStateUndefined (other)
+          || sRef_isDefinitelyNull (other))
     {
       ;
     }
@@ -9359,6 +9408,7 @@ static void sRef_updateNullState (sRef res, sRef other)
 {
   res->nullstate = other->nullstate;
   res->nullinfo = stateInfo_update (res->nullinfo, other->nullinfo);
+  sRef_resetAliasKind (res);
 }
 
 void sRef_combineNullState (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other)
@@ -9418,6 +9468,7 @@ void sRef_combineNullState (/*@notnull@*/ sRef res, /*@notnull@*/ sRef other)
     }
 
   res->nullstate = nn;
+  sRef_resetAliasKind (res);
 }
 
 cstring sRef_nullMessage (sRef s)