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