src/stateClauseList.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 ** stateClauseList.c
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30
  31 static /*@notnull@*/ stateClauseList stateClauseList_new (void)
  32 {
  33   stateClauseList s = (stateClauseList) dmalloc (sizeof (*s));
  34
  35   s->nelements = 0;
  36   s->nspace = stateClauseListBASESIZE;
  37   s->elements = (stateClause *)
  38     dmalloc (sizeof (*s->elements) * stateClauseListBASESIZE);
  39
  40   return (s);
  41 }
  42
  43 static void
  44 stateClauseList_grow (stateClauseList s)
  45 {
  46   int i;
  47   stateClause *newelements;
  48
  49   llassert (stateClauseList_isDefined (s));
  50
  51   s->nspace += stateClauseListBASESIZE;
  52
  53   newelements = (stateClause *)
  54     dmalloc (sizeof (*newelements) * (s->nelements + s->nspace));
  55
  56   for (i = 0; i < s->nelements; i++)
  57     {
  58       newelements[i] = s->elements[i];
  59     }
  60
  61   sfree (s->elements);
  62   s->elements = newelements;
  63 }
  64
  65 stateClauseList stateClauseList_add (stateClauseList s, stateClause el)
  66 {
  67   DPRINTF (("Adding: %s", stateClause_unparse (el)));
  68
  69   if (stateClauseList_isUndefined (s))
  70     {
  71       s = stateClauseList_new ();
  72     }
  73   else
  74     {
  75       stateClauseList_elements (s, cl)
  76         {
  77           if (stateClause_sameKind (cl, el))
  78             {
  79               voptgenerror
  80                 (FLG_SYNTAX,
  81                  message ("Multiple %q clauses for one function (ignoring second)",
  82                           stateClause_unparseKind (cl)),
  83                  g_currentloc);
  84
  85               stateClause_free (el);
  86               return s;
  87             }
  88         } end_stateClauseList_elements ;
  89     }
  90
  91   if (s->nspace <= 0)
  92     {
  93       stateClauseList_grow (s);
  94     }
  95
  96   s->nspace--;
  97   s->elements[s->nelements] = el;
  98   s->nelements++;
  99
 100   return s;
 101 }
 102
 103 cstring stateClauseList_unparse (stateClauseList s)
 104 {
 105   cstring st = cstring_undefined;
 106   int i;
 107
 108   if (stateClauseList_isDefined (s))
 109     {
 110       for (i = 0; i < stateClauseList_size (s); i++)
 111         {
 112           if (i == 0)
 113             {
 114               st = message ("%q;", stateClause_unparse (s->elements[i]));
 115             }
 116           else
 117             st = message ("%q %q;", st, stateClause_unparse (s->elements[i]));
 118         }
 119     }
 120
 121   return (st);
 122 }
 123
 124 stateClauseList stateClauseList_copy (stateClauseList s)
 125 {
 126   if (stateClauseList_isDefined (s))
 127     {
 128       stateClauseList t = (stateClauseList) dmalloc (sizeof (*t));
 129       int i;
 130
 131       t->nelements = s->nelements;
 132       t->nspace = 0;
 133
 134       if (s->nelements > 0)
 135         {
 136           t->elements = (stateClause *) dmalloc (sizeof (*t->elements) * t->nelements);
 137           for (i = 0; i < s->nelements; i++)
 138             {
 139               t->elements[i] = stateClause_copy (s->elements[i]);
 140             }
 141         }
 142       else
 143         {
 144           t->elements = NULL;
 145         }
 146
 147       return t;
 148     }
 149   else
 150     {
 151       return stateClauseList_undefined;
 152     }
 153 }
 154
 155 void
 156 stateClauseList_free (stateClauseList s)
 157 {
 158   if (!stateClauseList_isUndefined (s))
 159     {
 160       int i;
 161
 162       for (i = 0; i < s->nelements; i++)
 163         {
 164           stateClause_free (s->elements[i]);
 165         }
 166
 167       sfree (s->elements);
 168       sfree (s);
 169     }
 170 }
 171
 172 cstring stateClauseList_dump (stateClauseList s)
 173 {
 174   cstring st = cstring_undefined;
 175
 176   if (stateClauseList_isUndefined (s)) return st;
 177
 178   stateClauseList_elements (s, current)
 179     {
 180       st = message ("%q%q$", st, stateClause_dump (current));
 181     } end_stateClauseList_elements;
 182
 183   return st;
 184 }
 185
 186 stateClauseList stateClauseList_undump (char **s)
 187 {
 188   char c;
 189   stateClauseList pn = stateClauseList_new ();
 190   int paramno = 0;
 191
 192   c = **s;
 193
 194   while (c != '#' && c != '@')
 195     {
 196       stateClause sc = stateClause_undump (s);
 197
 198       pn = stateClauseList_add (pn, sc);
 199       reader_checkChar (s, '$');
 200       c = **s;
 201       paramno++;
 202     }
 203
 204   return pn;
 205 }
 206
 207 int stateClauseList_compare (stateClauseList s1, stateClauseList s2)
 208 {
 209   if (stateClauseList_isUndefined (s1)
 210       && stateClauseList_isUndefined (s2))
 211     {
 212       return 0;
 213     }
 214   else
 215     {
 216       if (s1 - s2 > 0) /* evans 2001-08-21: was (int) s1 > (int) s2) */
 217         {
 218           return 1;
 219         }
 220       else
 221         {
 222           return -1;
 223         }
 224     }
 225 }
 226
 227 static /*@exposed@*/ sRefSet
 228 stateClauseList_getClause (stateClauseList s, stateClause k)
 229 {
 230   stateClauseList_elements (s, el)
 231     {
 232       if (stateClause_matchKind (el, k))
 233         {
 234           return stateClause_getRefs (el);
 235         }
 236     } end_stateClauseList_elements ;
 237
 238   return sRefSet_undefined;
 239 }
 240
 241 void stateClauseList_checkAll (uentry ue)
 242 {
 243   stateClauseList clauses = uentry_getStateClauseList (ue);
 244   sRef res = uentry_getSref (ue);
 245   bool specialResult = FALSE;
 246
 247   DPRINTF (("Check state clauses: %s", uentry_unparseFull (ue)));
 248
 249   stateClauseList_elements (clauses, cl)
 250     {
 251       bool isPre = stateClause_isBeforeOnly (cl);
 252
 253       if (stateClause_isGlobal (cl))
 254         {
 255           ;
 256         }
 257       else
 258         {
 259           sRefSet refs = stateClause_getRefs (cl);
 260
 261           sRefSet_allElements (refs, el)
 262             {
 263               sRef rb = sRef_getRootBase (el);
 264
 265               DPRINTF (("Check: %s", sRef_unparse (el)));
 266
 267               if (sRef_isResult (rb))
 268                 {
 269                   /*
 270                   ** The result type is now know, need to set it:
 271                   */
 272
 273                   if (ctype_isUnknown (sRef_getType (rb)))
 274                     {
 275                       ctype utype = uentry_getType (ue);
 276                       llassert (ctype_isFunction (utype));
 277
 278                       sRef_setTypeFull (rb, ctype_getReturnType (utype));
 279                       DPRINTF (("el: %s", sRef_unparseFull (el)));
 280                     }
 281                 }
 282
 283               if (stateClause_setsMetaState (cl))
 284                 {
 285                   qual q = stateClause_getMetaQual (cl);
 286                   annotationInfo qa = qual_getAnnotationInfo (q);
 287
 288                   if (!annotationInfo_matchesContextRef (qa, el))
 289                     {
 290                       if (optgenerror
 291                           (FLG_ANNOTATIONERROR,
 292                            message ("Attribute annotation %s used on inappropriate reference %q in %q clause of %q: %q",
 293                                     qual_unparse (q),
 294                                     sRef_unparse (el),
 295                                     stateClause_unparseKind (cl),
 296                                     uentry_getName (ue),
 297                                     stateClause_unparse (cl)),
 298                            uentry_whereLast (ue)))
 299                         {
 300                           /* annotationInfo_showContextError (ainfo, ue); */
 301                         }
 302                     }
 303                 }
 304
 305               if (sRef_isResult (rb))
 306                 {
 307                   if (isPre)
 308                     {
 309                       voptgenerror
 310                         (FLG_INCONDEFS,
 311                          message ("Function result is used in %q clause of %q "
 312                                   "(%q applies to the state before function is "
 313                                   "called, so should not use result): %q",
 314                                   stateClause_unparseKind (cl),
 315                                   uentry_getName (ue),
 316                                   stateClause_unparseKind (cl),
 317                                   sRef_unparse (el)),
 318                          uentry_whereLast (ue));
 319                     }
 320                   else
 321                     {
 322                       if (!sRef_isStateSpecial (res))
 323                         {
 324                           DPRINTF (("Here we are: %s", sRef_unparseFull (res)));
 325
 326                           if (!specialResult)
 327                             {
 328                               sstate pstate = sRef_getDefState (res);
 329
 330                               if (!sRef_makeStateSpecial (res))
 331                                 {
 332                                   if (optgenerror
 333                                       (FLG_INCONDEFS,
 334                                        message ("Function result is used in %q clause of %q "
 335                                                 "but was previously annotated with %s: %q",
 336                                                 stateClause_unparseKind (cl),
 337                                                 uentry_getName (ue),
 338                                                 sstate_unparse (pstate),
 339                                                 sRef_unparse (el)),
 340                                        uentry_whereLast (ue)))
 341                                     {
 342                                       specialResult = TRUE;
 343                                     }
 344                                 }
 345                             }
 346                         }
 347
 348                       DPRINTF (("Fixing result type! %s", sRef_unparseFull (el)));
 349                       (void) sRef_fixResultType (el, sRef_getType (res), ue);
 350                     }
 351                 }
 352               else if (sRef_isParam (rb))
 353                 {
 354                   DPRINTF (("Make special: %s", sRef_unparseFull (rb)));
 355
 356                   if (!sRef_makeStateSpecial (rb))
 357                     {
 358                       if (fileloc_isXHFile (uentry_whereLast (ue)))
 359                         {
 360                           ; /* Okay to override in .xh files */
 361                         }
 362                       else if (stateClause_isQual (cl))
 363                         {
 364                           ; /* qual clauses don't interfere with definition state */
 365                         }
 366                       else
 367                         {
 368                           voptgenerror
 369                             (FLG_INCONDEFS,
 370                              message ("Reference %q used in %q clause of %q, "
 371                                       "but was previously annotated with %s: %q",
 372                                       sRef_unparse (rb),
 373                                       stateClause_unparseKind (cl),
 374                                       uentry_getName (ue),
 375                                       sstate_unparse (sRef_getDefState (res)),
 376                                       sRef_unparse (el)),
 377                              uentry_whereLast (ue));
 378                         }
 379                     }
 380
 381                   DPRINTF (("Made special: %s", sRef_unparseFull (rb)));
 382                 }
 383               else if (sRef_isInvalid (rb))
 384                 {
 385                   /*@innercontinue@*/ continue;
 386                 }
 387               else
 388                 {
 389                   BADBRANCHCONT;
 390                   /*@innercontinue@*/ continue;
 391                 }
 392
 393               if (stateClause_isMemoryAllocation (cl))
 394                 {
 395                   if (!ctype_isVisiblySharable (sRef_getType (el)))
 396                     {
 397                       voptgenerror
 398                         (FLG_ANNOTATIONERROR,
 399                          /*@-sefparams@*/ /* This is okay because its fresh storage. */
 400                          message
 401                          ("%q clauses includes %q of "
 402                           "non-dynamically allocated type %s",
 403                           cstring_capitalizeFree (stateClause_unparseKind (cl)),
 404                           sRef_unparse (el),
 405                           ctype_unparse (sRef_getType (el))),
 406                          uentry_whereLast (ue));
 407                       /*@=sefparams@*/
 408                     }
 409                 }
 410
 411             } end_sRefSet_allElements ;
 412         }
 413     } end_stateClauseList_elements ;
 414 }
 415
 416 void stateClauseList_checkEqual (uentry old, uentry unew)
 417 {
 418   stateClauseList oldClauses = uentry_getStateClauseList (old);
 419   stateClauseList newClauses = uentry_getStateClauseList (unew);
 420
 421   if (stateClauseList_isDefined (newClauses))
 422     {
 423       stateClauseList_elements (newClauses, cl)
 424         {
 425           if (stateClause_isGlobal (cl))
 426             {
 427               ;
 428             }
 429           else
 430             {
 431               sRefSet sc = stateClauseList_getClause (oldClauses, cl);
 432
 433               if (!sRefSet_equal (sc, stateClause_getRefs (cl)))
 434                 {
 435                   if (optgenerror
 436                       (FLG_INCONDEFS,
 437                        message ("Function %q %rdeclared with inconsistent %q clause: %q",
 438                                 uentry_getName (old),
 439                                 uentry_isDeclared (old),
 440                                 stateClause_unparseKind (cl),
 441                                 sRefSet_unparsePlain (stateClause_getRefs (cl))),
 442                        g_currentloc))
 443                     {
 444                       uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc));
 445                     }
 446                 }
 447             }
 448         } end_stateClauseList_elements ;
 449
 450       stateClauseList_elements (oldClauses, cl)
 451         {
 452           if (stateClause_isGlobal (cl))
 453             {
 454               ; /* Don't handle globals for now */
 455             }
 456           else
 457             {
 458               sRefSet sc = stateClauseList_getClause (newClauses, cl);
 459
 460               if (sRefSet_isUndefined (sc) && !sRefSet_isEmpty (stateClause_getRefs (cl)))
 461                 {
 462                   if (optgenerror
 463                       (FLG_INCONDEFS,
 464                        message ("Function %q %rdeclared without %q clause (either "
 465                                 "use no special clauses in redeclaration, or "
 466                                 "they must match exactly: %q",
 467                                 uentry_getName (old),
 468                                 uentry_isDeclared (old),
 469                                 stateClause_unparseKind (cl),
 470                                 sRefSet_unparsePlain (stateClause_getRefs (cl))),
 471                        g_currentloc))
 472                     {
 473                       uentry_showWhereLastExtra (old, sRefSet_unparsePlain (sc));
 474                     }
 475                 }
 476             }
 477         } end_stateClauseList_elements ;
 478     }
 479 }
 480
 481
 482