src/checking.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 ** checking.c
  26 **
  27 ** sort checking.
  28 **
  29 **  AUTHOR:
  30 **      Yang Meng Tan,
  31 **         Massachusetts Institute of Technology
  32 */
  33
  34 # include "splintMacros.nf"
  35 # include "basic.h"
  36 # include "llgrammar.h"
  37 # include "checking.h"
  38
  39 /*@+ignorequals@*/
  40
  41 static /*@only@*/ cstring printBadArgs (sortSetList p_args);
  42 static /*@only@*/ sortSet
  43   standardOperators (/*@null@*/ nameNode p_n, sortSetList p_argSorts, sort p_q);
  44 static bool isStandardOperator (/*@null@*/ nameNode p_n);
  45 static void assignSorts (termNode p_t, sort p_s);
  46
  47 /*@null@*/ termNode
  48 computePossibleSorts (/*@returned@*/ /*@null@*/ termNode t)
  49 {
  50   ltoken errtok;
  51
  52   if (t != (termNode) 0)
  53     {
  54       switch (t->kind)
  55         {
  56         case TRM_LITERAL:
  57         case TRM_CONST:
  58         case TRM_VAR:
  59         case TRM_ZEROARY:
  60         case TRM_SIZEOF:
  61         case TRM_UNCHANGEDALL:
  62         case TRM_UNCHANGEDOTHERS:
  63         case TRM_QUANTIFIER:
  64           break;
  65         case TRM_APPLICATION:
  66           {
  67             bool fail = FALSE;
  68             sortSetList argSorts = sortSetList_new ();
  69             lslOpSet ops;
  70             sortSet standards;
  71
  72             if (termNodeList_size (t->args) != 0)
  73               {
  74                 termNodeList_elements (t->args, arg)
  75                 {
  76                   (void) computePossibleSorts (arg);
  77
  78                   if (sortSet_size (arg->possibleSorts) == 0)
  79                     {
  80                       fail = TRUE;
  81                     }
  82                   else
  83                     {
  84                       sortSetList_addh (argSorts, arg->possibleSorts);
  85                     }
  86                 } end_termNodeList_elements;
  87
  88                 if (fail)
  89                   {
  90                     lslOpSet_free (t->possibleOps);
  91                     sortSetList_free (argSorts);
  92                     t->possibleOps = lslOpSet_new ();
  93                     return t;
  94                   }
  95               }
  96
  97             ops = symtable_opsWithLegalDomain (g_symtab, t->name, argSorts, t->given);
  98             lslOpSet_free (t->possibleOps);
  99             t->possibleOps = ops;
 100
 101             lslOpSet_elements (t->possibleOps, op)
 102               {
 103                 sort sort;
 104                 sort = sigNode_rangeSort (op->signature);
 105                 (void) sortSet_insert (t->possibleSorts, sort);
 106               } end_lslOpSet_elements;
 107
 108             standards = standardOperators (t->name, argSorts, t->given);
 109
 110             sortSet_elements (standards, el)
 111               {
 112                 (void) sortSet_insert (t->possibleSorts, el);
 113               } end_sortSet_elements;
 114
 115             sortSet_free (standards);
 116
 117             if (!(t->error_reported) && sortSet_size (t->possibleSorts) == 0)
 118               {
 119                 unsigned int arity = termNodeList_size (t->args);
 120                 errtok = nameNode_errorToken (t->name);
 121
 122                 /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
 123
 124                 if (isStandardOperator (t->name))
 125                   {
 126                     lclerror (errtok,
 127                               message ("Type error: %q not declared for %q",
 128                                       nameNode_unparse (t->name), printBadArgs (argSorts)));
 129                   }
 130                 else if (t->name != NULL
 131                          && symtable_opExistsWithArity (g_symtab, t->name, arity))
 132                   {
 133                     sigNodeSet possibleOps = symtable_possibleOps (g_symtab, t->name);
 134                     cstring opName = nameNode_unparse (t->name);
 135
 136                     /*
 137                     ** all these will be standardOperators soon...
 138                     */
 139
 140                     if (cstring_equalLit (opName, "__ [__]"))
 141                       {
 142                         lclerror (errtok,
 143                                   message ("Type error: %q not declared for %q",
 144                                           opName, printBadArgs (argSorts)));
 145                       }
 146                     else
 147                       {
 148                         lclerror (errtok,
 149                                   message ("Type error: %q declared: %q\ngiven: %q",
 150                                           opName,
 151                                           sigNodeSet_unparseSomeSigs (possibleOps),
 152                                           printBadArgs (argSorts)));
 153                       }
 154                   }
 155                 else
 156                   {
 157                     sigNodeSet possibleOps;
 158                     int npossibleOps;
 159
 160                     llassert (t->name != NULL);
 161
 162                     possibleOps = symtable_possibleOps (g_symtab, t->name);
 163                     npossibleOps = sigNodeSet_size (possibleOps);
 164
 165                     /*
 166                      ** evs --- check is it is wrong arity...
 167                      */
 168
 169                     if (npossibleOps == 0)
 170                       {
 171                         lclerror
 172                           (errtok,
 173                            message ("Undeclared operator: %q", nameNode_unparse (t->name)));
 174                       }
 175                     else
 176                       {
 177                         lclerror
 178                           (errtok,
 179                            message ("Operator %q declared for %q arguments, given %d",
 180                                    nameNode_unparse (t->name),
 181                                    sigNodeSet_unparsePossibleAritys (possibleOps),
 182                                    arity));
 183                       }
 184                   }
 185                 t->error_reported = TRUE;
 186               }
 187             sortSetList_free (argSorts);
 188             break;
 189           }
 190         }
 191     }
 192
 193   return t;
 194 }
 195
 196 static /*@only@*/ cstring
 197 printBadArgs (sortSetList args)
 198 {
 199   if (sortSetList_size (args) == 1)
 200     {
 201       return (sortSet_unparseOr (sortSetList_head (args)));
 202     }
 203   else
 204     {
 205       cstring s = cstring_undefined;
 206       int argno = 1;
 207
 208       sortSetList_elements (args, ss)
 209         {
 210           if (argno == 1)
 211             s = message ("arg %d: %q", argno, sortSet_unparseOr (ss));
 212           else
 213             s = message ("%q; arg %d: %q", s, argno, sortSet_unparseOr (ss));
 214           argno++;
 215         } end_sortSetList_elements;
 216
 217       return s;
 218     }
 219 }
 220
 221 termNode
 222 checkSort (/*@returned@*/ termNode t)
 223 {
 224   sortSet sorts;
 225   sort theSort;
 226   int size;
 227   ltoken errtok;
 228
 229   (void) computePossibleSorts (t);
 230   sorts = t->possibleSorts;
 231
 232   llassert (sortSet_isDefined (sorts));
 233
 234   size = sortSet_size (sorts);
 235   switch (size)
 236     {
 237     case 0:                     /* complain later */
 238       break;
 239     case 1:                     /* just right */
 240       theSort = sortSet_choose (sorts);
 241       assignSorts (t, theSort);
 242       break;
 243     default:
 244      /* we allow C literals to have multiple sorts */
 245       if (t->kind != TRM_LITERAL)
 246         {
 247           errtok = termNode_errorToken (t);
 248           t->error_reported = TRUE;
 249
 250           lclerror (errtok,
 251                     message ("Term %q: can have more than one possible type.  Possible types: %q",
 252                              termNode_unparse (t), sortSet_unparseClean (sorts)));
 253         }
 254     }
 255   return t;
 256 }
 257
 258 static void
 259   assignSorts (termNode t, sort s)
 260 {
 261  /* other kinds are already assigned bottom-up */
 262   ltoken errtok;
 263
 264   switch (t->kind)
 265     {
 266     case TRM_ZEROARY:   /* pick s to be the sort chosen */
 267     case TRM_LITERAL:
 268       sortSet_elements (t->possibleSorts, s2)
 269       {
 270         if (sort_equal (s2, s))
 271           {
 272             sortSet_free (t->possibleSorts);
 273             t->possibleSorts = sortSet_new ();
 274             (void) sortSet_insert (t->possibleSorts, s);
 275             t->sort = s;
 276           }
 277         return;
 278       } end_sortSet_elements;
 279       break;
 280     case TRM_APPLICATION:
 281       {
 282         lslOpSet sigs = t->possibleOps;
 283         lslOpSet oldops = lslOpSet_undefined;
 284         sigNode op = (sigNode) 0;
 285         nameNode name = t->name;
 286         termNodeList args = t->args;
 287         bool found = FALSE;
 288
 289         errtok = nameNode_errorToken (name);
 290
 291         /* why compute again? to check for duplicates */
 292         lslOpSet_elements (sigs, sig)
 293           {
 294             sort rsort = sigNode_rangeSort (sig->signature);
 295
 296             if (sort_equal (s, rsort))
 297               {
 298                 lslOp iop;
 299
 300                 if (found)
 301                   {
 302                     t->error_reported = TRUE;
 303
 304                     lclerror (errtok,
 305                               message ("Ambiguous operator %q: %q or %q",
 306                                        nameNode_unparse (name),
 307                                        sigNode_unparse (op),
 308                                        sigNode_unparse (sig->signature)));
 309                     return;
 310                   }
 311
 312                 iop = (lslOp) dmalloc (sizeof (*iop));
 313                 found = TRUE;
 314                 op = sig->signature;
 315
 316                 oldops = t->possibleOps;
 317                 t->possibleOps = lslOpSet_new ();
 318                 iop->name = nameNode_copy (name);
 319                 iop->signature = op;
 320                 (void) lslOpSet_insert (t->possibleOps, iop);
 321                 t->sort = s;
 322                 /*@-branchstate@*/
 323               }
 324             /*@=branchstate@*/
 325           } end_lslOpSet_elements;
 326
 327         lslOpSet_free (oldops);
 328
 329         if (!found)
 330           {
 331             if (sortSet_size (t->possibleSorts) == 1)
 332               {
 333                 t->sort = sortSet_choose (t->possibleSorts);
 334               }
 335             else
 336               {
 337                 /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
 338                 t->error_reported = TRUE;
 339
 340                 lclerror (errtok, message ("Operator not found: %q",
 341                                            nameNode_unparse (name)));
 342                 /* evs --- ??? */
 343               }
 344             return;
 345           }
 346
 347         if (termNodeList_empty (args))
 348           {
 349             if (op != (sigNode) 0)
 350               {
 351                 /* was --- NB: copy to avoid interference */
 352                 /* shouldn't need to copy --- its a fresh list */
 353                 sortList dom = sigNode_domain (op);
 354
 355                 sortList_reset (dom);
 356                 termNodeList_elements (args, arg)
 357                   {
 358                     assignSorts (arg, sortList_current (dom));
 359                     sortList_advance (dom);
 360                   } end_termNodeList_elements;
 361
 362                 sortList_free (dom);
 363               }
 364             else
 365               {
 366                 errtok = nameNode_errorToken (name);
 367                 /* errorShowPoint (inputStream_thisLine (lclsource), ltoken_getCol (errtok)); */
 368                 t->error_reported = TRUE;
 369
 370                 lclerror (errtok, message ("No matching operator: %q",
 371                                            nameNode_unparse (name)));
 372               }
 373             return;
 374           }
 375         break;
 376       }
 377     default:                    /* do nothing */
 378       break;
 379     }
 380 }
 381
 382 void
 383 checkLclPredicate (ltoken t, lclPredicateNode n)
 384 {
 385   sort theSort;
 386
 387   if ((n == NULL) || (n->predicate == NULL))
 388     {
 389       llcontbuglit ("checkLclPredicate expects valid lclPredicate.  "
 390                     "Skipping current check");
 391       return;
 392     }
 393
 394  /* check only if there are no previous errors */
 395
 396   if (!n->predicate->error_reported)
 397     {
 398      /* check that the sort of n is boolean */
 399       theSort = n->predicate->sort;
 400       if (!sort_compatible (theSort, g_sortCapBool))
 401         {
 402           if (sort_isNoSort (theSort))
 403             {
 404              ; /* "Expects a boolean term.  Given term has unknown sort" */
 405             }
 406           else
 407             {
 408               cstring clauset = ltoken_getRawString (t);
 409
 410               if (cstring_firstChar (clauset) == '(')
 411                 {
 412                   clauset = cstring_makeLiteral ("Equality");
 413                 }
 414               else
 415                 {
 416                   /* uppercase first letter */
 417                   clauset = cstring_copy (clauset);
 418                   cstring_setChar (clauset, 1,
 419                                    (char) toupper (cstring_firstChar (clauset)));
 420                 }
 421
 422               lclerror (t, message ("%q expects a boolean term, given %q.",
 423                                     clauset, sort_unparse (theSort)));
 424
 425             }
 426         }
 427     }
 428 }
 429
 430 /*
 431 ** these should not be doing string comparisons!
 432 */
 433
 434 static bool isDeRefOperator (cstring s)
 435 {
 436   return (cstring_equalLit (s, "*"));
 437 }
 438
 439 static bool isStateOperator (cstring s)
 440 {
 441   return (cstring_equalLit (s, "^") ||
 442           cstring_equalLit (s, "'") ||
 443           cstring_equalLit (s, "\\any") ||
 444           cstring_equalLit (s, "\\pre") ||
 445           cstring_equalLit (s, "\\post"));
 446 }
 447
 448 static bool isCompareOperator (cstring s) /* YUCK!!! */
 449 {
 450   return (cstring_equalLit (s, "\\eq") ||
 451           cstring_equalLit (s, "\\neq") ||
 452           cstring_equalLit (s, "=") ||
 453           cstring_equalLit (s, "!=") ||
 454           cstring_equalLit (s, "~=") ||
 455           cstring_equalLit (s, "=="));
 456 }
 457
 458 static bool isStandardOperator (/*@null@*/ nameNode n)
 459 {
 460   if (n != (nameNode) 0)
 461     {
 462       if (!n->isOpId)
 463         {
 464           opFormNode opf = n->content.opform;
 465
 466           llassert (opf != NULL);
 467
 468           switch (opf->kind)
 469             {
 470             case OPF_IF: return TRUE;
 471             case OPF_ANYOP:
 472               break;
 473             case OPF_MANYOP:
 474               {
 475                 cstring s = ltoken_getRawString (opf->content.anyop);
 476
 477                 if (isStateOperator (s)) return TRUE;
 478                 return FALSE;
 479               }
 480             case OPF_ANYOPM:
 481               /* operator: *__ */
 482               {
 483                 cstring s = ltoken_getRawString (opf->content.anyop);
 484
 485                 return (isDeRefOperator (s));
 486               }
 487             case OPF_MANYOPM:
 488               {
 489                 cstring s = ltoken_getRawString (opf->content.anyop);
 490
 491                 return (isCompareOperator (s));
 492               }
 493             case OPF_MIDDLE:
 494               break;
 495             case OPF_MMIDDLE:
 496               break;
 497             case OPF_MIDDLEM:
 498               break;
 499             case OPF_MMIDDLEM:
 500               break;
 501             case OPF_BMIDDLE:
 502               break;
 503             case OPF_BMMIDDLE:
 504               break;
 505             case OPF_BMIDDLEM:
 506               break;
 507             case OPF_BMMIDDLEM:
 508               break;
 509             case OPF_SELECT:
 510               break;
 511             case OPF_MAP:
 512               break;
 513             case OPF_MSELECT:
 514               break;
 515             case OPF_MMAP:
 516               break;
 517             default:
 518               break;
 519             }
 520         }
 521       else
 522         {
 523           int code = ltoken_getCode (n->content.opid);
 524
 525           if (code == simpleId)
 526             {
 527               cstring text = nameNode_unparse (n);
 528               bool ret = (cstring_equalLit (text, "trashed")
 529                           || cstring_equalLit (text, "maxIndex")
 530                           || cstring_equalLit (text, "minIndex")
 531                           || cstring_equalLit (text, "isSub"));
 532
 533               cstring_free (text);
 534               return ret;
 535             }
 536
 537           return (code == LLT_MODIFIES || code == LLT_FRESH
 538                   || code == LLT_UNCHANGED || code == LLT_SIZEOF);
 539         }
 540     }
 541   return FALSE;
 542 }
 543
 544 static /*@only@*/ sortSet
 545 standardOperators (/*@null@*/ nameNode n, sortSetList argSorts, /*@unused@*/ sort q)
 546 {
 547   sortSet argSet;
 548   sortSet ret = sortSet_new ();
 549
 550   if (n == (nameNode) 0) return ret;
 551
 552   if (n->isOpId)
 553     {
 554       int code = ltoken_getCode (n->content.opid);
 555
 556       if (sortSetList_size (argSorts) == 1)
 557         {
 558           sortSetList_reset (argSorts);
 559
 560           argSet = sortSetList_current (argSorts);
 561
 562           sortSet_elements (argSet, current)
 563             {
 564               sortNode sn;
 565
 566               sn = sort_quietLookup (current);
 567
 568               while (sn->kind == SRT_SYN)
 569                 {
 570                   sn = sort_quietLookup (sn->baseSort);
 571                 }
 572
 573               /*@-loopswitchbreak@*/
 574               switch (code)
 575                 {
 576                 case simpleId:
 577                   {
 578                     cstring text = ltoken_getRawString (n->content.opid);
 579
 580                     if (cstring_equalLit (text, "trashed")) /* GACK! */
 581                       {
 582                         if (sn->kind == SRT_OBJ ||
 583                             sn->kind == SRT_ARRAY)
 584                         (void) sortSet_insert (ret, g_sortBool);
 585                       }
 586
 587                     if (cstring_equalLit (text, "maxIndex") ||
 588                         cstring_equalLit (text, "minIndex"))
 589                       {
 590                         if (sn->kind == SRT_ARRAY || sn->kind == SRT_PTR)
 591                           (void) sortSet_insert (ret, g_sortInt);
 592
 593                         /*                if (lsymbol_fromChars ("maxIndex") */
 594                       }
 595                   }
 596                   break;
 597                 case LLT_MODIFIES:
 598                 case LLT_FRESH:
 599                 case LLT_UNCHANGED:
 600                   if (sn->kind == SRT_OBJ ||
 601                       sn->kind == SRT_ARRAY)
 602                     {
 603                       (void) sortSet_insert (ret, g_sortBool);
 604                     }
 605                   break;
 606                 case LLT_SIZEOF:
 607                   if (sn->kind == SRT_OBJ ||
 608                       sn->kind == SRT_ARRAY ||
 609                       sn->kind == SRT_VECTOR)
 610                   (void) sortSet_insert (ret, g_sortInt);
 611                   break;
 612                 default:
 613                   break;
 614                 }
 615             } end_sortSet_elements;
 616         }
 617     }
 618   else
 619     {
 620       opFormNode opf = n->content.opform;
 621
 622       llassert (opf != NULL);
 623
 624       switch (opf->kind)
 625         {
 626         case OPF_IF:
 627           /*
 628           ** if __ then __ else __ : bool, S, S -> S
 629           **     is defined for all sorts
 630           */
 631
 632           if (sortSetList_size (argSorts) == 3)
 633             {
 634               argSet = sortSetList_head (argSorts);
 635
 636               if (sortSet_member (argSet, g_sortBool))
 637                 {
 638                   sortSetList_reset (argSorts);
 639                   sortSetList_advance (argSorts);
 640
 641                   argSet = sortSetList_current (argSorts);
 642
 643                   if (sortSet_size (argSet) == 1)
 644                     {
 645                       sort clause = sortSet_choose (argSet);
 646                       sort clause2;
 647
 648                       sortSetList_advance (argSorts);
 649                       argSet = sortSetList_current (argSorts);
 650
 651                       clause2 = sortSet_choose (argSet);
 652
 653                       if (sortSet_size (argSet) == 1 &&
 654                           sort_equal (clause, clause2))
 655                         {
 656                           (void) sortSet_insert (ret, clause);
 657                         }
 658                     }
 659                 }
 660             }
 661           break;
 662         case OPF_MANYOP:
 663           {
 664             cstring s = ltoken_getRawString (opf->content.anyop);
 665
 666             if (isStateOperator (s))
 667               {
 668                 if (sortSetList_size (argSorts) == 1)
 669                   {
 670                     sortSetList_reset (argSorts);
 671
 672                     argSet = sortSetList_current (argSorts);
 673
 674                     sortSet_elements (argSet, current)
 675                       {
 676                         sortNode sn;
 677
 678                         sn = sort_quietLookup (current);
 679
 680                         while (sn->kind == SRT_SYN)
 681                           {
 682                             sn = sort_quietLookup (sn->baseSort);
 683                           }
 684
 685                         switch (sn->kind)
 686                           {
 687                           case SRT_OBJ:
 688                             (void) sortSet_insert (ret, sn->baseSort);
 689                             break;
 690                           case SRT_ARRAY:
 691                             (void) sortSet_insert (ret,
 692                                                    sort_makeVec (ltoken_undefined, current));
 693                             break;
 694                           case SRT_STRUCT:
 695                             (void) sortSet_insert (ret,
 696                                                    sort_makeTuple (ltoken_undefined, current));
 697                             break;
 698                           case SRT_UNION:
 699                             (void) sortSet_insert (ret,
 700                                                    sort_makeUnionVal (ltoken_undefined, current));
 701                             break;
 702                           case SRT_TUPLE:
 703                           case SRT_UNIONVAL:
 704                           case SRT_ENUM:
 705                           case SRT_LAST:
 706                           case SRT_FIRST:
 707                           case SRT_NONE:
 708                           case SRT_HOF:
 709                           case SRT_PRIM:
 710                           case SRT_PTR:
 711                           case SRT_VECTOR:
 712                             break;
 713                           case SRT_SYN:
 714                             llbuglit ("standardOperators: Synonym in switch");
 715                           }
 716                       } end_sortSet_elements ;
 717                   }
 718               }
 719           }
 720           break;
 721         case OPF_ANYOPM:
 722           /* operator: *__ */
 723           {
 724             cstring s = ltoken_getRawString (opf->content.anyop);
 725
 726             if (isDeRefOperator (s))
 727               {
 728                 if (sortSetList_size (argSorts) == 1)
 729                   {
 730                     sortSetList_reset (argSorts);
 731
 732                     argSet = sortSetList_current (argSorts);
 733
 734                     sortSet_elements (argSet, current)
 735                       {
 736                         sortNode sn;
 737
 738                         sn = sort_quietLookup (current);
 739
 740                         while (sn->kind == SRT_SYN)
 741                           {
 742                             sn = sort_quietLookup (sn->baseSort);
 743                           }
 744
 745                         if (sn->kind == SRT_PTR)
 746                           {
 747                             (void) sortSet_insert (ret, sn->baseSort);
 748                           }
 749                       } end_sortSet_elements;
 750                   }
 751               }
 752           }
 753           break;
 754         case OPF_ANYOP:
 755           break;
 756         case OPF_MANYOPM:
 757           {
 758             cstring s = ltoken_getRawString (opf->content.anyop);
 759
 760             if (isCompareOperator (s))
 761               {
 762                 if (sortSetList_size (argSorts) == 2)
 763                   {
 764                     sortSet argSet2;
 765
 766                     sortSetList_reset (argSorts);
 767
 768                     argSet = sortSetList_current (argSorts);
 769                     sortSetList_advance (argSorts);
 770                     argSet2 = sortSetList_current (argSorts);
 771
 772                     if (sortSet_size (argSet) == 1)
 773                       {
 774                         sortSet_elements (argSet, cl)
 775                           {
 776                             sortSet_elements (argSet2, cl2)
 777                               {
 778                                 if (sort_equal (cl, cl2))
 779                                   {
 780                                     (void) sortSet_insert (ret, g_sortBool);
 781                                   }
 782                               } end_sortSet_elements;
 783                           } end_sortSet_elements;
 784                       }
 785                   }
 786               }
 787           }
 788           break;
 789         case OPF_MIDDLE:
 790           break;
 791         case OPF_MMIDDLE:
 792           break;
 793         case OPF_MIDDLEM:
 794           break;
 795         case OPF_MMIDDLEM:
 796           break;
 797         case OPF_BMIDDLE:
 798           break;
 799         case OPF_BMMIDDLE:
 800           break;
 801         case OPF_BMIDDLEM:
 802           break;
 803         case OPF_BMMIDDLEM:
 804           break;
 805         case OPF_SELECT:
 806           break;
 807         case OPF_MAP:
 808           break;
 809         case OPF_MSELECT:
 810           break;
 811         case OPF_MMAP:
 812           break;
 813         default:
 814           break;
 815         }
 816       /*@=loopswitchbreak@*/
 817     }
 818   return ret;
 819 }