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