User: | Jiri Slaby |
Error type: | Reachable Error Location |
Error type description: | A specified error location is reachable in some program path |
File location: | systemc/token_ring.08_safe.cil.c |
Line in file: | 8 |
Project: | SV-COMP 2013 |
Project version: | 2.6.28 |
Tools: |
Manual Work
|
Entered: | 2013-01-17 16:57:54 UTC |
1/* Generated by CIL v. 1.3.6 */ 2/* print_CIL_Input is true */ 3 4void error(void) 5{ 6 7 { 8 ERROR: ; 9 goto ERROR; 10 return; 11} 12} 13int m_pc = 0; 14int t1_pc = 0; 15int t2_pc = 0; 16int t3_pc = 0; 17int t4_pc = 0; 18int t5_pc = 0; 19int t6_pc = 0; 20int t7_pc = 0; 21int t8_pc = 0; 22int m_st ; 23int t1_st ; 24int t2_st ; 25int t3_st ; 26int t4_st ; 27int t5_st ; 28int t6_st ; 29int t7_st ; 30int t8_st ; 31int m_i ; 32int t1_i ; 33int t2_i ; 34int t3_i ; 35int t4_i ; 36int t5_i ; 37int t6_i ; 38int t7_i ; 39int t8_i ; 40int M_E = 2; 41int T1_E = 2; 42int T2_E = 2; 43int T3_E = 2; 44int T4_E = 2; 45int T5_E = 2; 46int T6_E = 2; 47int T7_E = 2; 48int T8_E = 2; 49int E_M = 2; 50int E_1 = 2; 51int E_2 = 2; 52int E_3 = 2; 53int E_4 = 2; 54int E_5 = 2; 55int E_6 = 2; 56int E_7 = 2; 57int E_8 = 2; 58int is_master_triggered(void) ; 59int is_transmit1_triggered(void) ; 60int is_transmit2_triggered(void) ; 61int is_transmit3_triggered(void) ; 62int is_transmit4_triggered(void) ; 63int is_transmit5_triggered(void) ; 64int is_transmit6_triggered(void) ; 65int is_transmit7_triggered(void) ; 66int is_transmit8_triggered(void) ; 67void immediate_notify(void) ; 68int token ; 69int __VERIFIER_nondet_int() ; 70int local ; 71void master(void) 72{ 73 74 { 75 if (m_pc == 0) { 76 goto M_ENTRY; 77 } else { 78 if (m_pc == 1) { 79 goto M_WAIT; 80 } else { 81 82 } 83 } 84 M_ENTRY: ; 85 { 86 while (1) { 87 while_0_continue: /* CIL Label */ ; 88 { 89 token = __VERIFIER_nondet_int(); 90 local = token; 91 E_1 = 1; 92 immediate_notify(); 93 E_1 = 2; 94 m_pc = 1; 95 m_st = 2; 96 } 97 98 goto return_label; 99 M_WAIT: ; 100 if (token != local + 8) { 101 { 102 error(); 103 } 104 } else { 105 106 } 107 } 108 while_0_break: /* CIL Label */ ; 109 } 110 111 return_label: /* CIL Label */ 112 return; 113} 114} 115void transmit1(void) 116{ 117 118 { 119 if (t1_pc == 0) { 120 goto T1_ENTRY; 121 } else { 122 if (t1_pc == 1) { 123 goto T1_WAIT; 124 } else { 125 126 } 127 } 128 T1_ENTRY: ; 129 { 130 while (1) { 131 while_1_continue: /* CIL Label */ ; 132 t1_pc = 1; 133 t1_st = 2; 134 135 goto return_label; 136 T1_WAIT: 137 { 138 token += 1; 139 E_2 = 1; 140 immediate_notify(); 141 E_2 = 2; 142 } 143 } 144 while_1_break: /* CIL Label */ ; 145 } 146 147 return_label: /* CIL Label */ 148 return; 149} 150} 151void transmit2(void) 152{ 153 154 { 155 if (t2_pc == 0) { 156 goto T2_ENTRY; 157 } else { 158 if (t2_pc == 1) { 159 goto T2_WAIT; 160 } else { 161 162 } 163 } 164 T2_ENTRY: ; 165 { 166 while (1) { 167 while_2_continue: /* CIL Label */ ; 168 t2_pc = 1; 169 t2_st = 2; 170 171 goto return_label; 172 T2_WAIT: 173 { 174 token += 1; 175 E_3 = 1; 176 immediate_notify(); 177 E_3 = 2; 178 } 179 } 180 while_2_break: /* CIL Label */ ; 181 } 182 183 return_label: /* CIL Label */ 184 return; 185} 186} 187void transmit3(void) 188{ 189 190 { 191 if (t3_pc == 0) { 192 goto T3_ENTRY; 193 } else { 194 if (t3_pc == 1) { 195 goto T3_WAIT; 196 } else { 197 198 } 199 } 200 T3_ENTRY: ; 201 { 202 while (1) { 203 while_3_continue: /* CIL Label */ ; 204 t3_pc = 1; 205 t3_st = 2; 206 207 goto return_label; 208 T3_WAIT: 209 { 210 token += 1; 211 E_4 = 1; 212 immediate_notify(); 213 E_4 = 2; 214 } 215 } 216 while_3_break: /* CIL Label */ ; 217 } 218 219 return_label: /* CIL Label */ 220 return; 221} 222} 223void transmit4(void) 224{ 225 226 { 227 if (t4_pc == 0) { 228 goto T4_ENTRY; 229 } else { 230 if (t4_pc == 1) { 231 goto T4_WAIT; 232 } else { 233 234 } 235 } 236 T4_ENTRY: ; 237 { 238 while (1) { 239 while_4_continue: /* CIL Label */ ; 240 t4_pc = 1; 241 t4_st = 2; 242 243 goto return_label; 244 T4_WAIT: 245 { 246 token += 1; 247 E_5 = 1; 248 immediate_notify(); 249 E_5 = 2; 250 } 251 } 252 while_4_break: /* CIL Label */ ; 253 } 254 255 return_label: /* CIL Label */ 256 return; 257} 258} 259void transmit5(void) 260{ 261 262 { 263 if (t5_pc == 0) { 264 goto T5_ENTRY; 265 } else { 266 if (t5_pc == 1) { 267 goto T5_WAIT; 268 } else { 269 270 } 271 } 272 T5_ENTRY: ; 273 { 274 while (1) { 275 while_5_continue: /* CIL Label */ ; 276 t5_pc = 1; 277 t5_st = 2; 278 279 goto return_label; 280 T5_WAIT: 281 { 282 token += 1; 283 E_6 = 1; 284 immediate_notify(); 285 E_6 = 2; 286 } 287 } 288 while_5_break: /* CIL Label */ ; 289 } 290 291 return_label: /* CIL Label */ 292 return; 293} 294} 295void transmit6(void) 296{ 297 298 { 299 if (t6_pc == 0) { 300 goto T6_ENTRY; 301 } else { 302 if (t6_pc == 1) { 303 goto T6_WAIT; 304 } else { 305 306 } 307 } 308 T6_ENTRY: ; 309 { 310 while (1) { 311 while_6_continue: /* CIL Label */ ; 312 t6_pc = 1; 313 t6_st = 2; 314 315 goto return_label; 316 T6_WAIT: 317 { 318 token += 1; 319 E_7 = 1; 320 immediate_notify(); 321 E_7 = 2; 322 } 323 } 324 while_6_break: /* CIL Label */ ; 325 } 326 327 return_label: /* CIL Label */ 328 return; 329} 330} 331void transmit7(void) 332{ 333 334 { 335 if (t7_pc == 0) { 336 goto T7_ENTRY; 337 } else { 338 if (t7_pc == 1) { 339 goto T7_WAIT; 340 } else { 341 342 } 343 } 344 T7_ENTRY: ; 345 { 346 while (1) { 347 while_7_continue: /* CIL Label */ ; 348 t7_pc = 1; 349 t7_st = 2; 350 351 goto return_label; 352 T7_WAIT: 353 { 354 token += 1; 355 E_8 = 1; 356 immediate_notify(); 357 E_8 = 2; 358 } 359 } 360 while_7_break: /* CIL Label */ ; 361 } 362 363 return_label: /* CIL Label */ 364 return; 365} 366} 367void transmit8(void) 368{ 369 370 { 371 if (t8_pc == 0) { 372 goto T8_ENTRY; 373 } else { 374 if (t8_pc == 1) { 375 goto T8_WAIT; 376 } else { 377 378 } 379 } 380 T8_ENTRY: ; 381 { 382 while (1) { 383 while_8_continue: /* CIL Label */ ; 384 t8_pc = 1; 385 t8_st = 2; 386 387 goto return_label; 388 T8_WAIT: 389 { 390 token += 1; 391 E_M = 1; 392 immediate_notify(); 393 E_M = 2; 394 } 395 } 396 while_8_break: /* CIL Label */ ; 397 } 398 399 return_label: /* CIL Label */ 400 return; 401} 402} 403int is_master_triggered(void) 404{ int __retres1 ; 405 406 { 407 if (m_pc == 1) { 408 if (E_M == 1) { 409 __retres1 = 1; 410 goto return_label; 411 } else { 412 413 } 414 } else { 415 416 } 417 __retres1 = 0; 418 return_label: /* CIL Label */ 419 return (__retres1); 420} 421} 422int is_transmit1_triggered(void) 423{ int __retres1 ; 424 425 { 426 if (t1_pc == 1) { 427 if (E_1 == 1) { 428 __retres1 = 1; 429 goto return_label; 430 } else { 431 432 } 433 } else { 434 435 } 436 __retres1 = 0; 437 return_label: /* CIL Label */ 438 return (__retres1); 439} 440} 441int is_transmit2_triggered(void) 442{ int __retres1 ; 443 444 { 445 if (t2_pc == 1) { 446 if (E_2 == 1) { 447 __retres1 = 1; 448 goto return_label; 449 } else { 450 451 } 452 } else { 453 454 } 455 __retres1 = 0; 456 return_label: /* CIL Label */ 457 return (__retres1); 458} 459} 460int is_transmit3_triggered(void) 461{ int __retres1 ; 462 463 { 464 if (t3_pc == 1) { 465 if (E_3 == 1) { 466 __retres1 = 1; 467 goto return_label; 468 } else { 469 470 } 471 } else { 472 473 } 474 __retres1 = 0; 475 return_label: /* CIL Label */ 476 return (__retres1); 477} 478} 479int is_transmit4_triggered(void) 480{ int __retres1 ; 481 482 { 483 if (t4_pc == 1) { 484 if (E_4 == 1) { 485 __retres1 = 1; 486 goto return_label; 487 } else { 488 489 } 490 } else { 491 492 } 493 __retres1 = 0; 494 return_label: /* CIL Label */ 495 return (__retres1); 496} 497} 498int is_transmit5_triggered(void) 499{ int __retres1 ; 500 501 { 502 if (t5_pc == 1) { 503 if (E_5 == 1) { 504 __retres1 = 1; 505 goto return_label; 506 } else { 507 508 } 509 } else { 510 511 } 512 __retres1 = 0; 513 return_label: /* CIL Label */ 514 return (__retres1); 515} 516} 517int is_transmit6_triggered(void) 518{ int __retres1 ; 519 520 { 521 if (t6_pc == 1) { 522 if (E_6 == 1) { 523 __retres1 = 1; 524 goto return_label; 525 } else { 526 527 } 528 } else { 529 530 } 531 __retres1 = 0; 532 return_label: /* CIL Label */ 533 return (__retres1); 534} 535} 536int is_transmit7_triggered(void) 537{ int __retres1 ; 538 539 { 540 if (t7_pc == 1) { 541 if (E_7 == 1) { 542 __retres1 = 1; 543 goto return_label; 544 } else { 545 546 } 547 } else { 548 549 } 550 __retres1 = 0; 551 return_label: /* CIL Label */ 552 return (__retres1); 553} 554} 555int is_transmit8_triggered(void) 556{ int __retres1 ; 557 558 { 559 if (t8_pc == 1) { 560 if (E_8 == 1) { 561 __retres1 = 1; 562 goto return_label; 563 } else { 564 565 } 566 } else { 567 568 } 569 __retres1 = 0; 570 return_label: /* CIL Label */ 571 return (__retres1); 572} 573} 574void update_channels(void) 575{ 576 577 { 578 579 return; 580} 581} 582void init_threads(void) 583{ 584 585 { 586 if (m_i == 1) { 587 m_st = 0; 588 } else { 589 m_st = 2; 590 } 591 if (t1_i == 1) { 592 t1_st = 0; 593 } else { 594 t1_st = 2; 595 } 596 if (t2_i == 1) { 597 t2_st = 0; 598 } else { 599 t2_st = 2; 600 } 601 if (t3_i == 1) { 602 t3_st = 0; 603 } else { 604 t3_st = 2; 605 } 606 if (t4_i == 1) { 607 t4_st = 0; 608 } else { 609 t4_st = 2; 610 } 611 if (t5_i == 1) { 612 t5_st = 0; 613 } else { 614 t5_st = 2; 615 } 616 if (t6_i == 1) { 617 t6_st = 0; 618 } else { 619 t6_st = 2; 620 } 621 if (t7_i == 1) { 622 t7_st = 0; 623 } else { 624 t7_st = 2; 625 } 626 if (t8_i == 1) { 627 t8_st = 0; 628 } else { 629 t8_st = 2; 630 } 631 632 return; 633} 634} 635int exists_runnable_thread(void) 636{ int __retres1 ; 637 638 { 639 if (m_st == 0) { 640 __retres1 = 1; 641 goto return_label; 642 } else { 643 if (t1_st == 0) { 644 __retres1 = 1; 645 goto return_label; 646 } else { 647 if (t2_st == 0) { 648 __retres1 = 1; 649 goto return_label; 650 } else { 651 if (t3_st == 0) { 652 __retres1 = 1; 653 goto return_label; 654 } else { 655 if (t4_st == 0) { 656 __retres1 = 1; 657 goto return_label; 658 } else { 659 if (t5_st == 0) { 660 __retres1 = 1; 661 goto return_label; 662 } else { 663 if (t6_st == 0) { 664 __retres1 = 1; 665 goto return_label; 666 } else { 667 if (t7_st == 0) { 668 __retres1 = 1; 669 goto return_label; 670 } else { 671 if (t8_st == 0) { 672 __retres1 = 1; 673 goto return_label; 674 } else { 675 676 } 677 } 678 } 679 } 680 } 681 } 682 } 683 } 684 } 685 __retres1 = 0; 686 return_label: /* CIL Label */ 687 return (__retres1); 688} 689} 690void eval(void) 691{ 692 int tmp ; 693 694 { 695 { 696 while (1) { 697 while_9_continue: /* CIL Label */ ; 698 { 699 tmp = exists_runnable_thread(); 700 } 701 if (tmp) { 702 703 } else { 704 goto while_9_break; 705 } 706 if (m_st == 0) { 707 int tmp_ndt_1; 708 tmp_ndt_1 = __VERIFIER_nondet_int(); 709 if (tmp_ndt_1) { 710 { 711 m_st = 1; 712 master(); 713 } 714 } else { 715 716 } 717 } else { 718 719 } 720 if (t1_st == 0) { 721 int tmp_ndt_2; 722 tmp_ndt_2 = __VERIFIER_nondet_int(); 723 if (tmp_ndt_2) { 724 { 725 t1_st = 1; 726 transmit1(); 727 } 728 } else { 729 730 } 731 } else { 732 733 } 734 if (t2_st == 0) { 735 int tmp_ndt_3; 736 tmp_ndt_3 = __VERIFIER_nondet_int(); 737 if (tmp_ndt_3) { 738 { 739 t2_st = 1; 740 transmit2(); 741 } 742 } else { 743 744 } 745 } else { 746 747 } 748 if (t3_st == 0) { 749 int tmp_ndt_4; 750 tmp_ndt_4 = __VERIFIER_nondet_int(); 751 if (tmp_ndt_4) { 752 { 753 t3_st = 1; 754 transmit3(); 755 } 756 } else { 757 758 } 759 } else { 760 761 } 762 if (t4_st == 0) { 763 int tmp_ndt_5; 764 tmp_ndt_5 = __VERIFIER_nondet_int(); 765 if (tmp_ndt_5) { 766 { 767 t4_st = 1; 768 transmit4(); 769 } 770 } else { 771 772 } 773 } else { 774 775 } 776 if (t5_st == 0) { 777 int tmp_ndt_6; 778 tmp_ndt_6 = __VERIFIER_nondet_int(); 779 if (tmp_ndt_6) { 780 { 781 t5_st = 1; 782 transmit5(); 783 } 784 } else { 785 786 } 787 } else { 788 789 } 790 if (t6_st == 0) { 791 int tmp_ndt_7; 792 tmp_ndt_7 = __VERIFIER_nondet_int(); 793 if (tmp_ndt_7) { 794 { 795 t6_st = 1; 796 transmit6(); 797 } 798 } else { 799 800 } 801 } else { 802 803 } 804 if (t7_st == 0) { 805 int tmp_ndt_8; 806 tmp_ndt_8 = __VERIFIER_nondet_int(); 807 if (tmp_ndt_8) { 808 { 809 t7_st = 1; 810 transmit7(); 811 } 812 } else { 813 814 } 815 } else { 816 817 } 818 if (t8_st == 0) { 819 int tmp_ndt_9; 820 tmp_ndt_9 = __VERIFIER_nondet_int(); 821 if (tmp_ndt_9) { 822 { 823 t8_st = 1; 824 transmit8(); 825 } 826 } else { 827 828 } 829 } else { 830 831 } 832 } 833 while_9_break: /* CIL Label */ ; 834 } 835 836 return; 837} 838} 839void fire_delta_events(void) 840{ 841 842 { 843 if (M_E == 0) { 844 M_E = 1; 845 } else { 846 847 } 848 if (T1_E == 0) { 849 T1_E = 1; 850 } else { 851 852 } 853 if (T2_E == 0) { 854 T2_E = 1; 855 } else { 856 857 } 858 if (T3_E == 0) { 859 T3_E = 1; 860 } else { 861 862 } 863 if (T4_E == 0) { 864 T4_E = 1; 865 } else { 866 867 } 868 if (T5_E == 0) { 869 T5_E = 1; 870 } else { 871 872 } 873 if (T6_E == 0) { 874 T6_E = 1; 875 } else { 876 877 } 878 if (T7_E == 0) { 879 T7_E = 1; 880 } else { 881 882 } 883 if (T8_E == 0) { 884 T8_E = 1; 885 } else { 886 887 } 888 if (E_M == 0) { 889 E_M = 1; 890 } else { 891 892 } 893 if (E_1 == 0) { 894 E_1 = 1; 895 } else { 896 897 } 898 if (E_2 == 0) { 899 E_2 = 1; 900 } else { 901 902 } 903 if (E_3 == 0) { 904 E_3 = 1; 905 } else { 906 907 } 908 if (E_4 == 0) { 909 E_4 = 1; 910 } else { 911 912 } 913 if (E_5 == 0) { 914 E_5 = 1; 915 } else { 916 917 } 918 if (E_6 == 0) { 919 E_6 = 1; 920 } else { 921 922 } 923 if (E_7 == 0) { 924 E_7 = 1; 925 } else { 926 927 } 928 if (E_8 == 0) { 929 E_8 = 1; 930 } else { 931 932 } 933 934 return; 935} 936} 937void reset_delta_events(void) 938{ 939 940 { 941 if (M_E == 1) { 942 M_E = 2; 943 } else { 944 945 } 946 if (T1_E == 1) { 947 T1_E = 2; 948 } else { 949 950 } 951 if (T2_E == 1) { 952 T2_E = 2; 953 } else { 954 955 } 956 if (T3_E == 1) { 957 T3_E = 2; 958 } else { 959 960 } 961 if (T4_E == 1) { 962 T4_E = 2; 963 } else { 964 965 } 966 if (T5_E == 1) { 967 T5_E = 2; 968 } else { 969 970 } 971 if (T6_E == 1) { 972 T6_E = 2; 973 } else { 974 975 } 976 if (T7_E == 1) { 977 T7_E = 2; 978 } else { 979 980 } 981 if (T8_E == 1) { 982 T8_E = 2; 983 } else { 984 985 } 986 if (E_M == 1) { 987 E_M = 2; 988 } else { 989 990 } 991 if (E_1 == 1) { 992 E_1 = 2; 993 } else { 994 995 } 996 if (E_2 == 1) { 997 E_2 = 2; 998 } else { 999 1000 } 1001 if (E_3 == 1) { 1002 E_3 = 2; 1003 } else { 1004 1005 } 1006 if (E_4 == 1) { 1007 E_4 = 2; 1008 } else { 1009 1010 } 1011 if (E_5 == 1) { 1012 E_5 = 2; 1013 } else { 1014 1015 } 1016 if (E_6 == 1) { 1017 E_6 = 2; 1018 } else { 1019 1020 } 1021 if (E_7 == 1) { 1022 E_7 = 2; 1023 } else { 1024 1025 } 1026 if (E_8 == 1) { 1027 E_8 = 2; 1028 } else { 1029 1030 } 1031 1032 return; 1033} 1034} 1035void activate_threads(void) 1036{ int tmp ; 1037 int tmp___0 ; 1038 int tmp___1 ; 1039 int tmp___2 ; 1040 int tmp___3 ; 1041 int tmp___4 ; 1042 int tmp___5 ; 1043 int tmp___6 ; 1044 int tmp___7 ; 1045 1046 { 1047 { 1048 tmp = is_master_triggered(); 1049 } 1050 if (tmp) { 1051 m_st = 0; 1052 } else { 1053 1054 } 1055 { 1056 tmp___0 = is_transmit1_triggered(); 1057 } 1058 if (tmp___0) { 1059 t1_st = 0; 1060 } else { 1061 1062 } 1063 { 1064 tmp___1 = is_transmit2_triggered(); 1065 } 1066 if (tmp___1) { 1067 t2_st = 0; 1068 } else { 1069 1070 } 1071 { 1072 tmp___2 = is_transmit3_triggered(); 1073 } 1074 if (tmp___2) { 1075 t3_st = 0; 1076 } else { 1077 1078 } 1079 { 1080 tmp___3 = is_transmit4_triggered(); 1081 } 1082 if (tmp___3) { 1083 t4_st = 0; 1084 } else { 1085 1086 } 1087 { 1088 tmp___4 = is_transmit5_triggered(); 1089 } 1090 if (tmp___4) { 1091 t5_st = 0; 1092 } else { 1093 1094 } 1095 { 1096 tmp___5 = is_transmit6_triggered(); 1097 } 1098 if (tmp___5) { 1099 t6_st = 0; 1100 } else { 1101 1102 } 1103 { 1104 tmp___6 = is_transmit7_triggered(); 1105 } 1106 if (tmp___6) { 1107 t7_st = 0; 1108 } else { 1109 1110 } 1111 { 1112 tmp___7 = is_transmit8_triggered(); 1113 } 1114 if (tmp___7) { 1115 t8_st = 0; 1116 } else { 1117 1118 } 1119 1120 return; 1121} 1122} 1123void immediate_notify(void) 1124{ 1125 1126 { 1127 { 1128 activate_threads(); 1129 } 1130 1131 return; 1132} 1133} 1134void fire_time_events(void) 1135{ 1136 1137 { 1138 M_E = 1; 1139 1140 return; 1141} 1142} 1143void reset_time_events(void) 1144{ 1145 1146 { 1147 if (M_E == 1) { 1148 M_E = 2; 1149 } else { 1150 1151 } 1152 if (T1_E == 1) { 1153 T1_E = 2; 1154 } else { 1155 1156 } 1157 if (T2_E == 1) { 1158 T2_E = 2; 1159 } else { 1160 1161 } 1162 if (T3_E == 1) { 1163 T3_E = 2; 1164 } else { 1165 1166 } 1167 if (T4_E == 1) { 1168 T4_E = 2; 1169 } else { 1170 1171 } 1172 if (T5_E == 1) { 1173 T5_E = 2; 1174 } else { 1175 1176 } 1177 if (T6_E == 1) { 1178 T6_E = 2; 1179 } else { 1180 1181 } 1182 if (T7_E == 1) { 1183 T7_E = 2; 1184 } else { 1185 1186 } 1187 if (T8_E == 1) { 1188 T8_E = 2; 1189 } else { 1190 1191 } 1192 if (E_M == 1) { 1193 E_M = 2; 1194 } else { 1195 1196 } 1197 if (E_1 == 1) { 1198 E_1 = 2; 1199 } else { 1200 1201 } 1202 if (E_2 == 1) { 1203 E_2 = 2; 1204 } else { 1205 1206 } 1207 if (E_3 == 1) { 1208 E_3 = 2; 1209 } else { 1210 1211 } 1212 if (E_4 == 1) { 1213 E_4 = 2; 1214 } else { 1215 1216 } 1217 if (E_5 == 1) { 1218 E_5 = 2; 1219 } else { 1220 1221 } 1222 if (E_6 == 1) { 1223 E_6 = 2; 1224 } else { 1225 1226 } 1227 if (E_7 == 1) { 1228 E_7 = 2; 1229 } else { 1230 1231 } 1232 if (E_8 == 1) { 1233 E_8 = 2; 1234 } else { 1235 1236 } 1237 1238 return; 1239} 1240} 1241void init_model(void) 1242{ 1243 1244 { 1245 m_i = 1; 1246 t1_i = 1; 1247 t2_i = 1; 1248 t3_i = 1; 1249 t4_i = 1; 1250 t5_i = 1; 1251 t6_i = 1; 1252 t7_i = 1; 1253 t8_i = 1; 1254 1255 return; 1256} 1257} 1258int stop_simulation(void) 1259{ int tmp ; 1260 int __retres2 ; 1261 1262 { 1263 { 1264 tmp = exists_runnable_thread(); 1265 } 1266 if (tmp) { 1267 __retres2 = 0; 1268 goto return_label; 1269 } else { 1270 1271 } 1272 __retres2 = 1; 1273 return_label: /* CIL Label */ 1274 return (__retres2); 1275} 1276} 1277void start_simulation(void) 1278{ int kernel_st ; 1279 int tmp ; 1280 int tmp___0 ; 1281 1282 { 1283 { 1284 kernel_st = 0; 1285 update_channels(); 1286 init_threads(); 1287 fire_delta_events(); 1288 activate_threads(); 1289 reset_delta_events(); 1290 } 1291 { 1292 while (1) { 1293 while_10_continue: /* CIL Label */ ; 1294 { 1295 kernel_st = 1; 1296 eval(); 1297 } 1298 { 1299 kernel_st = 2; 1300 update_channels(); 1301 } 1302 { 1303 kernel_st = 3; 1304 fire_delta_events(); 1305 activate_threads(); 1306 reset_delta_events(); 1307 } 1308 { 1309 tmp = exists_runnable_thread(); 1310 } 1311 if (tmp == 0) { 1312 { 1313 kernel_st = 4; 1314 fire_time_events(); 1315 activate_threads(); 1316 reset_time_events(); 1317 } 1318 } else { 1319 1320 } 1321 { 1322 tmp___0 = stop_simulation(); 1323 } 1324 if (tmp___0) { 1325 goto while_10_break; 1326 } else { 1327 1328 } 1329 } 1330 while_10_break: /* CIL Label */ ; 1331 } 1332 1333 return; 1334} 1335} 1336int main(void) 1337{ int __retres1 ; 1338 1339 { 1340 { 1341 init_model(); 1342 start_simulation(); 1343 } 1344 __retres1 = 0; 1345 return (__retres1); 1346} 1347}