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