| 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 | |