1extern unsigned int __VERIFIER_nondet_uint();
2extern int __VERIFIER_nondet_int();
3void error(void)
4{
5 {
6 goto ERROR;
7 ERROR: ;
8 return;
9}
10}
11int c ;
12int c_t ;
13int c_req_up ;
14int p_in ;
15int p_out ;
16int wl_st ;
17int c1_st ;
18int c2_st ;
19int wb_st ;
20int r_st ;
21int wl_i ;
22int c1_i ;
23int c2_i ;
24int wb_i ;
25int r_i ;
26int wl_pc ;
27int c1_pc ;
28int c2_pc ;
29int wb_pc ;
30int e_e ;
31int e_f ;
32int e_g ;
33int e_c ;
34int e_p_in ;
35int e_wl ;
36void write_loop(void) ;
37void compute1(void) ;
38void compute2(void) ;
39void write_back(void) ;
40void read(void) ;
41int d ;
42int data ;
43int processed ;
44static int t_b ;
45void write_loop(void)
46{ int t ;
47 {
48 if ((int )wl_pc == 0) {
49 goto WL_ENTRY_LOC;
50 } else {
51 if ((int )wl_pc == 2) {
52 goto WL_WAIT_2_LOC;
53 } else {
54 if ((int )wl_pc == 1) {
55 goto WL_WAIT_1_LOC;
56 } else {
57 }
58 }
59 }
60 WL_ENTRY_LOC:
61 wl_st = 2;
62 wl_pc = 1;
63 e_wl = 0;
64 goto return_label;
65 WL_WAIT_1_LOC:
66 {
67 unsigned int loop1=0, n1=__VERIFIER_nondet_uint();
68 while (loop1<n1 ) {
69 loop1++;
70 while_0_continue: ;
71 t = d;
72 data = d;
73 processed = 0;
74 e_f = 1;
75 if ((int )c1_pc == 1) {
76 if ((int )e_f == 1) {
77 c1_st = 0;
78 } else {
79 }
80 } else {
81 }
82 if ((int )c2_pc == 1) {
83 if ((int )e_f == 1) {
84 c2_st = 0;
85 } else {
86 }
87 } else {
88 }
89 e_f = 2;
90 wl_st = 2;
91 wl_pc = 2;
92 t_b = t;
93 goto return_label;
94 WL_WAIT_2_LOC:
95 t = t_b;
96 if (d == t + 1) {
97 } else {
98 if (d == t + 2) {
99 } else {
100 {
101 error();
102 }
103 }
104 }
105 }
106 while_0_break: ;
107 }
108 return_label:
109 return;
110}
111}
112void compute1(void)
113{
114 {
115 if ((int )c1_pc == 0) {
116 goto C1_ENTRY_LOC;
117 } else {
118 if ((int )c1_pc == 1) {
119 goto C1_WAIT_LOC;
120 } else {
121 }
122 }
123 C1_ENTRY_LOC:
124 {
125 unsigned int loop2=0, n2=__VERIFIER_nondet_uint();
126 while (loop2<n2 ) {
127 loop2++;
128 while_1_continue: ;
129 c1_st = 2;
130 c1_pc = 1;
131 goto return_label;
132 C1_WAIT_LOC:
133 if (! processed) {
134 data += 1;
135 e_g = 1;
136 if ((int )wb_pc == 1) {
137 if ((int )e_g == 1) {
138 wb_st = 0;
139 } else {
140 }
141 } else {
142 }
143 e_g = 2;
144 } else {
145 }
146 }
147 while_1_break: ;
148 }
149 return_label:
150 return;
151}
152}
153void compute2(void)
154{
155 {
156 if ((int )c2_pc == 0) {
157 goto C2_ENTRY_LOC;
158 } else {
159 if ((int )c2_pc == 1) {
160 goto C2_WAIT_LOC;
161 } else {
162 }
163 }
164 C2_ENTRY_LOC:
165 {
166 unsigned int loop3=0, n3=__VERIFIER_nondet_uint();
167 while (loop3<n3 ) {
168 loop3++;
169 while_2_continue: ;
170 c2_st = 2;
171 c2_pc = 1;
172 goto return_label;
173 C2_WAIT_LOC:
174 if (! processed) {
175 data += 1;
176 e_g = 1;
177 if ((int )wb_pc == 1) {
178 if ((int )e_g == 1) {
179 wb_st = 0;
180 } else {
181 }
182 } else {
183 }
184 e_g = 2;
185 } else {
186 }
187 }
188 while_2_break: ;
189 }
190 return_label:
191 return;
192}
193}
194void write_back(void)
195{
196 {
197 if ((int )wb_pc == 0) {
198 goto WB_ENTRY_LOC;
199 } else {
200 if ((int )wb_pc == 1) {
201 goto WB_WAIT_LOC;
202 } else {
203 }
204 }
205 WB_ENTRY_LOC:
206 {
207 unsigned int loop4=0, n4=__VERIFIER_nondet_uint();
208 while (loop4<n4 ) {
209 loop4++;
210 while_3_continue: ;
211 wb_st = 2;
212 wb_pc = 1;
213 goto return_label;
214 WB_WAIT_LOC:
215 c_t = data;
216 c_req_up = 1;
217 processed = 1;
218 }
219 while_3_break: ;
220 }
221 return_label:
222 return;
223}
224}
225void read(void)
226{
227 {
228 d = c;
229 e_e = 1;
230 if ((int )wl_pc == 1) {
231 if ((int )e_wl == 1) {
232 wl_st = 0;
233 } else {
234 goto _L;
235 }
236 } else {
237 _L:
238 if ((int )wl_pc == 2) {
239 if ((int )e_e == 1) {
240 wl_st = 0;
241 } else {
242 }
243 } else {
244 }
245 }
246 e_e = 2;
247 r_st = 2;
248 return;
249}
250}
251void eval(void)
252{ int tmp ;
253 int tmp___0 ;
254 int tmp___1 ;
255 int tmp___2 ;
256 int tmp___3 ;
257 {
258 {
259 unsigned int loop5=0, n5=__VERIFIER_nondet_uint();
260 while (loop5<n5 ) {
261 loop5++;
262 while_4_continue: ;
263 if ((int )wl_st == 0) {
264 } else {
265 if ((int )c1_st == 0) {
266 } else {
267 if ((int )c2_st == 0) {
268 } else {
269 if ((int )wb_st == 0) {
270 } else {
271 if ((int )r_st == 0) {
272 } else {
273 goto while_4_break;
274 }
275 }
276 }
277 }
278 }
279 if ((int )wl_st == 0) {
280 {
281 tmp = __VERIFIER_nondet_int();
282 }
283 if (tmp) {
284 {
285 wl_st = 1;
286 write_loop();
287 }
288 } else {
289 }
290 } else {
291 }
292 if ((int )c1_st == 0) {
293 {
294 tmp___0 = __VERIFIER_nondet_int();
295 }
296 if (tmp___0) {
297 {
298 c1_st = 1;
299 compute1();
300 }
301 } else {
302 }
303 } else {
304 }
305 if ((int )c2_st == 0) {
306 {
307 tmp___1 = __VERIFIER_nondet_int();
308 }
309 if (tmp___1) {
310 {
311 c2_st = 1;
312 compute2();
313 }
314 } else {
315 }
316 } else {
317 }
318 if ((int )wb_st == 0) {
319 {
320 tmp___2 = __VERIFIER_nondet_int();
321 }
322 if (tmp___2) {
323 {
324 wb_st = 1;
325 write_back();
326 }
327 } else {
328 }
329 } else {
330 }
331 if ((int )r_st == 0) {
332 {
333 tmp___3 = __VERIFIER_nondet_int();
334 }
335 if (tmp___3) {
336 {
337 r_st = 1;
338 read();
339 }
340 } else {
341 }
342 } else {
343 }
344 }
345 while_4_break: ;
346 }
347 return;
348}
349}
350void start_simulation(void)
351{ int kernel_st ;
352 {
353 kernel_st = 0;
354 if ((int )c_req_up == 1) {
355 if (c != c_t) {
356 c = c_t;
357 e_c = 0;
358 } else {
359 }
360 c_req_up = 0;
361 } else {
362 }
363 if ((int )wl_i == 1) {
364 wl_st = 0;
365 } else {
366 wl_st = 2;
367 }
368 if ((int )c1_i == 1) {
369 c1_st = 0;
370 } else {
371 c1_st = 2;
372 }
373 if ((int )c2_i == 1) {
374 c2_st = 0;
375 } else {
376 c2_st = 2;
377 }
378 if ((int )wb_i == 1) {
379 wb_st = 0;
380 } else {
381 wb_st = 2;
382 }
383 if ((int )r_i == 1) {
384 r_st = 0;
385 } else {
386 r_st = 2;
387 }
388 if ((int )e_f == 0) {
389 e_f = 1;
390 } else {
391 }
392 if ((int )e_g == 0) {
393 e_g = 1;
394 } else {
395 }
396 if ((int )e_e == 0) {
397 e_e = 1;
398 } else {
399 }
400 if ((int )e_c == 0) {
401 e_c = 1;
402 } else {
403 }
404 if ((int )e_wl == 0) {
405 e_wl = 1;
406 } else {
407 }
408 if ((int )wl_pc == 1) {
409 if ((int )e_wl == 1) {
410 wl_st = 0;
411 } else {
412 goto _L;
413 }
414 } else {
415 _L:
416 if ((int )wl_pc == 2) {
417 if ((int )e_e == 1) {
418 wl_st = 0;
419 } else {
420 }
421 } else {
422 }
423 }
424 if ((int )c1_pc == 1) {
425 if ((int )e_f == 1) {
426 c1_st = 0;
427 } else {
428 }
429 } else {
430 }
431 if ((int )c2_pc == 1) {
432 if ((int )e_f == 1) {
433 c2_st = 0;
434 } else {
435 }
436 } else {
437 }
438 if ((int )wb_pc == 1) {
439 if ((int )e_g == 1) {
440 wb_st = 0;
441 } else {
442 }
443 } else {
444 }
445 if ((int )e_c == 1) {
446 r_st = 0;
447 } else {
448 }
449 if ((int )e_e == 1) {
450 e_e = 2;
451 } else {
452 }
453 if ((int )e_f == 1) {
454 e_f = 2;
455 } else {
456 }
457 if ((int )e_g == 1) {
458 e_g = 2;
459 } else {
460 }
461 if ((int )e_c == 1) {
462 e_c = 2;
463 } else {
464 }
465 if ((int )e_wl == 1) {
466 e_wl = 2;
467 } else {
468 }
469 {
470 unsigned int loop6=0, n6=__VERIFIER_nondet_uint();
471 while (loop6<n6 ) {
472 loop6++;
473 while_5_continue: ;
474 {
475 kernel_st = 1;
476 eval();
477 }
478 kernel_st = 2;
479 if ((int )c_req_up == 1) {
480 if (c != c_t) {
481 c = c_t;
482 e_c = 0;
483 } else {
484 }
485 c_req_up = 0;
486 } else {
487 }
488 kernel_st = 3;
489 if ((int )e_f == 0) {
490 e_f = 1;
491 } else {
492 }
493 if ((int )e_g == 0) {
494 e_g = 1;
495 } else {
496 }
497 if ((int )e_e == 0) {
498 e_e = 1;
499 } else {
500 }
501 if ((int )e_c == 0) {
502 e_c = 1;
503 } else {
504 }
505 if ((int )e_wl == 0) {
506 e_wl = 1;
507 } else {
508 }
509 if ((int )wl_pc == 1) {
510 if ((int )e_wl == 1) {
511 wl_st = 0;
512 } else {
513 goto _L___0;
514 }
515 } else {
516 _L___0:
517 if ((int )wl_pc == 2) {
518 if ((int )e_e == 1) {
519 wl_st = 0;
520 } else {
521 }
522 } else {
523 }
524 }
525 if ((int )c1_pc == 1) {
526 if ((int )e_f == 1) {
527 c1_st = 0;
528 } else {
529 }
530 } else {
531 }
532 if ((int )c2_pc == 1) {
533 if ((int )e_f == 1) {
534 c2_st = 0;
535 } else {
536 }
537 } else {
538 }
539 if ((int )wb_pc == 1) {
540 if ((int )e_g == 1) {
541 wb_st = 0;
542 } else {
543 }
544 } else {
545 }
546 if ((int )e_c == 1) {
547 r_st = 0;
548 } else {
549 }
550 if ((int )e_e == 1) {
551 e_e = 2;
552 } else {
553 }
554 if ((int )e_f == 1) {
555 e_f = 2;
556 } else {
557 }
558 if ((int )e_g == 1) {
559 e_g = 2;
560 } else {
561 }
562 if ((int )e_c == 1) {
563 e_c = 2;
564 } else {
565 }
566 if ((int )e_wl == 1) {
567 e_wl = 2;
568 } else {
569 }
570 if ((int )wl_st == 0) {
571 } else {
572 if ((int )c1_st == 0) {
573 } else {
574 if ((int )c2_st == 0) {
575 } else {
576 if ((int )wb_st == 0) {
577 } else {
578 if ((int )r_st == 0) {
579 } else {
580 goto while_5_break;
581 }
582 }
583 }
584 }
585 }
586 }
587 while_5_break: ;
588 }
589 return;
590}
591}
592int main(void)
593{ int __retres1 ;
594 {
595 {
596 e_wl = 2;
597 e_c = e_wl;
598 e_g = e_c;
599 e_f = e_g;
600 e_e = e_f;
601 wl_pc = 0;
602 c1_pc = 0;
603 c2_pc = 0;
604 wb_pc = 0;
605 wb_i = 1;
606 c2_i = wb_i;
607 c1_i = c2_i;
608 wl_i = c1_i;
609 r_i = 0;
610 c_req_up = 0;
611 d = 0;
612 c = 0;
613 start_simulation();
614 }
615 __retres1 = 0;
616 return (__retres1);
617}
618}