verif/nico-md-merge/pan.m

   1 #define rand    pan_rand
   2 #if defined(HAS_CODE) && defined(VERBOSE)
   3         cpu_printf("Pr: %d Tr: %d\n", II, t->forw);
   4 #endif
   5         switch (t->forw) {
   6         default: Uerror("bad forward move");
   7         case 0: /* if without executable clauses */
   8                 continue;
   9         case 1: /* generic 'goto' or 'skip' */
  10                 IfNotBlocked
  11                 _m = 3; goto P999;
  12         case 2: /* generic 'else' */
  13                 IfNotBlocked
  14                 if (trpt->o_pm&1) continue;
  15                 _m = 3; goto P999;
  16
  17                  /* PROC :never: */
  18         case 3: /* STATE 1 - line 304 "pan.___" - [((((4+1)<=8)&&(events_lost!=0)))] (0:0:0 - 1) */
  19
  20 #if defined(VERI) && !defined(NP)
  21                 {       static int reported1 = 0;
  22                         if (verbose && !reported1)
  23                         {       printf("depth %d: Claim reached state %d (line %d)\n",
  24                                         depth, frm_st0[t->forw], src_claim[1]);
  25                                 reported1 = 1;
  26                                 fflush(stdout);
  27                 }       }
  28 #endif
  29                 reached[5][1] = 1;
  30                 if (!((((4+1)<=8)&&(((int)now.events_lost)!=0))))
  31                         continue;
  32                 _m = 3; goto P999; /* 0 */
  33         case 4: /* STATE 8 - line 309 "pan.___" - [-end-] (0:0:0 - 1) */
  34
  35 #if defined(VERI) && !defined(NP)
  36                 {       static int reported8 = 0;
  37                         if (verbose && !reported8)
  38                         {       printf("depth %d: Claim reached state %d (line %d)\n",
  39                                         depth, frm_st0[t->forw], src_claim[8]);
  40                                 reported8 = 1;
  41                                 fflush(stdout);
  42                 }       }
  43 #endif
  44                 reached[5][8] = 1;
  45                 if (!delproc(1, II)) continue;
  46                 _m = 3; goto P999; /* 0 */
  47
  48                  /* PROC :init: */
  49         case 5: /* STATE 1 - line 255 "pan.___" - [i = 0] (0:0:1 - 1) */
  50                 IfNotBlocked
  51                 reached[4][1] = 1;
  52                 (trpt+1)->bup.oval = ((int)((P4 *)this)->i);
  53                 ((P4 *)this)->i = 0;
  54 #ifdef VAR_RANGES
  55                 logval(":init::i", ((int)((P4 *)this)->i));
  56 #endif
  57                 ;
  58                 _m = 3; goto P999; /* 0 */
  59         case 6: /* STATE 2 - line 257 "pan.___" - [((i<2))] (7:0:2 - 1) */
  60                 IfNotBlocked
  61                 reached[4][2] = 1;
  62                 if (!((((int)((P4 *)this)->i)<2)))
  63                         continue;
  64                 /* merge: commit_count[i] = 0(7, 3, 7) */
  65                 reached[4][3] = 1;
  66                 (trpt+1)->bup.ovals = grab_ints(2);
  67                 (trpt+1)->bup.ovals[0] = ((int)now.commit_count[ Index(((int)((P4 *)this)->i), 2) ]);
  68                 now.commit_count[ Index(((P4 *)this)->i, 2) ] = 0;
  69 #ifdef VAR_RANGES
  70                 logval("commit_count[:init::i]", ((int)now.commit_count[ Index(((int)((P4 *)this)->i), 2) ]));
  71 #endif
  72                 ;
  73                 /* merge: i = (i+1)(7, 4, 7) */
  74                 reached[4][4] = 1;
  75                 (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i);
  76                 ((P4 *)this)->i = (((int)((P4 *)this)->i)+1);
  77 #ifdef VAR_RANGES
  78                 logval(":init::i", ((int)((P4 *)this)->i));
  79 #endif
  80                 ;
  81                 /* merge: .(goto)(0, 8, 7) */
  82                 reached[4][8] = 1;
  83                 ;
  84                 _m = 3; goto P999; /* 3 */
  85         case 7: /* STATE 5 - line 260 "pan.___" - [((i>=2))] (17:0:3 - 1) */
  86                 IfNotBlocked
  87                 reached[4][5] = 1;
  88                 if (!((((int)((P4 *)this)->i)>=2)))
  89                         continue;
  90                 /* dead 1: i */  (trpt+1)->bup.ovals = grab_ints(3);
  91                 (trpt+1)->bup.ovals[0] = ((P4 *)this)->i;
  92 #ifdef HAS_CODE
  93                 if (!readtrail)
  94 #endif
  95                         ((P4 *)this)->i = 0;
  96                 /* merge: goto :b6(17, 6, 17) */
  97                 reached[4][6] = 1;
  98                 ;
  99                 /* merge: _commit_sum = 0(17, 10, 17) */
 100                 reached[4][10] = 1;
 101                 (trpt+1)->bup.ovals[1] = ((int)now._commit_sum);
 102                 now._commit_sum = 0;
 103 #ifdef VAR_RANGES
 104                 logval("_commit_sum", ((int)now._commit_sum));
 105 #endif
 106                 ;
 107                 /* merge: i = 0(17, 11, 17) */
 108                 reached[4][11] = 1;
 109                 (trpt+1)->bup.ovals[2] = ((int)((P4 *)this)->i);
 110                 ((P4 *)this)->i = 0;
 111 #ifdef VAR_RANGES
 112                 logval(":init::i", ((int)((P4 *)this)->i));
 113 #endif
 114                 ;
 115                 /* merge: .(goto)(0, 18, 17) */
 116                 reached[4][18] = 1;
 117                 ;
 118                 _m = 3; goto P999; /* 4 */
 119         case 8: /* STATE 10 - line 263 "pan.___" - [_commit_sum = 0] (0:17:2 - 3) */
 120                 IfNotBlocked
 121                 reached[4][10] = 1;
 122                 (trpt+1)->bup.ovals = grab_ints(2);
 123                 (trpt+1)->bup.ovals[0] = ((int)now._commit_sum);
 124                 now._commit_sum = 0;
 125 #ifdef VAR_RANGES
 126                 logval("_commit_sum", ((int)now._commit_sum));
 127 #endif
 128                 ;
 129                 /* merge: i = 0(17, 11, 17) */
 130                 reached[4][11] = 1;
 131                 (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i);
 132                 ((P4 *)this)->i = 0;
 133 #ifdef VAR_RANGES
 134                 logval(":init::i", ((int)((P4 *)this)->i));
 135 #endif
 136                 ;
 137                 /* merge: .(goto)(0, 18, 17) */
 138                 reached[4][18] = 1;
 139                 ;
 140                 _m = 3; goto P999; /* 2 */
 141         case 9: /* STATE 12 - line 267 "pan.___" - [((i<8))] (17:0:2 - 1) */
 142                 IfNotBlocked
 143                 reached[4][12] = 1;
 144                 if (!((((int)((P4 *)this)->i)<8)))
 145                         continue;
 146                 /* merge: buffer_use[i] = 0(17, 13, 17) */
 147                 reached[4][13] = 1;
 148                 (trpt+1)->bup.ovals = grab_ints(2);
 149                 (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((int)((P4 *)this)->i), 8) ]);
 150                 now.buffer_use[ Index(((P4 *)this)->i, 8) ] = 0;
 151 #ifdef VAR_RANGES
 152                 logval("buffer_use[:init::i]", ((int)now.buffer_use[ Index(((int)((P4 *)this)->i), 8) ]));
 153 #endif
 154                 ;
 155                 /* merge: i = (i+1)(17, 14, 17) */
 156                 reached[4][14] = 1;
 157                 (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i);
 158                 ((P4 *)this)->i = (((int)((P4 *)this)->i)+1);
 159 #ifdef VAR_RANGES
 160                 logval(":init::i", ((int)((P4 *)this)->i));
 161 #endif
 162                 ;
 163                 /* merge: .(goto)(0, 18, 17) */
 164                 reached[4][18] = 1;
 165                 ;
 166                 _m = 3; goto P999; /* 3 */
 167         case 10: /* STATE 15 - line 270 "pan.___" - [((i>=8))] (0:0:1 - 1) */
 168                 IfNotBlocked
 169                 reached[4][15] = 1;
 170                 if (!((((int)((P4 *)this)->i)>=8)))
 171                         continue;
 172                 /* dead 1: i */  (trpt+1)->bup.oval = ((P4 *)this)->i;
 173 #ifdef HAS_CODE
 174                 if (!readtrail)
 175 #endif
 176                         ((P4 *)this)->i = 0;
 177                 _m = 3; goto P999; /* 0 */
 178         case 11: /* STATE 20 - line 272 "pan.___" - [(run reader())] (0:0:0 - 3) */
 179                 IfNotBlocked
 180                 reached[4][20] = 1;
 181                 if (!(addproc(2)))
 182                         continue;
 183                 _m = 3; goto P999; /* 0 */
 184         case 12: /* STATE 21 - line 273 "pan.___" - [(run cleaner())] (29:0:1 - 1) */
 185                 IfNotBlocked
 186                 reached[4][21] = 1;
 187                 if (!(addproc(3)))
 188                         continue;
 189                 /* merge: i = 0(0, 22, 29) */
 190                 reached[4][22] = 1;
 191                 (trpt+1)->bup.oval = ((int)((P4 *)this)->i);
 192                 ((P4 *)this)->i = 0;
 193 #ifdef VAR_RANGES
 194                 logval(":init::i", ((int)((P4 *)this)->i));
 195 #endif
 196                 ;
 197                 /* merge: .(goto)(0, 30, 29) */
 198                 reached[4][30] = 1;
 199                 ;
 200                 _m = 3; goto P999; /* 2 */
 201         case 13: /* STATE 23 - line 276 "pan.___" - [((i<4))] (25:0:1 - 1) */
 202                 IfNotBlocked
 203                 reached[4][23] = 1;
 204                 if (!((((int)((P4 *)this)->i)<4)))
 205                         continue;
 206                 /* merge: refcount = (refcount+1)(0, 24, 25) */
 207                 reached[4][24] = 1;
 208                 (trpt+1)->bup.oval = ((int)now.refcount);
 209                 now.refcount = (((int)now.refcount)+1);
 210 #ifdef VAR_RANGES
 211                 logval("refcount", ((int)now.refcount));
 212 #endif
 213                 ;
 214                 _m = 3; goto P999; /* 1 */
 215         case 14: /* STATE 25 - line 278 "pan.___" - [(run tracer())] (29:0:1 - 1) */
 216                 IfNotBlocked
 217                 reached[4][25] = 1;
 218                 if (!(addproc(1)))
 219                         continue;
 220                 /* merge: i = (i+1)(0, 26, 29) */
 221                 reached[4][26] = 1;
 222                 (trpt+1)->bup.oval = ((int)((P4 *)this)->i);
 223                 ((P4 *)this)->i = (((int)((P4 *)this)->i)+1);
 224 #ifdef VAR_RANGES
 225                 logval(":init::i", ((int)((P4 *)this)->i));
 226 #endif
 227                 ;
 228                 /* merge: .(goto)(0, 30, 29) */
 229                 reached[4][30] = 1;
 230                 ;
 231                 _m = 3; goto P999; /* 2 */
 232         case 15: /* STATE 27 - line 280 "pan.___" - [((i>=4))] (39:0:2 - 1) */
 233                 IfNotBlocked
 234                 reached[4][27] = 1;
 235                 if (!((((int)((P4 *)this)->i)>=4)))
 236                         continue;
 237                 /* dead 1: i */  (trpt+1)->bup.ovals = grab_ints(2);
 238                 (trpt+1)->bup.ovals[0] = ((P4 *)this)->i;
 239 #ifdef HAS_CODE
 240                 if (!readtrail)
 241 #endif
 242                         ((P4 *)this)->i = 0;
 243                 /* merge: goto :b8(39, 28, 39) */
 244                 reached[4][28] = 1;
 245                 ;
 246                 /* merge: i = 0(39, 32, 39) */
 247                 reached[4][32] = 1;
 248                 (trpt+1)->bup.ovals[1] = ((int)((P4 *)this)->i);
 249                 ((P4 *)this)->i = 0;
 250 #ifdef VAR_RANGES
 251                 logval(":init::i", ((int)((P4 *)this)->i));
 252 #endif
 253                 ;
 254                 /* merge: .(goto)(0, 40, 39) */
 255                 reached[4][40] = 1;
 256                 ;
 257                 _m = 3; goto P999; /* 3 */
 258         case 16: /* STATE 32 - line 282 "pan.___" - [i = 0] (0:39:1 - 3) */
 259                 IfNotBlocked
 260                 reached[4][32] = 1;
 261                 (trpt+1)->bup.oval = ((int)((P4 *)this)->i);
 262                 ((P4 *)this)->i = 0;
 263 #ifdef VAR_RANGES
 264                 logval(":init::i", ((int)((P4 *)this)->i));
 265 #endif
 266                 ;
 267                 /* merge: .(goto)(0, 40, 39) */
 268                 reached[4][40] = 1;
 269                 ;
 270                 _m = 3; goto P999; /* 1 */
 271         case 17: /* STATE 33 - line 284 "pan.___" - [((i<1))] (35:0:1 - 1) */
 272                 IfNotBlocked
 273                 reached[4][33] = 1;
 274                 if (!((((int)((P4 *)this)->i)<1)))
 275                         continue;
 276                 /* merge: refcount = (refcount+1)(0, 34, 35) */
 277                 reached[4][34] = 1;
 278                 (trpt+1)->bup.oval = ((int)now.refcount);
 279                 now.refcount = (((int)now.refcount)+1);
 280 #ifdef VAR_RANGES
 281                 logval("refcount", ((int)now.refcount));
 282 #endif
 283                 ;
 284                 _m = 3; goto P999; /* 1 */
 285         case 18: /* STATE 35 - line 286 "pan.___" - [(run switcher())] (39:0:1 - 1) */
 286                 IfNotBlocked
 287                 reached[4][35] = 1;
 288                 if (!(addproc(0)))
 289                         continue;
 290                 /* merge: i = (i+1)(0, 36, 39) */
 291                 reached[4][36] = 1;
 292                 (trpt+1)->bup.oval = ((int)((P4 *)this)->i);
 293                 ((P4 *)this)->i = (((int)((P4 *)this)->i)+1);
 294 #ifdef VAR_RANGES
 295                 logval(":init::i", ((int)((P4 *)this)->i));
 296 #endif
 297                 ;
 298                 /* merge: .(goto)(0, 40, 39) */
 299                 reached[4][40] = 1;
 300                 ;
 301                 _m = 3; goto P999; /* 2 */
 302         case 19: /* STATE 37 - line 288 "pan.___" - [((i>=1))] (41:0:1 - 1) */
 303                 IfNotBlocked
 304                 reached[4][37] = 1;
 305                 if (!((((int)((P4 *)this)->i)>=1)))
 306                         continue;
 307                 /* dead 1: i */  (trpt+1)->bup.oval = ((P4 *)this)->i;
 308 #ifdef HAS_CODE
 309                 if (!readtrail)
 310 #endif
 311                         ((P4 *)this)->i = 0;
 312                 /* merge: goto :b9(0, 38, 41) */
 313                 reached[4][38] = 1;
 314                 ;
 315                 _m = 3; goto P999; /* 1 */
 316         case 20: /* STATE 43 - line 291 "pan.___" - [-end-] (0:0:0 - 1) */
 317                 IfNotBlocked
 318                 reached[4][43] = 1;
 319                 if (!delproc(1, II)) continue;
 320                 _m = 3; goto P999; /* 0 */
 321
 322                  /* PROC cleaner */
 323         case 21: /* STATE 1 - line 240 "pan.___" - [((refcount==0))] (3:0:1 - 1) */
 324                 IfNotBlocked
 325                 reached[3][1] = 1;
 326                 if (!((((int)now.refcount)==0)))
 327                         continue;
 328                 /* merge: refcount = (refcount+1)(0, 2, 3) */
 329                 reached[3][2] = 1;
 330                 (trpt+1)->bup.oval = ((int)now.refcount);
 331                 now.refcount = (((int)now.refcount)+1);
 332 #ifdef VAR_RANGES
 333                 logval("refcount", ((int)now.refcount));
 334 #endif
 335                 ;
 336                 _m = 3; goto P999; /* 1 */
 337         case 22: /* STATE 3 - line 242 "pan.___" - [(run switcher())] (7:0:0 - 1) */
 338                 IfNotBlocked
 339                 reached[3][3] = 1;
 340                 if (!(addproc(0)))
 341                         continue;
 342                 /* merge: goto :b5(0, 4, 7) */
 343                 reached[3][4] = 1;
 344                 ;
 345                 _m = 3; goto P999; /* 1 */
 346         case 23: /* STATE 9 - line 246 "pan.___" - [-end-] (0:0:0 - 1) */
 347                 IfNotBlocked
 348                 reached[3][9] = 1;
 349                 if (!delproc(1, II)) continue;
 350                 _m = 3; goto P999; /* 0 */
 351
 352                  /* PROC reader */
 353         case 24: /* STATE 1 - line 203 "pan.___" - [((((((write_off/(8/2))-(read_off/(8/2)))>0)&&(((write_off/(8/2))-(read_off/(8/2)))<(255/2)))&&(((commit_count[((read_off%8)/(8/2))]-(8/2))-(((read_off/8)*8)/2))==0)))] (0:0:0 - 1) */
 354                 IfNotBlocked
 355                 reached[2][1] = 1;
 356                 if (!((((((((int)now.write_off)/(8/2))-(((int)now.read_off)/(8/2)))>0)&&(((((int)now.write_off)/(8/2))-(((int)now.read_off)/(8/2)))<(255/2)))&&(((((int)now.commit_count[ Index(((((int)now.read_off)%8)/(8/2)), 2) ])-(8/2))-(((((int)now.read_off)/8)*8)/2))==0))))
 357                         continue;
 358                 _m = 3; goto P999; /* 0 */
 359         case 25: /* STATE 2 - line 205 "pan.___" - [i = 0] (0:0:1 - 1) */
 360                 IfNotBlocked
 361                 reached[2][2] = 1;
 362                 (trpt+1)->bup.oval = ((int)((P2 *)this)->i);
 363                 ((P2 *)this)->i = 0;
 364 #ifdef VAR_RANGES
 365                 logval("reader:i", ((int)((P2 *)this)->i));
 366 #endif
 367                 ;
 368                 _m = 3; goto P999; /* 0 */
 369         case 26: /* STATE 3 - line 207 "pan.___" - [((i<(8/2)))] (9:0:2 - 1) */
 370                 IfNotBlocked
 371                 reached[2][3] = 1;
 372                 if (!((((int)((P2 *)this)->i)<(8/2))))
 373                         continue;
 374                 /* merge: assert((buffer_use[((read_off+i)%8)]==0))(9, 4, 9) */
 375                 reached[2][4] = 1;
 376                 assert((((int)now.buffer_use[ Index(((((int)now.read_off)+((int)((P2 *)this)->i))%8), 8) ])==0), "(buffer_use[((read_off+i)%8)]==0)", II, tt, t);
 377                 /* merge: buffer_use[((read_off+i)%8)] = 1(9, 5, 9) */
 378                 reached[2][5] = 1;
 379                 (trpt+1)->bup.ovals = grab_ints(2);
 380                 (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((((int)now.read_off)+((int)((P2 *)this)->i))%8), 8) ]);
 381                 now.buffer_use[ Index(((now.read_off+((P2 *)this)->i)%8), 8) ] = 1;
 382 #ifdef VAR_RANGES
 383                 logval("buffer_use[((read_off+reader:i)%8)]", ((int)now.buffer_use[ Index(((((int)now.read_off)+((int)((P2 *)this)->i))%8), 8) ]));
 384 #endif
 385                 ;
 386                 /* merge: i = (i+1)(9, 6, 9) */
 387                 reached[2][6] = 1;
 388                 (trpt+1)->bup.ovals[1] = ((int)((P2 *)this)->i);
 389                 ((P2 *)this)->i = (((int)((P2 *)this)->i)+1);
 390 #ifdef VAR_RANGES
 391                 logval("reader:i", ((int)((P2 *)this)->i));
 392 #endif
 393                 ;
 394                 /* merge: .(goto)(0, 10, 9) */
 395                 reached[2][10] = 1;
 396                 ;
 397                 _m = 3; goto P999; /* 4 */
 398         case 27: /* STATE 7 - line 211 "pan.___" - [((i>=(8/2)))] (11:0:1 - 1) */
 399                 IfNotBlocked
 400                 reached[2][7] = 1;
 401                 if (!((((int)((P2 *)this)->i)>=(8/2))))
 402                         continue;
 403                 /* dead 1: i */  (trpt+1)->bup.oval = ((P2 *)this)->i;
 404 #ifdef HAS_CODE
 405                 if (!readtrail)
 406 #endif
 407                         ((P2 *)this)->i = 0;
 408                 /* merge: goto :b3(0, 8, 11) */
 409                 reached[2][8] = 1;
 410                 ;
 411                 _m = 3; goto P999; /* 1 */
 412 /* STATE 13 - line 219 "pan.___" - [i = 0] (0:0 - 1) same as 25 (0:0 - 1) */
 413         case 28: /* STATE 14 - line 221 "pan.___" - [((i<(8/2)))] (19:0:2 - 1) */
 414                 IfNotBlocked
 415                 reached[2][14] = 1;
 416                 if (!((((int)((P2 *)this)->i)<(8/2))))
 417                         continue;
 418                 /* merge: buffer_use[((read_off+i)%8)] = 0(19, 15, 19) */
 419                 reached[2][15] = 1;
 420                 (trpt+1)->bup.ovals = grab_ints(2);
 421                 (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((((int)now.read_off)+((int)((P2 *)this)->i))%8), 8) ]);
 422                 now.buffer_use[ Index(((now.read_off+((P2 *)this)->i)%8), 8) ] = 0;
 423 #ifdef VAR_RANGES
 424                 logval("buffer_use[((read_off+reader:i)%8)]", ((int)now.buffer_use[ Index(((((int)now.read_off)+((int)((P2 *)this)->i))%8), 8) ]));
 425 #endif
 426                 ;
 427                 /* merge: i = (i+1)(19, 16, 19) */
 428                 reached[2][16] = 1;
 429                 (trpt+1)->bup.ovals[1] = ((int)((P2 *)this)->i);
 430                 ((P2 *)this)->i = (((int)((P2 *)this)->i)+1);
 431 #ifdef VAR_RANGES
 432                 logval("reader:i", ((int)((P2 *)this)->i));
 433 #endif
 434                 ;
 435                 /* merge: .(goto)(0, 20, 19) */
 436                 reached[2][20] = 1;
 437                 ;
 438                 _m = 3; goto P999; /* 3 */
 439         case 29: /* STATE 17 - line 224 "pan.___" - [((i>=(8/2)))] (0:0:1 - 1) */
 440                 IfNotBlocked
 441                 reached[2][17] = 1;
 442                 if (!((((int)((P2 *)this)->i)>=(8/2))))
 443                         continue;
 444                 /* dead 1: i */  (trpt+1)->bup.oval = ((P2 *)this)->i;
 445 #ifdef HAS_CODE
 446                 if (!readtrail)
 447 #endif
 448                         ((P2 *)this)->i = 0;
 449                 _m = 3; goto P999; /* 0 */
 450         case 30: /* STATE 22 - line 226 "pan.___" - [read_off = (read_off+(8/2))] (0:0:1 - 1) */
 451                 IfNotBlocked
 452                 reached[2][22] = 1;
 453                 (trpt+1)->bup.oval = ((int)now.read_off);
 454                 now.read_off = (((int)now.read_off)+(8/2));
 455 #ifdef VAR_RANGES
 456                 logval("read_off", ((int)now.read_off));
 457 #endif
 458                 ;
 459                 _m = 3; goto P999; /* 0 */
 460         case 31: /* STATE 24 - line 228 "pan.___" - [((read_off>=(4-events_lost)))] (0:0:0 - 1) */
 461                 IfNotBlocked
 462                 reached[2][24] = 1;
 463                 if (!((((int)now.read_off)>=(4-((int)now.events_lost)))))
 464                         continue;
 465                 _m = 3; goto P999; /* 0 */
 466         case 32: /* STATE 29 - line 230 "pan.___" - [-end-] (0:0:0 - 3) */
 467                 IfNotBlocked
 468                 reached[2][29] = 1;
 469                 if (!delproc(1, II)) continue;
 470                 _m = 3; goto P999; /* 0 */
 471
 472                  /* PROC tracer */
 473         case 33: /* STATE 1 - line 126 "pan.___" - [prev_off = write_off] (0:10:2 - 1) */
 474                 IfNotBlocked
 475                 reached[1][1] = 1;
 476                 (trpt+1)->bup.ovals = grab_ints(2);
 477                 (trpt+1)->bup.ovals[0] = ((int)((P1 *)this)->prev_off);
 478                 ((P1 *)this)->prev_off = ((int)now.write_off);
 479 #ifdef VAR_RANGES
 480                 logval("tracer:prev_off", ((int)((P1 *)this)->prev_off));
 481 #endif
 482                 ;
 483                 /* merge: new_off = (prev_off+size)(10, 2, 10) */
 484                 reached[1][2] = 1;
 485                 (trpt+1)->bup.ovals[1] = ((int)((P1 *)this)->new_off);
 486                 ((P1 *)this)->new_off = (((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->size));
 487 #ifdef VAR_RANGES
 488                 logval("tracer:new_off", ((int)((P1 *)this)->new_off));
 489 #endif
 490                 ;
 491                 _m = 3; goto P999; /* 1 */
 492         case 34: /* STATE 4 - line 131 "pan.___" - [((((new_off-read_off)>8)&&((new_off-read_off)<(255/2))))] (0:0:1 - 1) */
 493                 IfNotBlocked
 494                 reached[1][4] = 1;
 495                 if (!((((((int)((P1 *)this)->new_off)-((int)now.read_off))>8)&&((((int)((P1 *)this)->new_off)-((int)now.read_off))<(255/2)))))
 496                         continue;
 497                 /* dead 1: new_off */  (trpt+1)->bup.oval = ((P1 *)this)->new_off;
 498 #ifdef HAS_CODE
 499                 if (!readtrail)
 500 #endif
 501                         ((P1 *)this)->new_off = 0;
 502                 _m = 3; goto P999; /* 0 */
 503         case 35: /* STATE 7 - line 133 "pan.___" - [(1)] (27:0:0 - 1) */
 504                 IfNotBlocked
 505                 reached[1][7] = 1;
 506                 if (!(1))
 507                         continue;
 508                 /* merge: .(goto)(0, 9, 27) */
 509                 reached[1][9] = 1;
 510                 ;
 511                 _m = 3; goto P999; /* 1 */
 512         case 36: /* STATE 11 - line 138 "pan.___" - [((prev_off!=write_off))] (3:0:1 - 1) */
 513                 IfNotBlocked
 514                 reached[1][11] = 1;
 515                 if (!((((int)((P1 *)this)->prev_off)!=((int)now.write_off))))
 516                         continue;
 517                 /* dead 1: prev_off */  (trpt+1)->bup.oval = ((P1 *)this)->prev_off;
 518 #ifdef HAS_CODE
 519                 if (!readtrail)
 520 #endif
 521                         ((P1 *)this)->prev_off = 0;
 522                 /* merge: goto cmpxchg_loop(0, 12, 3) */
 523                 reached[1][12] = 1;
 524                 ;
 525                 _m = 3; goto P999; /* 1 */
 526         case 37: /* STATE 14 - line 139 "pan.___" - [write_off = new_off] (0:24:2 - 1) */
 527                 IfNotBlocked
 528                 reached[1][14] = 1;
 529                 (trpt+1)->bup.ovals = grab_ints(2);
 530                 (trpt+1)->bup.ovals[0] = ((int)now.write_off);
 531                 now.write_off = ((int)((P1 *)this)->new_off);
 532 #ifdef VAR_RANGES
 533                 logval("write_off", ((int)now.write_off));
 534 #endif
 535                 ;
 536                 /* merge: .(goto)(24, 16, 24) */
 537                 reached[1][16] = 1;
 538                 ;
 539                 /* merge: i = 0(24, 17, 24) */
 540                 reached[1][17] = 1;
 541                 (trpt+1)->bup.ovals[1] = ((int)((P1 *)this)->i);
 542                 ((P1 *)this)->i = 0;
 543 #ifdef VAR_RANGES
 544                 logval("tracer:i", ((int)((P1 *)this)->i));
 545 #endif
 546                 ;
 547                 /* merge: .(goto)(0, 25, 24) */
 548                 reached[1][25] = 1;
 549                 ;
 550                 _m = 3; goto P999; /* 3 */
 551         case 38: /* STATE 17 - line 141 "pan.___" - [i = 0] (0:24:1 - 2) */
 552                 IfNotBlocked
 553                 reached[1][17] = 1;
 554                 (trpt+1)->bup.oval = ((int)((P1 *)this)->i);
 555                 ((P1 *)this)->i = 0;
 556 #ifdef VAR_RANGES
 557                 logval("tracer:i", ((int)((P1 *)this)->i));
 558 #endif
 559                 ;
 560                 /* merge: .(goto)(0, 25, 24) */
 561                 reached[1][25] = 1;
 562                 ;
 563                 _m = 3; goto P999; /* 1 */
 564         case 39: /* STATE 18 - line 143 "pan.___" - [((i<size))] (24:0:2 - 1) */
 565                 IfNotBlocked
 566                 reached[1][18] = 1;
 567                 if (!((((int)((P1 *)this)->i)<((int)((P1 *)this)->size))))
 568                         continue;
 569                 /* merge: assert((buffer_use[((prev_off+i)%8)]==0))(24, 19, 24) */
 570                 reached[1][19] = 1;
 571                 assert((((int)now.buffer_use[ Index(((((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->i))%8), 8) ])==0), "(buffer_use[((prev_off+i)%8)]==0)", II, tt, t);
 572                 /* merge: buffer_use[((prev_off+i)%8)] = 1(24, 20, 24) */
 573                 reached[1][20] = 1;
 574                 (trpt+1)->bup.ovals = grab_ints(2);
 575                 (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->i))%8), 8) ]);
 576                 now.buffer_use[ Index(((((P1 *)this)->prev_off+((P1 *)this)->i)%8), 8) ] = 1;
 577 #ifdef VAR_RANGES
 578                 logval("buffer_use[((tracer:prev_off+tracer:i)%8)]", ((int)now.buffer_use[ Index(((((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->i))%8), 8) ]));
 579 #endif
 580                 ;
 581                 /* merge: i = (i+1)(24, 21, 24) */
 582                 reached[1][21] = 1;
 583                 (trpt+1)->bup.ovals[1] = ((int)((P1 *)this)->i);
 584                 ((P1 *)this)->i = (((int)((P1 *)this)->i)+1);
 585 #ifdef VAR_RANGES
 586                 logval("tracer:i", ((int)((P1 *)this)->i));
 587 #endif
 588                 ;
 589                 /* merge: .(goto)(0, 25, 24) */
 590                 reached[1][25] = 1;
 591                 ;
 592                 _m = 3; goto P999; /* 4 */
 593         case 40: /* STATE 22 - line 147 "pan.___" - [((i>=size))] (26:0:1 - 1) */
 594                 IfNotBlocked
 595                 reached[1][22] = 1;
 596                 if (!((((int)((P1 *)this)->i)>=((int)((P1 *)this)->size))))
 597                         continue;
 598                 /* dead 1: i */  (trpt+1)->bup.oval = ((P1 *)this)->i;
 599 #ifdef HAS_CODE
 600                 if (!readtrail)
 601 #endif
 602                         ((P1 *)this)->i = 0;
 603                 /* merge: goto :b0(0, 23, 26) */
 604                 reached[1][23] = 1;
 605                 ;
 606                 _m = 3; goto P999; /* 1 */
 607         case 41: /* STATE 28 - line 155 "pan.___" - [i = 0] (0:0:1 - 1) */
 608                 IfNotBlocked
 609                 reached[1][28] = 1;
 610                 (trpt+1)->bup.oval = ((int)((P1 *)this)->i);
 611                 ((P1 *)this)->i = 0;
 612 #ifdef VAR_RANGES
 613                 logval("tracer:i", ((int)((P1 *)this)->i));
 614 #endif
 615                 ;
 616                 _m = 3; goto P999; /* 0 */
 617         case 42: /* STATE 29 - line 157 "pan.___" - [((i<size))] (34:0:2 - 1) */
 618                 IfNotBlocked
 619                 reached[1][29] = 1;
 620                 if (!((((int)((P1 *)this)->i)<((int)((P1 *)this)->size))))
 621                         continue;
 622                 /* merge: buffer_use[((prev_off+i)%8)] = 0(34, 30, 34) */
 623                 reached[1][30] = 1;
 624                 (trpt+1)->bup.ovals = grab_ints(2);
 625                 (trpt+1)->bup.ovals[0] = ((int)now.buffer_use[ Index(((((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->i))%8), 8) ]);
 626                 now.buffer_use[ Index(((((P1 *)this)->prev_off+((P1 *)this)->i)%8), 8) ] = 0;
 627 #ifdef VAR_RANGES
 628                 logval("buffer_use[((tracer:prev_off+tracer:i)%8)]", ((int)now.buffer_use[ Index(((((int)((P1 *)this)->prev_off)+((int)((P1 *)this)->i))%8), 8) ]));
 629 #endif
 630                 ;
 631                 /* merge: i = (i+1)(34, 31, 34) */
 632                 reached[1][31] = 1;
 633                 (trpt+1)->bup.ovals[1] = ((int)((P1 *)this)->i);
 634                 ((P1 *)this)->i = (((int)((P1 *)this)->i)+1);
 635 #ifdef VAR_RANGES
 636                 logval("tracer:i", ((int)((P1 *)this)->i));
 637 #endif
 638                 ;
 639                 /* merge: .(goto)(0, 35, 34) */
 640                 reached[1][35] = 1;
 641                 ;
 642                 _m = 3; goto P999; /* 3 */
 643         case 43: /* STATE 32 - line 160 "pan.___" - [((i>=size))] (44:0:4 - 1) */
 644                 IfNotBlocked
 645                 reached[1][32] = 1;
 646                 if (!((((int)((P1 *)this)->i)>=((int)((P1 *)this)->size))))
 647                         continue;
 648                 /* dead 1: i */  (trpt+1)->bup.ovals = grab_ints(4);
 649                 (trpt+1)->bup.ovals[0] = ((P1 *)this)->i;
 650 #ifdef HAS_CODE
 651                 if (!readtrail)
 652 #endif
 653                         ((P1 *)this)->i = 0;
 654                 /* merge: goto :b1(44, 33, 44) */
 655                 reached[1][33] = 1;
 656                 ;
 657                 /* merge: tmp_commit = (commit_count[((prev_off%8)/(8/2))]+size)(44, 37, 44) */
 658                 reached[1][37] = 1;
 659                 (trpt+1)->bup.ovals[1] = ((int)((P1 *)this)->tmp_commit);
 660                 ((P1 *)this)->tmp_commit = (((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%8)/(8/2)), 2) ])+((int)((P1 *)this)->size));
 661 #ifdef VAR_RANGES
 662                 logval("tracer:tmp_commit", ((int)((P1 *)this)->tmp_commit));
 663 #endif
 664                 ;
 665                 /* merge: _commit_sum = ((_commit_sum-commit_count[((prev_off%8)/(8/2))])+tmp_commit)(44, 38, 44) */
 666                 reached[1][38] = 1;
 667                 (trpt+1)->bup.ovals[2] = ((int)now._commit_sum);
 668                 now._commit_sum = ((((int)now._commit_sum)-((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%8)/(8/2)), 2) ]))+((int)((P1 *)this)->tmp_commit));
 669 #ifdef VAR_RANGES
 670                 logval("_commit_sum", ((int)now._commit_sum));
 671 #endif
 672                 ;
 673                 /* merge: commit_count[((prev_off%8)/(8/2))] = tmp_commit(44, 39, 44) */
 674                 reached[1][39] = 1;
 675                 (trpt+1)->bup.ovals[3] = ((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%8)/(8/2)), 2) ]);
 676                 now.commit_count[ Index(((((P1 *)this)->prev_off%8)/(8/2)), 2) ] = ((int)((P1 *)this)->tmp_commit);
 677 #ifdef VAR_RANGES
 678                 logval("commit_count[((tracer:prev_off%8)/(8/2))]", ((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%8)/(8/2)), 2) ]));
 679 #endif
 680                 ;
 681                 _m = 3; goto P999; /* 4 */
 682         case 44: /* STATE 37 - line 162 "pan.___" - [tmp_commit = (commit_count[((prev_off%8)/(8/2))]+size)] (0:44:3 - 3) */
 683                 IfNotBlocked
 684                 reached[1][37] = 1;
 685                 (trpt+1)->bup.ovals = grab_ints(3);
 686                 (trpt+1)->bup.ovals[0] = ((int)((P1 *)this)->tmp_commit);
 687                 ((P1 *)this)->tmp_commit = (((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%8)/(8/2)), 2) ])+((int)((P1 *)this)->size));
 688 #ifdef VAR_RANGES
 689                 logval("tracer:tmp_commit", ((int)((P1 *)this)->tmp_commit));
 690 #endif
 691                 ;
 692                 /* merge: _commit_sum = ((_commit_sum-commit_count[((prev_off%8)/(8/2))])+tmp_commit)(44, 38, 44) */
 693                 reached[1][38] = 1;
 694                 (trpt+1)->bup.ovals[1] = ((int)now._commit_sum);
 695                 now._commit_sum = ((((int)now._commit_sum)-((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%8)/(8/2)), 2) ]))+((int)((P1 *)this)->tmp_commit));
 696 #ifdef VAR_RANGES
 697                 logval("_commit_sum", ((int)now._commit_sum));
 698 #endif
 699                 ;
 700                 /* merge: commit_count[((prev_off%8)/(8/2))] = tmp_commit(44, 39, 44) */
 701                 reached[1][39] = 1;
 702                 (trpt+1)->bup.ovals[2] = ((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%8)/(8/2)), 2) ]);
 703                 now.commit_count[ Index(((((P1 *)this)->prev_off%8)/(8/2)), 2) ] = ((int)((P1 *)this)->tmp_commit);
 704 #ifdef VAR_RANGES
 705                 logval("commit_count[((tracer:prev_off%8)/(8/2))]", ((int)now.commit_count[ Index(((((int)((P1 *)this)->prev_off)%8)/(8/2)), 2) ]));
 706 #endif
 707                 ;
 708                 _m = 3; goto P999; /* 2 */
 709         case 45: /* STATE 40 - line 170 "pan.___" - [((((((prev_off/8)*8)/2)+(8/2))-tmp_commit))] (50:0:3 - 1) */
 710                 IfNotBlocked
 711                 reached[1][40] = 1;
 712                 if (!((((((((int)((P1 *)this)->prev_off)/8)*8)/2)+(8/2))-((int)((P1 *)this)->tmp_commit))))
 713                         continue;
 714                 /* dead 1: prev_off */  (trpt+1)->bup.ovals = grab_ints(3);
 715                 (trpt+1)->bup.ovals[0] = ((P1 *)this)->prev_off;
 716 #ifdef HAS_CODE
 717                 if (!readtrail)
 718 #endif
 719                         ((P1 *)this)->prev_off = 0;
 720                 /* dead 1: tmp_commit */  (trpt+1)->bup.ovals[1] = ((P1 *)this)->tmp_commit;
 721 #ifdef HAS_CODE
 722                 if (!readtrail)
 723 #endif
 724                         ((P1 *)this)->tmp_commit = 0;
 725                 /* merge: deliver = 1(50, 41, 50) */
 726                 reached[1][41] = 1;
 727                 (trpt+1)->bup.ovals[2] = ((int)deliver);
 728                 deliver = 1;
 729 #ifdef VAR_RANGES
 730                 logval("deliver", ((int)deliver));
 731 #endif
 732                 ;
 733                 /* merge: .(goto)(50, 45, 50) */
 734                 reached[1][45] = 1;
 735                 ;
 736                 _m = 3; goto P999; /* 2 */
 737         case 46: /* STATE 45 - line 175 "pan.___" - [.(goto)] (0:50:0 - 2) */
 738                 IfNotBlocked
 739                 reached[1][45] = 1;
 740                 ;
 741                 _m = 3; goto P999; /* 0 */
 742         case 47: /* STATE 43 - line 173 "pan.___" - [(1)] (50:0:0 - 1) */
 743                 IfNotBlocked
 744                 reached[1][43] = 1;
 745                 if (!(1))
 746                         continue;
 747                 /* merge: .(goto)(50, 45, 50) */
 748                 reached[1][45] = 1;
 749                 ;
 750                 _m = 3; goto P999; /* 1 */
 751         case 48: /* STATE 48 - line 179 "pan.___" - [events_lost = (events_lost+1)] (0:0:1 - 2) */
 752                 IfNotBlocked
 753                 reached[1][48] = 1;
 754                 (trpt+1)->bup.oval = ((int)now.events_lost);
 755                 now.events_lost = (((int)now.events_lost)+1);
 756 #ifdef VAR_RANGES
 757                 logval("events_lost", ((int)now.events_lost));
 758 #endif
 759                 ;
 760                 _m = 3; goto P999; /* 0 */
 761         case 49: /* STATE 49 - line 181 "pan.___" - [refcount = (refcount-1)] (0:0:1 - 2) */
 762                 IfNotBlocked
 763                 reached[1][49] = 1;
 764                 (trpt+1)->bup.oval = ((int)now.refcount);
 765                 now.refcount = (((int)now.refcount)-1);
 766 #ifdef VAR_RANGES
 767                 logval("refcount", ((int)now.refcount));
 768 #endif
 769                 ;
 770                 _m = 3; goto P999; /* 0 */
 771         case 50: /* STATE 51 - line 183 "pan.___" - [-end-] (0:0:0 - 1) */
 772                 IfNotBlocked
 773                 reached[1][51] = 1;
 774                 if (!delproc(1, II)) continue;
 775                 _m = 3; goto P999; /* 0 */
 776
 777                  /* PROC switcher */
 778         case 51: /* STATE 1 - line 75 "pan.___" - [prev_off = write_off] (0:9:3 - 1) */
 779                 IfNotBlocked
 780                 reached[0][1] = 1;
 781                 (trpt+1)->bup.ovals = grab_ints(3);
 782                 (trpt+1)->bup.ovals[0] = ((int)((P0 *)this)->prev_off);
 783                 ((P0 *)this)->prev_off = ((int)now.write_off);
 784 #ifdef VAR_RANGES
 785                 logval("switcher:prev_off", ((int)((P0 *)this)->prev_off));
 786 #endif
 787                 ;
 788                 /* merge: size = ((8/2)-(prev_off%(8/2)))(9, 2, 9) */
 789                 reached[0][2] = 1;
 790                 (trpt+1)->bup.ovals[1] = ((int)((P0 *)this)->size);
 791                 ((P0 *)this)->size = ((8/2)-(((int)((P0 *)this)->prev_off)%(8/2)));
 792 #ifdef VAR_RANGES
 793                 logval("switcher:size", ((int)((P0 *)this)->size));
 794 #endif
 795                 ;
 796                 /* merge: new_off = (prev_off+size)(9, 3, 9) */
 797                 reached[0][3] = 1;
 798                 (trpt+1)->bup.ovals[2] = ((int)((P0 *)this)->new_off);
 799                 ((P0 *)this)->new_off = (((int)((P0 *)this)->prev_off)+((int)((P0 *)this)->size));
 800 #ifdef VAR_RANGES
 801                 logval("switcher:new_off", ((int)((P0 *)this)->new_off));
 802 #endif
 803                 ;
 804                 _m = 3; goto P999; /* 2 */
 805         case 52: /* STATE 4 - line 80 "pan.___" - [(((((new_off-read_off)>8)&&((new_off-read_off)<(255/2)))||(size==(8/2))))] (30:0:3 - 1) */
 806                 IfNotBlocked
 807                 reached[0][4] = 1;
 808                 if (!(((((((int)((P0 *)this)->new_off)-((int)now.read_off))>8)&&((((int)((P0 *)this)->new_off)-((int)now.read_off))<(255/2)))||(((int)((P0 *)this)->size)==(8/2)))))
 809                         continue;
 810                 /* dead 1: new_off */  (trpt+1)->bup.ovals = grab_ints(3);
 811                 (trpt+1)->bup.ovals[0] = ((P0 *)this)->new_off;
 812 #ifdef HAS_CODE
 813                 if (!readtrail)
 814 #endif
 815                         ((P0 *)this)->new_off = 0;
 816                 /* dead 1: size */  (trpt+1)->bup.ovals[1] = ((P0 *)this)->size;
 817 #ifdef HAS_CODE
 818                 if (!readtrail)
 819 #endif
 820                         ((P0 *)this)->size = 0;
 821                 /* merge: refcount = (refcount-1)(30, 5, 30) */
 822                 reached[0][5] = 1;
 823                 (trpt+1)->bup.ovals[2] = ((int)now.refcount);
 824                 now.refcount = (((int)now.refcount)-1);
 825 #ifdef VAR_RANGES
 826                 logval("refcount", ((int)now.refcount));
 827 #endif
 828                 ;
 829                 /* merge: goto not_needed(30, 6, 30) */
 830                 reached[0][6] = 1;
 831                 ;
 832                 _m = 3; goto P999; /* 2 */
 833         case 53: /* STATE 8 - line 83 "pan.___" - [(1)] (18:0:0 - 1) */
 834                 IfNotBlocked
 835                 reached[0][8] = 1;
 836                 if (!(1))
 837                         continue;
 838                 /* merge: .(goto)(0, 10, 18) */
 839                 reached[0][10] = 1;
 840                 ;
 841                 _m = 3; goto P999; /* 1 */
 842         case 54: /* STATE 12 - line 88 "pan.___" - [((prev_off!=write_off))] (11:0:1 - 1) */
 843                 IfNotBlocked
 844                 reached[0][12] = 1;
 845                 if (!((((int)((P0 *)this)->prev_off)!=((int)now.write_off))))
 846                         continue;
 847                 /* dead 1: prev_off */  (trpt+1)->bup.oval = ((P0 *)this)->prev_off;
 848 #ifdef HAS_CODE
 849                 if (!readtrail)
 850 #endif
 851                         ((P0 *)this)->prev_off = 0;
 852                 /* merge: goto cmpxchg_loop(0, 13, 11) */
 853                 reached[0][13] = 1;
 854                 ;
 855                 _m = 3; goto P999; /* 1 */
 856         case 55: /* STATE 17 - line 91 "pan.___" - [.(goto)] (0:29:0 - 1) */
 857                 IfNotBlocked
 858                 reached[0][17] = 1;
 859                 ;
 860                 _m = 3; goto P999; /* 0 */
 861         case 56: /* STATE 15 - line 89 "pan.___" - [write_off = new_off] (0:29:1 - 1) */
 862                 IfNotBlocked
 863                 reached[0][15] = 1;
 864                 (trpt+1)->bup.oval = ((int)now.write_off);
 865                 now.write_off = ((int)((P0 *)this)->new_off);
 866 #ifdef VAR_RANGES
 867                 logval("write_off", ((int)now.write_off));
 868 #endif
 869                 ;
 870                 /* merge: .(goto)(29, 17, 29) */
 871                 reached[0][17] = 1;
 872                 ;
 873                 _m = 3; goto P999; /* 1 */
 874         case 57: /* STATE 19 - line 94 "pan.___" - [tmp_commit = (commit_count[((prev_off%8)/(8/2))]+size)] (0:26:3 - 1) */
 875                 IfNotBlocked
 876                 reached[0][19] = 1;
 877                 (trpt+1)->bup.ovals = grab_ints(3);
 878                 (trpt+1)->bup.ovals[0] = ((int)((P0 *)this)->tmp_commit);
 879                 ((P0 *)this)->tmp_commit = (((int)now.commit_count[ Index(((((int)((P0 *)this)->prev_off)%8)/(8/2)), 2) ])+((int)((P0 *)this)->size));
 880 #ifdef VAR_RANGES
 881                 logval("switcher:tmp_commit", ((int)((P0 *)this)->tmp_commit));
 882 #endif
 883                 ;
 884                 /* merge: _commit_sum = ((_commit_sum-commit_count[((prev_off%8)/(8/2))])+tmp_commit)(26, 20, 26) */
 885                 reached[0][20] = 1;
 886                 (trpt+1)->bup.ovals[1] = ((int)now._commit_sum);
 887                 now._commit_sum = ((((int)now._commit_sum)-((int)now.commit_count[ Index(((((int)((P0 *)this)->prev_off)%8)/(8/2)), 2) ]))+((int)((P0 *)this)->tmp_commit));
 888 #ifdef VAR_RANGES
 889                 logval("_commit_sum", ((int)now._commit_sum));
 890 #endif
 891                 ;
 892                 /* merge: commit_count[((prev_off%8)/(8/2))] = tmp_commit(26, 21, 26) */
 893                 reached[0][21] = 1;
 894                 (trpt+1)->bup.ovals[2] = ((int)now.commit_count[ Index(((((int)((P0 *)this)->prev_off)%8)/(8/2)), 2) ]);
 895                 now.commit_count[ Index(((((P0 *)this)->prev_off%8)/(8/2)), 2) ] = ((int)((P0 *)this)->tmp_commit);
 896 #ifdef VAR_RANGES
 897                 logval("commit_count[((switcher:prev_off%8)/(8/2))]", ((int)now.commit_count[ Index(((((int)((P0 *)this)->prev_off)%8)/(8/2)), 2) ]));
 898 #endif
 899                 ;
 900                 _m = 3; goto P999; /* 2 */
 901         case 58: /* STATE 22 - line 102 "pan.___" - [((((((prev_off/8)*8)/2)+(8/2))-tmp_commit))] (30:0:4 - 1) */
 902                 IfNotBlocked
 903                 reached[0][22] = 1;
 904                 if (!((((((((int)((P0 *)this)->prev_off)/8)*8)/2)+(8/2))-((int)((P0 *)this)->tmp_commit))))
 905                         continue;
 906                 /* dead 1: prev_off */  (trpt+1)->bup.ovals = grab_ints(4);
 907                 (trpt+1)->bup.ovals[0] = ((P0 *)this)->prev_off;
 908 #ifdef HAS_CODE
 909                 if (!readtrail)
 910 #endif
 911                         ((P0 *)this)->prev_off = 0;
 912                 /* dead 1: tmp_commit */  (trpt+1)->bup.ovals[1] = ((P0 *)this)->tmp_commit;
 913 #ifdef HAS_CODE
 914                 if (!readtrail)
 915 #endif
 916                         ((P0 *)this)->tmp_commit = 0;
 917                 /* merge: deliver = 1(30, 23, 30) */
 918                 reached[0][23] = 1;
 919                 (trpt+1)->bup.ovals[2] = ((int)deliver);
 920                 deliver = 1;
 921 #ifdef VAR_RANGES
 922                 logval("deliver", ((int)deliver));
 923 #endif
 924                 ;
 925                 /* merge: .(goto)(30, 27, 30) */
 926                 reached[0][27] = 1;
 927                 ;
 928                 /* merge: refcount = (refcount-1)(30, 28, 30) */
 929                 reached[0][28] = 1;
 930                 (trpt+1)->bup.ovals[3] = ((int)now.refcount);
 931                 now.refcount = (((int)now.refcount)-1);
 932 #ifdef VAR_RANGES
 933                 logval("refcount", ((int)now.refcount));
 934 #endif
 935                 ;
 936                 _m = 3; goto P999; /* 3 */
 937         case 59: /* STATE 27 - line 107 "pan.___" - [.(goto)] (0:30:1 - 2) */
 938                 IfNotBlocked
 939                 reached[0][27] = 1;
 940                 ;
 941                 /* merge: refcount = (refcount-1)(30, 28, 30) */
 942                 reached[0][28] = 1;
 943                 (trpt+1)->bup.oval = ((int)now.refcount);
 944                 now.refcount = (((int)now.refcount)-1);
 945 #ifdef VAR_RANGES
 946                 logval("refcount", ((int)now.refcount));
 947 #endif
 948                 ;
 949                 _m = 3; goto P999; /* 1 */
 950         case 60: /* STATE 25 - line 105 "pan.___" - [(1)] (30:0:1 - 1) */
 951                 IfNotBlocked
 952                 reached[0][25] = 1;
 953                 if (!(1))
 954                         continue;
 955                 /* merge: .(goto)(30, 27, 30) */
 956                 reached[0][27] = 1;
 957                 ;
 958                 /* merge: refcount = (refcount-1)(30, 28, 30) */
 959                 reached[0][28] = 1;
 960                 (trpt+1)->bup.oval = ((int)now.refcount);
 961                 now.refcount = (((int)now.refcount)-1);
 962 #ifdef VAR_RANGES
 963                 logval("refcount", ((int)now.refcount));
 964 #endif
 965                 ;
 966                 _m = 3; goto P999; /* 2 */
 967         case 61: /* STATE 31 - line 111 "pan.___" - [-end-] (0:0:0 - 1) */
 968                 IfNotBlocked
 969                 reached[0][31] = 1;
 970                 if (!delproc(1, II)) continue;
 971                 _m = 3; goto P999; /* 0 */
 972         case  _T5:      /* np_ */
 973                 if (!((!(trpt->o_pm&4) && !(trpt->tau&128))))
 974                         continue;
 975                 /* else fall through */
 976         case  _T2:      /* true */
 977                 _m = 3; goto P999;
 978 #undef rand
 979         }
 980