src/annotationInfo.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2003 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 ** annotationInfo.c
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30
  31 annotationInfo annotationInfo_create (cstring name,
  32                                       metaStateInfo state, mtContextNode context,
  33                                       int value, fileloc loc)
  34 {
  35   annotationInfo res = (annotationInfo) dmalloc (sizeof (*res));
  36
  37   res->name = name;
  38   res->state = state;
  39   res->context = context;
  40   res->value = value;
  41   res->loc = loc;
  42
  43   return res;
  44 }
  45
  46 void annotationInfo_free (annotationInfo a)
  47 {
  48   if (annotationInfo_isDefined (a))
  49     {
  50       cstring_free (a->name);
  51       fileloc_free (a->loc);
  52       mtContextNode_free (a->context); /* evans 2002-01-03 */
  53       sfree (a);
  54     }
  55 }
  56
  57 cstring annotationInfo_getName (annotationInfo a)
  58 {
  59   llassert (annotationInfo_isDefined (a));
  60   return a->name;
  61 }
  62
  63 /*@observer@*/ cstring annotationInfo_unparse (annotationInfo a)
  64 {
  65   return annotationInfo_getName (a);
  66 }
  67
  68 /*@observer@*/ metaStateInfo annotationInfo_getState (annotationInfo a) /*@*/
  69 {
  70   llassert (annotationInfo_isDefined (a));
  71   return a->state;
  72 }
  73
  74 /*@observer@*/ fileloc annotationInfo_getLoc (annotationInfo a) /*@*/
  75 {
  76   llassert (annotationInfo_isDefined (a));
  77   return a->loc;
  78 }
  79
  80 int annotationInfo_getValue (annotationInfo a) /*@*/
  81 {
  82   llassert (annotationInfo_isDefined (a));
  83   return a->value;
  84 }
  85
  86
  87 bool annotationInfo_matchesContext (annotationInfo a, uentry ue)
  88 {
  89   /*
  90   ** Returns true iff the annotation context matches the uentry.
  91   */
  92
  93   mtContextNode mcontext;
  94
  95   llassert (annotationInfo_isDefined (a));
  96   mcontext = a->context;
  97
  98   if (mtContextNode_matchesEntry (mcontext, ue))
  99     {
 100       /* Matches annotation context, must also match meta state context. */
 101       metaStateInfo minfo = a->state;
 102
 103       if (mtContextNode_matchesEntry (metaStateInfo_getContext (minfo), ue))
 104         {
 105           return TRUE;
 106         }
 107       else
 108         {
 109           return FALSE;
 110         }
 111     }
 112   else
 113     {
 114       return FALSE;
 115     }
 116 }
 117
 118 bool annotationInfo_matchesContextRef (annotationInfo a, sRef sr)
 119 {
 120   /*
 121   ** Returns true iff the annotation context matches the uentry.
 122   */
 123
 124   mtContextNode mcontext;
 125
 126   llassert (annotationInfo_isDefined (a));
 127   mcontext = a->context;
 128
 129   if (mtContextNode_matchesRef (mcontext, sr))
 130     {
 131       /* Matches annotation context, must also match meta state context. */
 132       metaStateInfo minfo = a->state;
 133
 134       if (mtContextNode_matchesRef (metaStateInfo_getContext (minfo), sr))
 135         {
 136           return TRUE;
 137         }
 138       else
 139         {
 140           return FALSE;
 141         }
 142     }
 143   else
 144     {
 145       return FALSE;
 146     }
 147 }
 148
 149 cstring annotationInfo_dump (annotationInfo a)
 150 {
 151   llassert (annotationInfo_isDefined (a));
 152   return a->name;
 153 }
 154
 155 /*@observer@*/ annotationInfo annotationInfo_undump (char **s)
 156 {
 157   cstring mname = reader_readUntil (s, '.');
 158   annotationInfo a;
 159
 160   llassert (cstring_isDefined (mname));
 161   a = context_lookupAnnotation (mname);
 162
 163   if (annotationInfo_isUndefined (a))
 164     {
 165       llfatalerrorLoc
 166         (message ("Library uses undefined annotation %s.  Must use same -mts flags as when library was created.",
 167                   mname));
 168     }
 169   else
 170     {
 171       cstring_free (mname);
 172       return a;
 173     }
 174
 175   BADBRANCHRET (annotationInfo_undefined);
 176 }
 177
 178 void annotationInfo_showContextRefError (annotationInfo a, sRef sr)
 179 {
 180   mtContextNode mcontext;
 181   llassert (!annotationInfo_matchesContextRef (a, sr));
 182   llassert (annotationInfo_isDefined (a));
 183   mcontext = a->context;
 184
 185   if (mtContextNode_matchesRef (mcontext, sr))
 186     {
 187       /* Matches annotation context, must also match meta state context. */
 188       metaStateInfo minfo = a->state;
 189
 190       if (mtContextNode_matchesRef (metaStateInfo_getContext (minfo), sr))
 191         {
 192           BADBRANCH;
 193         }
 194       else
 195         {
 196           mtContextNode_showRefError (metaStateInfo_getContext (minfo), sr);
 197         }
 198     }
 199   else
 200     {
 201       mtContextNode_showRefError (mcontext, sr);
 202     }
 203 }