source: CIVL/mods/dev.civl.abc/examples/svcomp/svcomp_frontend_bug.c

main
Last change on this file was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 9.4 KB
Line 
1extern void __VERIFIER_error() __attribute__ ((__noreturn__));
2extern void __VERIFIER_assume(int);
3
4extern int __VERIFIER_nondet_int();
5/* Generated by CIL v. 1.3.6 */
6/* print_CIL_Input is true */
7
8
9
10void error(void)
11{
12
13 {
14 ERROR: __VERIFIER_error();
15 return;
16}
17}
18
19int c ;
20int c_t ;
21int c_req_up ;
22int p_in ;
23int p_out ;
24int wl_st ;
25int c1_st ;
26int c2_st ;
27int wb_st ;
28int r_st ;
29int wl_i ;
30int c1_i ;
31int c2_i ;
32int wb_i ;
33int r_i ;
34int wl_pc ;
35int c1_pc ;
36int c2_pc ;
37int wb_pc ;
38int e_e ;
39int e_f ;
40int e_g ;
41int e_c ;
42int e_p_in ;
43int e_wl ;
44void write_loop(void) ;
45void compute1(void) ;
46void compute2(void) ;
47void write_back(void) ;
48void read(void) ;
49int d ;
50int data ;
51int processed ;
52static int t_b ;
53void write_loop(void)
54{ int t ;
55
56 {
57 if ((int )wl_pc == 0) {
58 goto WL_ENTRY_LOC;
59 } else {
60 if ((int )wl_pc == 2) {
61 goto WL_WAIT_2_LOC;
62 } else {
63 if ((int )wl_pc == 1) {
64 goto WL_WAIT_1_LOC;
65 } else {
66
67 }
68 }
69 }
70 WL_ENTRY_LOC:
71 wl_st = 2;
72 wl_pc = 1;
73 e_wl = 0;
74
75 goto return_label;
76 WL_WAIT_1_LOC:
77 {
78 while (1) {
79 while_0_continue: /* CIL Label */ ;
80 t = d;
81 data = d;
82 processed = 0;
83 e_f = 1;
84 if ((int )c1_pc == 1) {
85 if ((int )e_f == 1) {
86 c1_st = 0;
87 } else {
88
89 }
90 } else {
91
92 }
93 if ((int )c2_pc == 1) {
94 if ((int )e_f == 1) {
95 c2_st = 0;
96 } else {
97
98 }
99 } else {
100
101 }
102 e_f = 2;
103 wl_st = 2;
104 wl_pc = 2;
105 t_b = t;
106
107 goto return_label;
108 WL_WAIT_2_LOC:
109 t = t_b;
110 if (d == t + 1) {
111
112 } else {
113 if (d == t + 2) {
114
115 } else {
116 {
117 error();
118 }
119 }
120 }
121 if (d == t + 1) {
122
123 } else {
124 {
125 error();
126 }
127
128 }
129 }
130 while_0_break: /* CIL Label */ ;
131 }
132 return_label: /* CIL Label */
133 return;
134}
135}
136void compute1(void)
137{
138
139 {
140 if ((int )c1_pc == 0) {
141 goto C1_ENTRY_LOC;
142 } else {
143 if ((int )c1_pc == 1) {
144 goto C1_WAIT_LOC;
145 } else {
146
147 }
148 }
149 C1_ENTRY_LOC:
150 {
151 while (1) {
152 while_1_continue: /* CIL Label */ ;
153 c1_st = 2;
154 c1_pc = 1;
155
156 goto return_label;
157 C1_WAIT_LOC:
158 if (! processed) {
159 data += 1;
160 e_g = 1;
161 if ((int )wb_pc == 1) {
162 if ((int )e_g == 1) {
163 wb_st = 0;
164 } else {
165
166 }
167 } else {
168
169 }
170 e_g = 2;
171 } else {
172
173 }
174 }
175 while_1_break: /* CIL Label */ ;
176 }
177 return_label: /* CIL Label */
178 return;
179}
180}
181void compute2(void)
182{
183
184 {
185 if ((int )c2_pc == 0) {
186 goto C2_ENTRY_LOC;
187 } else {
188 if ((int )c2_pc == 1) {
189 goto C2_WAIT_LOC;
190 } else {
191
192 }
193 }
194 C2_ENTRY_LOC:
195 {
196 while (1) {
197 while_2_continue: /* CIL Label */ ;
198 c2_st = 2;
199 c2_pc = 1;
200
201 goto return_label;
202 C2_WAIT_LOC:
203 if (! processed) {
204 data += 1;
205 e_g = 1;
206 if ((int )wb_pc == 1) {
207 if ((int )e_g == 1) {
208 wb_st = 0;
209 } else {
210
211 }
212 } else {
213
214 }
215 e_g = 2;
216 } else {
217
218 }
219 }
220 while_2_break: /* CIL Label */ ;
221 }
222 return_label: /* CIL Label */
223 return;
224}
225}
226void write_back(void)
227{
228
229 {
230 if ((int )wb_pc == 0) {
231 goto WB_ENTRY_LOC;
232 } else {
233 if ((int )wb_pc == 1) {
234 goto WB_WAIT_LOC;
235 } else {
236
237 }
238 }
239 WB_ENTRY_LOC:
240 {
241 while (1) {
242 while_3_continue: /* CIL Label */ ;
243 wb_st = 2;
244 wb_pc = 1;
245
246 goto return_label;
247 WB_WAIT_LOC:
248 c_t = data;
249 c_req_up = 1;
250 processed = 1;
251 }
252 while_3_break: /* CIL Label */ ;
253 }
254 return_label: /* CIL Label */
255 return;
256}
257}
258void read(void)
259{
260
261 {
262 d = c;
263 e_e = 1;
264 if ((int )wl_pc == 1) {
265 if ((int )e_wl == 1) {
266 wl_st = 0;
267 } else {
268 goto _L;
269 }
270 } else {
271 _L: /* CIL Label */
272 if ((int )wl_pc == 2) {
273 if ((int )e_e == 1) {
274 wl_st = 0;
275 } else {
276
277 }
278 } else {
279
280 }
281 }
282 e_e = 2;
283 r_st = 2;
284
285 return;
286}
287}
288void eval(void)
289{ int tmp ;
290 int tmp___0 ;
291 int tmp___1 ;
292 int tmp___2 ;
293 int tmp___3 ;
294
295 {
296 {
297 while (1) {
298 while_4_continue: /* CIL Label */ ;
299 if ((int )wl_st == 0) {
300
301 } else {
302 if ((int )c1_st == 0) {
303
304 } else {
305 if ((int )c2_st == 0) {
306
307 } else {
308 if ((int )wb_st == 0) {
309
310 } else {
311 if ((int )r_st == 0) {
312
313 } else {
314 goto while_4_break;
315 }
316 }
317 }
318 }
319 }
320 if ((int )wl_st == 0) {
321 {
322 tmp = __VERIFIER_nondet_int();
323 }
324 if (tmp) {
325 {
326 wl_st = 1;
327 write_loop();
328 }
329 } else {
330
331 }
332 } else {
333
334 }
335 if ((int )c1_st == 0) {
336 {
337 tmp___0 = __VERIFIER_nondet_int();
338 }
339 if (tmp___0) {
340 {
341 c1_st = 1;
342 compute1();
343 }
344 } else {
345
346 }
347 } else {
348
349 }
350 if ((int )c2_st == 0) {
351 {
352 tmp___1 = __VERIFIER_nondet_int();
353 }
354 if (tmp___1) {
355 {
356 c2_st = 1;
357 compute2();
358 }
359 } else {
360
361 }
362 } else {
363
364 }
365 if ((int )wb_st == 0) {
366 {
367 tmp___2 = __VERIFIER_nondet_int();
368 }
369 if (tmp___2) {
370 {
371 wb_st = 1;
372 write_back();
373 }
374 } else {
375
376 }
377 } else {
378
379 }
380 if ((int )r_st == 0) {
381 {
382 tmp___3 = __VERIFIER_nondet_int();
383 }
384 if (tmp___3) {
385 {
386 r_st = 1;
387 read();
388 }
389 } else {
390
391 }
392 } else {
393
394 }
395 }
396 while_4_break: /* CIL Label */ ;
397 }
398
399 return;
400}
401}
402void start_simulation(void)
403{ int kernel_st ;
404
405 {
406/*
407 kernel_st = 0;
408 if ((int )c_req_up == 1) {
409 if (c != c_t) {
410 c = c_t;
411 e_c = 0;
412 } else {
413
414 }
415 c_req_up = 0;
416 } else {
417
418 }
419 if ((int )wl_i == 1) {
420 wl_st = 0;
421 } else {
422 wl_st = 2;
423 }
424 if ((int )c1_i == 1) {
425 c1_st = 0;
426 } else {
427 c1_st = 2;
428 }
429 if ((int )c2_i == 1) {
430 c2_st = 0;
431 } else {
432 c2_st = 2;
433 }
434 if ((int )wb_i == 1) {
435 wb_st = 0;
436 } else {
437 wb_st = 2;
438 }
439 if ((int )r_i == 1) {
440 r_st = 0;
441 } else {
442 r_st = 2;
443 }
444 if ((int )e_f == 0) {
445 e_f = 1;
446 } else {
447
448 }
449 if ((int )e_g == 0) {
450 e_g = 1;
451 } else {
452
453 }
454 if ((int )e_e == 0) {
455 e_e = 1;
456 } else {
457
458 }
459 if ((int )e_c == 0) {
460 e_c = 1;
461 } else {
462
463 }
464 if ((int )e_wl == 0) {
465 e_wl = 1;
466 } else {
467
468 }
469 if ((int )wl_pc == 1) {
470 if ((int )e_wl == 1) {
471 wl_st = 0;
472 } else {
473 goto _L;
474 }
475 } else {
476 _L: // CIL Label
477 if ((int )wl_pc == 2) {
478 if ((int )e_e == 1) {
479 wl_st = 0;
480 } else {
481
482 }
483 } else {
484
485 }
486 }
487 if ((int )c1_pc == 1) {
488 if ((int )e_f == 1) {
489 c1_st = 0;
490 } else {
491
492 }
493 } else {
494
495 }
496 if ((int )c2_pc == 1) {
497 if ((int )e_f == 1) {
498 c2_st = 0;
499 } else {
500
501 }
502 } else {
503
504 }
505 if ((int )wb_pc == 1) {
506 if ((int )e_g == 1) {
507 wb_st = 0;
508 } else {
509
510 }
511 } else {
512
513 }
514 if ((int )e_c == 1) {
515 r_st = 0;
516 } else {
517
518 }
519 if ((int )e_e == 1) {
520 e_e = 2;
521 } else {
522
523 }
524 if ((int )e_f == 1) {
525 e_f = 2;
526 } else {
527
528 }
529 if ((int )e_g == 1) {
530 e_g = 2;
531 } else {
532
533 }
534 if ((int )e_c == 1) {
535 e_c = 2;
536 } else {
537
538 }
539 if ((int )e_wl == 1) {
540 e_wl = 2;
541 } else {
542
543 }
544*/
545 {
546
547 while (1) {
548 while_5_continue: // CIL Label ;
549 {
550 kernel_st = 1;
551 { wl_st = 0; wl_pc = 2; d = t + 42; }
552 eval();
553 }
554/*
555 kernel_st = 2;
556 if ((int )c_req_up == 1) {
557 if (c != c_t) {
558 c = c_t;
559 e_c = 0;
560 } else {
561
562 }
563 c_req_up = 0;
564 } else {
565
566 }
567 kernel_st = 3;
568 if ((int )e_f == 0) {
569 e_f = 1;
570 } else {
571
572 }
573 if ((int )e_g == 0) {
574 e_g = 1;
575 } else {
576
577 }
578 if ((int )e_e == 0) {
579 e_e = 1;
580 } else {
581
582 }
583 if ((int )e_c == 0) {
584 e_c = 1;
585 } else {
586
587 }
588 if ((int )e_wl == 0) {
589 e_wl = 1;
590 } else {
591
592 }
593 if ((int )wl_pc == 1) {
594 if ((int )e_wl == 1) {
595 wl_st = 0;
596 } else {
597 goto _L___0;
598 }
599 } else {
600 _L___0: // CIL Label
601 if ((int )wl_pc == 2) {
602 if ((int )e_e == 1) {
603 wl_st = 0;
604 } else {
605
606 }
607 } else {
608
609 }
610 }
611 if ((int )c1_pc == 1) {
612 if ((int )e_f == 1) {
613 c1_st = 0;
614 } else {
615
616 }
617 } else {
618
619 }
620 if ((int )c2_pc == 1) {
621 if ((int )e_f == 1) {
622 c2_st = 0;
623 } else {
624
625 }
626 } else {
627
628 }
629 if ((int )wb_pc == 1) {
630 if ((int )e_g == 1) {
631 wb_st = 0;
632 } else {
633
634 }
635 } else {
636
637 }
638 if ((int )e_c == 1) {
639 r_st = 0;
640 } else {
641
642 }
643 if ((int )e_e == 1) {
644 e_e = 2;
645 } else {
646
647 }
648 if ((int )e_f == 1) {
649 e_f = 2;
650 } else {
651
652 }
653 if ((int )e_g == 1) {
654 e_g = 2;
655 } else {
656
657 }
658 if ((int )e_c == 1) {
659 e_c = 2;
660 } else {
661
662 }
663 if ((int )e_wl == 1) {
664 e_wl = 2;
665 } else {
666
667 }
668 if ((int )wl_st == 0) {
669
670 } else {
671 if ((int )c1_st == 0) {
672
673 } else {
674 if ((int )c2_st == 0) {
675
676 } else {
677 if ((int )wb_st == 0) {
678
679 } else {
680 if ((int )r_st == 0) {
681
682 } else {
683 goto while_5_break;
684 }
685 }
686 }
687 }
688 }
689*/
690 }
691
692 while_5_break: // CIL Label
693 ;
694 }
695
696 return;
697}
698}
699int main(void)
700{ int __retres1 ;
701
702 {
703 {
704 e_wl = 2;
705 e_c = e_wl;
706 e_g = e_c;
707 e_f = e_g;
708 e_e = e_f;
709 wl_pc = 0;
710 c1_pc = 0;
711 c2_pc = 0;
712 wb_pc = 0;
713 wb_i = 1;
714 c2_i = wb_i;
715 c1_i = c2_i;
716 wl_i = c1_i;
717 r_i = 0;
718 c_req_up = 0;
719 d = 0;
720 c = 0;
721 start_simulation();
722 }
723 __retres1 = 0;
724 return (__retres1);
725}
726}
Note: See TracBrowser for help on using the repository browser.