src/stateInfo.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2002 University of Virginia,
   4 **         Massachusetts Institute of Technology
   5 **
   6 ** This program is free software; you can redistribute it and/or modify it
   7 ** under the terms of the GNU General Public License as published by the
   8 ** Free Software Foundation; either version 2 of the License, or (at your
   9 ** option) any later version.
  10 **
  11 ** This program is distributed in the hope that it will be useful, but
  12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
  13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  14 ** General Public License for more details.
  15 **
  16 ** The GNU General Public License is available from http://www.gnu.org/ or
  17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  18 ** MA 02111-1307, USA.
  19 **
  20 ** For information on splint: info@splint.org
  21 ** To report a bug: splint-bug@splint.org
  22 ** For more information: http://www.splint.org
  23 */
  24
  25 # include "splintMacros.nf"
  26 # include "basic.h"
  27
  28 void stateInfo_free (/*@only@*/ stateInfo a)
  29 {
  30   if (a != NULL)
  31     {
  32       fileloc_free (a->loc);
  33       sfree (a);
  34     }
  35 }
  36
  37 /*@only@*/ stateInfo stateInfo_update (/*@only@*/ stateInfo old, stateInfo newinfo)
  38      /*
  39      ** returns an stateInfo with the same value as new.  May reuse the
  40      ** storage of old.  (i.e., same effect as copy, but more
  41      ** efficient.)
  42      */
  43 {
  44   if (old == NULL)
  45     {
  46       return stateInfo_copy (newinfo);
  47     }
  48   else if (newinfo == NULL)
  49     {
  50       stateInfo_free (old);
  51       return NULL;
  52     }
  53   else
  54     {
  55       stateInfo snew = stateInfo_makeRefLoc (newinfo->ref, newinfo->loc);
  56       llassert (snew->previous == NULL);
  57       snew->previous = old;
  58       return snew;
  59     }
  60 }
  61
  62 /*@only@*/ stateInfo stateInfo_updateLoc (/*@only@*/ stateInfo old, fileloc loc)
  63 {
  64   if (old == NULL)
  65     {
  66       old = stateInfo_makeLoc (loc);
  67     }
  68   else
  69     {
  70       old->loc = fileloc_update (old->loc, loc);
  71       old->ref = sRef_undefined;
  72     }
  73
  74   return old;
  75 }
  76
  77 /*@only@*/ stateInfo
  78     stateInfo_updateRefLoc (/*@only@*/ stateInfo old, /*@exposed@*/ sRef ref, fileloc loc)
  79 {
  80   if (old == NULL)
  81     {
  82       old = stateInfo_makeRefLoc (ref, loc);
  83     }
  84   else
  85     {
  86       old->loc = fileloc_update (old->loc, loc);
  87       old->ref = ref;
  88     }
  89
  90   return old;
  91 }
  92
  93 /*@only@*/ stateInfo stateInfo_copy (stateInfo a)
  94 {
  95   if (a == NULL)
  96     {
  97       return NULL;
  98     }
  99   else
 100     {
 101       stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
 102
 103       ret->loc = fileloc_copy (a->loc); /*< should report bug without copy! >*/
 104       ret->ref = a->ref;
 105       ret->previous = stateInfo_copy (a->previous);
 106
 107       return ret;
 108     }
 109 }
 110
 111 /*@only@*/ /*@notnull@*/ stateInfo
 112 stateInfo_currentLoc (void)
 113 {
 114   return stateInfo_makeLoc (g_currentloc);
 115 }
 116
 117 /*@only@*/ /*@notnull@*/ stateInfo
 118 stateInfo_makeLoc (fileloc loc)
 119 {
 120   stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
 121
 122   ret->loc = fileloc_copy (loc); /* don't need to copy! */
 123   ret->ref = sRef_undefined;
 124   ret->previous = stateInfo_undefined;
 125
 126   return ret;
 127 }
 128
 129 /*@only@*/ /*@notnull@*/ stateInfo
 130 stateInfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc)
 131      /*@post:isnull result->previous@*/
 132 {
 133   stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
 134
 135   ret->loc = fileloc_copy (loc);
 136   ret->ref = ref;
 137   ret->previous = stateInfo_undefined;
 138
 139   return ret;
 140 }
 141
 142 /*@only@*/ cstring
 143 stateInfo_unparse (stateInfo s)
 144 {
 145     if (stateInfo_isDefined (s) && fileloc_isDefined (s->loc))
 146       {
 147         if (stateInfo_isDefined (s->previous)) {
 148           return message ("%q; %q", fileloc_unparse (s->loc), stateInfo_unparse (s->previous));
 149         } else {
 150           return fileloc_unparse (s->loc);
 151         }
 152       }
 153     else
 154       {
 155         return cstring_makeLiteral ("<no info>");
 156       }
 157 }
 158
 159 fileloc stateInfo_getLoc (stateInfo info)
 160 {
 161     if (stateInfo_isDefined (info))
 162       {
 163         return info->loc;
 164       }
 165
 166     return fileloc_undefined;
 167 }
 168
 169 void stateInfo_display (stateInfo s, cstring sname)
 170 {
 171   while (stateInfo_isDefined (s))
 172     {
 173       cstring msg = message ("Storage %s ", sname);
 174
 175       if (sRef_isValid (s->ref)) {
 176         msg = message ("%q through alias %q ", msg, sRef_unparse (s->ref));
 177       }
 178
 179       msg = message ("%qreleased", msg); /* For now, just used for release...need to make this work. */
 180       llgenindentmsg (msg, s->loc);
 181       s = s->previous;
 182     }
 183
 184   cstring_free (sname);
 185 }
 186
 187