src/annotationInfo.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 lclint: lclint-request@cs.virginia.edu
  21 ** To report a bug: lclint-bug@cs.virginia.edu
  22 ** For more information: http://www.splint.org
  23 */
  24 /*
  25 ** annotationInfo.c
  26 */
  27
  28 # include "lclintMacros.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 ainfo)
  47 {
  48   if (annotationInfo_isDefined (ainfo))
  49     {
  50       cstring_free (ainfo->name);
  51       fileloc_free (ainfo->loc);
  52       sfree (ainfo);
  53     }
  54 }
  55
  56 cstring annotationInfo_getName (annotationInfo ainfo)
  57 {
  58   llassert (annotationInfo_isDefined (ainfo));
  59   return ainfo->name;
  60 }
  61
  62 /*@observer@*/ cstring annotationInfo_unparse (annotationInfo ainfo)
  63 {
  64   return annotationInfo_getName (ainfo);
  65 }
  66
  67 /*@observer@*/ metaStateInfo annotationInfo_getState (annotationInfo a) /*@*/
  68 {
  69   llassert (annotationInfo_isDefined (a));
  70   return a->state;
  71 }
  72
  73 /*@observer@*/ fileloc annotationInfo_getLoc (annotationInfo ainfo) /*@*/
  74 {
  75   llassert (annotationInfo_isDefined (ainfo));
  76   return ainfo->loc;
  77 }
  78
  79 int annotationInfo_getValue (annotationInfo a) /*@*/
  80 {
  81   llassert (annotationInfo_isDefined (a));
  82   return a->value;
  83 }
  84
  85
  86 bool annotationInfo_matchesContext (annotationInfo a, uentry ue)
  87 {
  88   /*
  89   ** Returns true iff the annotation context matches the uentry.
  90   */
  91
  92   mtContextNode mcontext;
  93
  94   llassert (annotationInfo_isDefined (a));
  95   mcontext = a->context;
  96
  97   if (mtContextNode_matchesEntry (mcontext, ue))
  98     {
  99       /* Matches annotation context, must also match meta state context. */
 100       metaStateInfo minfo = a->state;
 101
 102       if (mtContextNode_matchesEntry (metaStateInfo_getContext (minfo), ue))
 103         {
 104           return TRUE;
 105         }
 106       else
 107         {
 108           return FALSE;
 109         }
 110     }
 111   else
 112     {
 113       return FALSE;
 114     }
 115 }
 116
 117 bool annotationInfo_matchesContextRef (annotationInfo a, sRef sr)
 118 {
 119   /*
 120   ** Returns true iff the annotation context matches the uentry.
 121   */
 122
 123   mtContextNode mcontext;
 124
 125   llassert (annotationInfo_isDefined (a));
 126   mcontext = a->context;
 127
 128   if (mtContextNode_matchesRef (mcontext, sr))
 129     {
 130       /* Matches annotation context, must also match meta state context. */
 131       metaStateInfo minfo = a->state;
 132
 133       if (mtContextNode_matchesRef (metaStateInfo_getContext (minfo), sr))
 134         {
 135           return TRUE;
 136         }
 137       else
 138         {
 139           return FALSE;
 140         }
 141     }
 142   else
 143     {
 144       return FALSE;
 145     }
 146 }
 147
 148 cstring annotationInfo_dump (annotationInfo ainfo)
 149 {
 150   llassert (annotationInfo_isDefined (ainfo));
 151   return ainfo->name;
 152 }
 153
 154 /*@observer@*/ annotationInfo annotationInfo_undump (char **s)
 155 {
 156   cstring mname = reader_readUntil (s, '.');
 157   annotationInfo ainfo;
 158
 159   llassert (cstring_isDefined (mname));
 160   ainfo = context_lookupAnnotation (mname);
 161
 162   if (annotationInfo_isUndefined (ainfo))
 163     {
 164       llfatalerrorLoc
 165         (message ("Library uses undefined annotation %s.  Must use same -mts flags as when library was created.",
 166                   mname));
 167     }
 168   else
 169     {
 170       cstring_free (mname);
 171       return ainfo;
 172     }
 173
 174   BADBRANCHRET (annotationInfo_undefined);
 175 }
 176
 177 void annotationInfo_showContextRefError (annotationInfo a, sRef sr)
 178 {
 179   mtContextNode mcontext;
 180   llassert (!annotationInfo_matchesContextRef (a, sr));
 181   llassert (annotationInfo_isDefined (a));
 182   mcontext = a->context;
 183
 184   if (mtContextNode_matchesRef (mcontext, sr))
 185     {
 186       /* Matches annotation context, must also match meta state context. */
 187       metaStateInfo minfo = a->state;
 188
 189       if (mtContextNode_matchesRef (metaStateInfo_getContext (minfo), sr))
 190         {
 191           BADBRANCH;
 192         }
 193       else
 194         {
 195           mtContextNode_showRefError (metaStateInfo_getContext (minfo), sr);
 196         }
 197     }
 198   else
 199     {
 200       mtContextNode_showRefError (mcontext, sr);
 201     }
 202 }