verif/md/pan.b

   1         switch (t->back) {
   2         default: Uerror("bad return move");
   3         case  0: goto R999; /* nothing to undo */
   4
   5                  /* PROC :never: */
   6 ;
   7                 ;
   8                 ;
   9                 ;
  10                 ;
  11                 ;
  12
  13         case 6: /* STATE 14 */
  14                 ;
  15                 p_restor(II);
  16                 ;
  17                 ;
  18                 goto R999;
  19
  20                  /* PROC :init: */
  21
  22         case 7: /* STATE 1 */
  23                 ;
  24                 ((P4 *)this)->i = trpt->bup.oval;
  25                 ;
  26                 goto R999;
  27
  28         case 8: /* STATE 4 */
  29                 ;
  30                 ((P4 *)this)->i = trpt->bup.ovals[1];
  31                 now.commit_count[ Index(((P4 *)this)->i, 2) ] = trpt->bup.ovals[0];
  32                 ;
  33                 ungrab_ints(trpt->bup.ovals, 2);
  34                 goto R999;
  35
  36         case 9: /* STATE 11 */
  37                 ;
  38                 ((P4 *)this)->i = trpt->bup.ovals[2];
  39                 now._commit_sum = trpt->bup.ovals[1];
  40         /* 0 */ ((P4 *)this)->i = trpt->bup.ovals[0];
  41                 ;
  42                 ;
  43                 ungrab_ints(trpt->bup.ovals, 3);
  44                 goto R999;
  45
  46         case 10: /* STATE 11 */
  47                 ;
  48                 ((P4 *)this)->i = trpt->bup.ovals[1];
  49                 now._commit_sum = trpt->bup.ovals[0];
  50                 ;
  51                 ungrab_ints(trpt->bup.ovals, 2);
  52                 goto R999;
  53
  54         case 11: /* STATE 14 */
  55                 ;
  56                 ((P4 *)this)->i = trpt->bup.ovals[1];
  57                 now.buffer_use[ Index(((P4 *)this)->i, 4) ] = trpt->bup.ovals[0];
  58                 ;
  59                 ungrab_ints(trpt->bup.ovals, 2);
  60                 goto R999;
  61
  62         case 12: /* STATE 15 */
  63                 ;
  64         /* 0 */ ((P4 *)this)->i = trpt->bup.oval;
  65                 ;
  66                 ;
  67                 goto R999;
  68
  69         case 13: /* STATE 20 */
  70                 ;
  71                 ;
  72                 delproc(0, now._nr_pr-1);
  73                 ;
  74                 goto R999;
  75
  76         case 14: /* STATE 22 */
  77                 ;
  78                 ((P4 *)this)->i = trpt->bup.oval;
  79                 ;
  80                 delproc(0, now._nr_pr-1);
  81                 ;
  82                 goto R999;
  83
  84         case 15: /* STATE 24 */
  85                 ;
  86                 now.refcount = trpt->bup.oval;
  87                 ;
  88                 goto R999;
  89
  90         case 16: /* STATE 26 */
  91                 ;
  92                 ((P4 *)this)->i = trpt->bup.oval;
  93                 ;
  94                 delproc(0, now._nr_pr-1);
  95                 ;
  96                 goto R999;
  97
  98         case 17: /* STATE 32 */
  99                 ;
 100                 ((P4 *)this)->i = trpt->bup.ovals[1];
 101         /* 0 */ ((P4 *)this)->i = trpt->bup.ovals[0];
 102                 ;
 103                 ;
 104                 ungrab_ints(trpt->bup.ovals, 2);
 105                 goto R999;
 106
 107         case 18: /* STATE 32 */
 108                 ;
 109                 ((P4 *)this)->i = trpt->bup.oval;
 110                 ;
 111                 goto R999;
 112
 113         case 19: /* STATE 34 */
 114                 ;
 115                 now.refcount = trpt->bup.oval;
 116                 ;
 117                 goto R999;
 118
 119         case 20: /* STATE 36 */
 120                 ;
 121                 ((P4 *)this)->i = trpt->bup.oval;
 122                 ;
 123                 delproc(0, now._nr_pr-1);
 124                 ;
 125                 goto R999;
 126
 127         case 21: /* STATE 37 */
 128                 ;
 129         /* 0 */ ((P4 *)this)->i = trpt->bup.oval;
 130                 ;
 131                 ;
 132                 goto R999;
 133
 134         case 22: /* STATE 43 */
 135                 ;
 136                 p_restor(II);
 137                 ;
 138                 ;
 139                 goto R999;
 140
 141                  /* PROC cleaner */
 142
 143         case 23: /* STATE 2 */
 144                 ;
 145                 now.refcount = trpt->bup.oval;
 146                 ;
 147                 goto R999;
 148
 149         case 24: /* STATE 3 */
 150                 ;
 151                 ;
 152                 delproc(0, now._nr_pr-1);
 153                 ;
 154                 goto R999;
 155
 156         case 25: /* STATE 9 */
 157                 ;
 158                 p_restor(II);
 159                 ;
 160                 ;
 161                 goto R999;
 162
 163                  /* PROC reader */
 164 ;
 165                 ;
 166
 167         case 27: /* STATE 2 */
 168                 ;
 169                 ((P2 *)this)->i = trpt->bup.oval;
 170                 ;
 171                 goto R999;
 172
 173         case 28: /* STATE 6 */
 174                 ;
 175                 ((P2 *)this)->i = trpt->bup.ovals[1];
 176                 now.buffer_use[ Index(((now.read_off+((P2 *)this)->i)%4), 4) ] = trpt->bup.ovals[0];
 177                 ;
 178                 ungrab_ints(trpt->bup.ovals, 2);
 179                 goto R999;
 180
 181         case 29: /* STATE 7 */
 182                 ;
 183         /* 0 */ ((P2 *)this)->i = trpt->bup.oval;
 184                 ;
 185                 ;
 186                 goto R999;
 187
 188         case 30: /* STATE 16 */
 189                 ;
 190                 ((P2 *)this)->i = trpt->bup.ovals[1];
 191                 now.buffer_use[ Index(((now.read_off+((P2 *)this)->i)%4), 4) ] = trpt->bup.ovals[0];
 192                 ;
 193                 ungrab_ints(trpt->bup.ovals, 2);
 194                 goto R999;
 195
 196         case 31: /* STATE 17 */
 197                 ;
 198         /* 0 */ ((P2 *)this)->i = trpt->bup.oval;
 199                 ;
 200                 ;
 201                 goto R999;
 202
 203         case 32: /* STATE 22 */
 204                 ;
 205                 now.read_off = trpt->bup.oval;
 206                 ;
 207                 goto R999;
 208 ;
 209                 ;
 210
 211         case 34: /* STATE 29 */
 212                 ;
 213                 p_restor(II);
 214                 ;
 215                 ;
 216                 goto R999;
 217
 218                  /* PROC tracer */
 219
 220         case 35: /* STATE 2 */
 221                 ;
 222                 ((P1 *)this)->new_off = trpt->bup.ovals[1];
 223                 ((P1 *)this)->prev_off = trpt->bup.ovals[0];
 224                 ;
 225                 ungrab_ints(trpt->bup.ovals, 2);
 226                 goto R999;
 227
 228         case 36: /* STATE 4 */
 229                 ;
 230         /* 0 */ ((P1 *)this)->new_off = trpt->bup.oval;
 231                 ;
 232                 ;
 233                 goto R999;
 234 ;
 235
 236         case 37: /* STATE 7 */
 237                 goto R999;
 238
 239         case 38: /* STATE 11 */
 240                 ;
 241         /* 0 */ ((P1 *)this)->prev_off = trpt->bup.oval;
 242                 ;
 243                 ;
 244                 goto R999;
 245
 246         case 39: /* STATE 17 */
 247                 ;
 248                 ((P1 *)this)->i = trpt->bup.ovals[1];
 249                 now.write_off = trpt->bup.ovals[0];
 250                 ;
 251                 ungrab_ints(trpt->bup.ovals, 2);
 252                 goto R999;
 253
 254         case 40: /* STATE 17 */
 255                 ;
 256                 ((P1 *)this)->i = trpt->bup.oval;
 257                 ;
 258                 goto R999;
 259
 260         case 41: /* STATE 21 */
 261                 ;
 262                 ((P1 *)this)->i = trpt->bup.ovals[1];
 263                 now.buffer_use[ Index(((((P1 *)this)->prev_off+((P1 *)this)->i)%4), 4) ] = trpt->bup.ovals[0];
 264                 ;
 265                 ungrab_ints(trpt->bup.ovals, 2);
 266                 goto R999;
 267
 268         case 42: /* STATE 22 */
 269                 ;
 270         /* 0 */ ((P1 *)this)->i = trpt->bup.oval;
 271                 ;
 272                 ;
 273                 goto R999;
 274
 275         case 43: /* STATE 28 */
 276                 ;
 277                 ((P1 *)this)->i = trpt->bup.oval;
 278                 ;
 279                 goto R999;
 280
 281         case 44: /* STATE 31 */
 282                 ;
 283                 ((P1 *)this)->i = trpt->bup.ovals[1];
 284                 now.buffer_use[ Index(((((P1 *)this)->prev_off+((P1 *)this)->i)%4), 4) ] = trpt->bup.ovals[0];
 285                 ;
 286                 ungrab_ints(trpt->bup.ovals, 2);
 287                 goto R999;
 288
 289         case 45: /* STATE 39 */
 290                 ;
 291                 now.commit_count[ Index(((((P1 *)this)->prev_off%4)/(4/2)), 2) ] = trpt->bup.ovals[3];
 292                 now._commit_sum = trpt->bup.ovals[2];
 293                 ((P1 *)this)->tmp_commit = trpt->bup.ovals[1];
 294         /* 0 */ ((P1 *)this)->i = trpt->bup.ovals[0];
 295                 ;
 296                 ;
 297                 ungrab_ints(trpt->bup.ovals, 4);
 298                 goto R999;
 299
 300         case 46: /* STATE 39 */
 301                 ;
 302                 now.commit_count[ Index(((((P1 *)this)->prev_off%4)/(4/2)), 2) ] = trpt->bup.ovals[2];
 303                 now._commit_sum = trpt->bup.ovals[1];
 304                 ((P1 *)this)->tmp_commit = trpt->bup.ovals[0];
 305                 ;
 306                 ungrab_ints(trpt->bup.ovals, 3);
 307                 goto R999;
 308
 309         case 47: /* STATE 41 */
 310                 ;
 311                 deliver = trpt->bup.ovals[2];
 312         /* 1 */ ((P1 *)this)->tmp_commit = trpt->bup.ovals[1];
 313         /* 0 */ ((P1 *)this)->prev_off = trpt->bup.ovals[0];
 314                 ;
 315                 ;
 316                 ungrab_ints(trpt->bup.ovals, 3);
 317                 goto R999;
 318 ;
 319
 320         case 48: /* STATE 45 */
 321                 goto R999;
 322 ;
 323
 324         case 49: /* STATE 43 */
 325                 goto R999;
 326
 327         case 50: /* STATE 48 */
 328                 ;
 329                 now.events_lost = trpt->bup.oval;
 330                 ;
 331                 goto R999;
 332
 333         case 51: /* STATE 49 */
 334                 ;
 335                 now.refcount = trpt->bup.oval;
 336                 ;
 337                 goto R999;
 338
 339         case 52: /* STATE 51 */
 340                 ;
 341                 p_restor(II);
 342                 ;
 343                 ;
 344                 goto R999;
 345
 346                  /* PROC switcher */
 347
 348         case 53: /* STATE 3 */
 349                 ;
 350                 ((P0 *)this)->new_off = trpt->bup.ovals[2];
 351                 ((P0 *)this)->size = trpt->bup.ovals[1];
 352                 ((P0 *)this)->prev_off = trpt->bup.ovals[0];
 353                 ;
 354                 ungrab_ints(trpt->bup.ovals, 3);
 355                 goto R999;
 356
 357         case 54: /* STATE 5 */
 358                 ;
 359                 now.refcount = trpt->bup.ovals[2];
 360         /* 1 */ ((P0 *)this)->size = trpt->bup.ovals[1];
 361         /* 0 */ ((P0 *)this)->new_off = trpt->bup.ovals[0];
 362                 ;
 363                 ;
 364                 ungrab_ints(trpt->bup.ovals, 3);
 365                 goto R999;
 366 ;
 367
 368         case 55: /* STATE 8 */
 369                 goto R999;
 370
 371         case 56: /* STATE 12 */
 372                 ;
 373         /* 0 */ ((P0 *)this)->prev_off = trpt->bup.oval;
 374                 ;
 375                 ;
 376                 goto R999;
 377 ;
 378
 379         case 57: /* STATE 17 */
 380                 goto R999;
 381
 382         case 58: /* STATE 15 */
 383                 ;
 384                 now.write_off = trpt->bup.oval;
 385                 ;
 386                 goto R999;
 387
 388         case 59: /* STATE 21 */
 389                 ;
 390                 now.commit_count[ Index(((((P0 *)this)->prev_off%4)/(4/2)), 2) ] = trpt->bup.ovals[2];
 391                 now._commit_sum = trpt->bup.ovals[1];
 392                 ((P0 *)this)->tmp_commit = trpt->bup.ovals[0];
 393                 ;
 394                 ungrab_ints(trpt->bup.ovals, 3);
 395                 goto R999;
 396
 397         case 60: /* STATE 28 */
 398                 ;
 399                 now.refcount = trpt->bup.ovals[3];
 400                 deliver = trpt->bup.ovals[2];
 401         /* 1 */ ((P0 *)this)->tmp_commit = trpt->bup.ovals[1];
 402         /* 0 */ ((P0 *)this)->prev_off = trpt->bup.ovals[0];
 403                 ;
 404                 ;
 405                 ungrab_ints(trpt->bup.ovals, 4);
 406                 goto R999;
 407
 408         case 61: /* STATE 28 */
 409                 ;
 410                 now.refcount = trpt->bup.oval;
 411                 ;
 412                 goto R999;
 413
 414         case 62: /* STATE 28 */
 415                 ;
 416                 now.refcount = trpt->bup.oval;
 417                 ;
 418                 goto R999;
 419
 420         case 63: /* STATE 31 */
 421                 ;
 422                 p_restor(II);
 423                 ;
 424                 ;
 425                 goto R999;
 426         }
 427