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.11_unsafe.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 t9_pc = 0; 23int t10_pc = 0; 24int t11_pc = 0; 25int m_st ; 26int t1_st ; 27int t2_st ; 28int t3_st ; 29int t4_st ; 30int t5_st ; 31int t6_st ; 32int t7_st ; 33int t8_st ; 34int t9_st ; 35int t10_st ; 36int t11_st ; 37int m_i ; 38int t1_i ; 39int t2_i ; 40int t3_i ; 41int t4_i ; 42int t5_i ; 43int t6_i ; 44int t7_i ; 45int t8_i ; 46int t9_i ; 47int t10_i ; 48int t11_i ; 49int M_E = 2; 50int T1_E = 2; 51int T2_E = 2; 52int T3_E = 2; 53int T4_E = 2; 54int T5_E = 2; 55int T6_E = 2; 56int T7_E = 2; 57int T8_E = 2; 58int T9_E = 2; 59int T10_E = 2; 60int T11_E = 2; 61int E_M = 2; 62int E_1 = 2; 63int E_2 = 2; 64int E_3 = 2; 65int E_4 = 2; 66int E_5 = 2; 67int E_6 = 2; 68int E_7 = 2; 69int E_8 = 2; 70int E_9 = 2; 71int E_10 = 2; 72int E_11 = 2; 73int is_master_triggered(void) ; 74int is_transmit1_triggered(void) ; 75int is_transmit2_triggered(void) ; 76int is_transmit3_triggered(void) ; 77int is_transmit4_triggered(void) ; 78int is_transmit5_triggered(void) ; 79int is_transmit6_triggered(void) ; 80int is_transmit7_triggered(void) ; 81int is_transmit8_triggered(void) ; 82int is_transmit9_triggered(void) ; 83int is_transmit10_triggered(void) ; 84int is_transmit11_triggered(void) ; 85void immediate_notify(void) ; 86int token ; 87int __VERIFIER_nondet_int() ; 88int local ; 89void master(void) 90{ 91int tmp_var ; 92 { 93 if (m_pc == 0) { 94 goto M_ENTRY; 95 } else { 96 if (m_pc == 1) { 97 goto M_WAIT; 98 } else { 99 100 } 101 } 102 M_ENTRY: ; 103 { 104 while (1) { 105 while_0_continue: /* CIL Label */ ; 106 { 107 token = __VERIFIER_nondet_int(); 108 local = token; 109 E_1 = 1; 110 immediate_notify(); 111 E_1 = 2; 112 m_pc = 1; 113 m_st = 2; 114 } 115 116 goto return_label; 117 M_WAIT: ; 118 if (token != local + 11) { 119 { 120 error(); 121 } 122 } else { 123 if(tmp_var <= 5){ 124 if(tmp_var >= 5){ 125 126 } 127 } 128 129 if(tmp_var <= 5){ 130 if(tmp_var >= 5){ 131 if(tmp_var == 5){ 132 error(); 133 } 134 } 135 } 136 } 137 } 138 while_0_break: /* CIL Label */ ; 139 } 140 141 return_label: /* CIL Label */ 142 return; 143} 144} 145void transmit1(void) 146{ 147 148 { 149 if (t1_pc == 0) { 150 goto T1_ENTRY; 151 } else { 152 if (t1_pc == 1) { 153 goto T1_WAIT; 154 } else { 155 156 } 157 } 158 T1_ENTRY: ; 159 { 160 while (1) { 161 while_1_continue: /* CIL Label */ ; 162 t1_pc = 1; 163 t1_st = 2; 164 165 goto return_label; 166 T1_WAIT: 167 { 168 token += 1; 169 E_2 = 1; 170 immediate_notify(); 171 E_2 = 2; 172 } 173 } 174 while_1_break: /* CIL Label */ ; 175 } 176 177 return_label: /* CIL Label */ 178 return; 179} 180} 181void transmit2(void) 182{ 183 184 { 185 if (t2_pc == 0) { 186 goto T2_ENTRY; 187 } else { 188 if (t2_pc == 1) { 189 goto T2_WAIT; 190 } else { 191 192 } 193 } 194 T2_ENTRY: ; 195 { 196 while (1) { 197 while_2_continue: /* CIL Label */ ; 198 t2_pc = 1; 199 t2_st = 2; 200 201 goto return_label; 202 T2_WAIT: 203 { 204 token += 1; 205 E_3 = 1; 206 immediate_notify(); 207 E_3 = 2; 208 } 209 } 210 while_2_break: /* CIL Label */ ; 211 } 212 213 return_label: /* CIL Label */ 214 return; 215} 216} 217void transmit3(void) 218{ 219 220 { 221 if (t3_pc == 0) { 222 goto T3_ENTRY; 223 } else { 224 if (t3_pc == 1) { 225 goto T3_WAIT; 226 } else { 227 228 } 229 } 230 T3_ENTRY: ; 231 { 232 while (1) { 233 while_3_continue: /* CIL Label */ ; 234 t3_pc = 1; 235 t3_st = 2; 236 237 goto return_label; 238 T3_WAIT: 239 { 240 token += 1; 241 E_4 = 1; 242 immediate_notify(); 243 E_4 = 2; 244 } 245 } 246 while_3_break: /* CIL Label */ ; 247 } 248 249 return_label: /* CIL Label */ 250 return; 251} 252} 253void transmit4(void) 254{ 255 256 { 257 if (t4_pc == 0) { 258 goto T4_ENTRY; 259 } else { 260 if (t4_pc == 1) { 261 goto T4_WAIT; 262 } else { 263 264 } 265 } 266 T4_ENTRY: ; 267 { 268 while (1) { 269 while_4_continue: /* CIL Label */ ; 270 t4_pc = 1; 271 t4_st = 2; 272 273 goto return_label; 274 T4_WAIT: 275 { 276 token += 1; 277 E_5 = 1; 278 immediate_notify(); 279 E_5 = 2; 280 } 281 } 282 while_4_break: /* CIL Label */ ; 283 } 284 285 return_label: /* CIL Label */ 286 return; 287} 288} 289void transmit5(void) 290{ 291 292 { 293 if (t5_pc == 0) { 294 goto T5_ENTRY; 295 } else { 296 if (t5_pc == 1) { 297 goto T5_WAIT; 298 } else { 299 300 } 301 } 302 T5_ENTRY: ; 303 { 304 while (1) { 305 while_5_continue: /* CIL Label */ ; 306 t5_pc = 1; 307 t5_st = 2; 308 309 goto return_label; 310 T5_WAIT: 311 { 312 token += 1; 313 E_6 = 1; 314 immediate_notify(); 315 E_6 = 2; 316 } 317 } 318 while_5_break: /* CIL Label */ ; 319 } 320 321 return_label: /* CIL Label */ 322 return; 323} 324} 325void transmit6(void) 326{ 327 328 { 329 if (t6_pc == 0) { 330 goto T6_ENTRY; 331 } else { 332 if (t6_pc == 1) { 333 goto T6_WAIT; 334 } else { 335 336 } 337 } 338 T6_ENTRY: ; 339 { 340 while (1) { 341 while_6_continue: /* CIL Label */ ; 342 t6_pc = 1; 343 t6_st = 2; 344 345 goto return_label; 346 T6_WAIT: 347 { 348 token += 1; 349 E_7 = 1; 350 immediate_notify(); 351 E_7 = 2; 352 } 353 } 354 while_6_break: /* CIL Label */ ; 355 } 356 357 return_label: /* CIL Label */ 358 return; 359} 360} 361void transmit7(void) 362{ 363 364 { 365 if (t7_pc == 0) { 366 goto T7_ENTRY; 367 } else { 368 if (t7_pc == 1) { 369 goto T7_WAIT; 370 } else { 371 372 } 373 } 374 T7_ENTRY: ; 375 { 376 while (1) { 377 while_7_continue: /* CIL Label */ ; 378 t7_pc = 1; 379 t7_st = 2; 380 381 goto return_label; 382 T7_WAIT: 383 { 384 token += 1; 385 E_8 = 1; 386 immediate_notify(); 387 E_8 = 2; 388 } 389 } 390 while_7_break: /* CIL Label */ ; 391 } 392 393 return_label: /* CIL Label */ 394 return; 395} 396} 397void transmit8(void) 398{ 399 400 { 401 if (t8_pc == 0) { 402 goto T8_ENTRY; 403 } else { 404 if (t8_pc == 1) { 405 goto T8_WAIT; 406 } else { 407 408 } 409 } 410 T8_ENTRY: ; 411 { 412 while (1) { 413 while_8_continue: /* CIL Label */ ; 414 t8_pc = 1; 415 t8_st = 2; 416 417 goto return_label; 418 T8_WAIT: 419 { 420 token += 1; 421 E_9 = 1; 422 immediate_notify(); 423 E_9 = 2; 424 } 425 } 426 while_8_break: /* CIL Label */ ; 427 } 428 429 return_label: /* CIL Label */ 430 return; 431} 432} 433void transmit9(void) 434{ 435 436 { 437 if (t9_pc == 0) { 438 goto T9_ENTRY; 439 } else { 440 if (t9_pc == 1) { 441 goto T9_WAIT; 442 } else { 443 444 } 445 } 446 T9_ENTRY: ; 447 { 448 while (1) { 449 while_9_continue: /* CIL Label */ ; 450 t9_pc = 1; 451 t9_st = 2; 452 453 goto return_label; 454 T9_WAIT: 455 { 456 token += 1; 457 E_10 = 1; 458 immediate_notify(); 459 E_10 = 2; 460 } 461 } 462 while_9_break: /* CIL Label */ ; 463 } 464 465 return_label: /* CIL Label */ 466 return; 467} 468} 469void transmit10(void) 470{ 471 472 { 473 if (t10_pc == 0) { 474 goto T10_ENTRY; 475 } else { 476 if (t10_pc == 1) { 477 goto T10_WAIT; 478 } else { 479 480 } 481 } 482 T10_ENTRY: ; 483 { 484 while (1) { 485 while_10_continue: /* CIL Label */ ; 486 t10_pc = 1; 487 t10_st = 2; 488 489 goto return_label; 490 T10_WAIT: 491 { 492 token += 1; 493 E_11 = 1; 494 immediate_notify(); 495 E_11 = 2; 496 } 497 } 498 while_10_break: /* CIL Label */ ; 499 } 500 501 return_label: /* CIL Label */ 502 return; 503} 504} 505void transmit11(void) 506{ 507 508 { 509 if (t11_pc == 0) { 510 goto T11_ENTRY; 511 } else { 512 if (t11_pc == 1) { 513 goto T11_WAIT; 514 } else { 515 516 } 517 } 518 T11_ENTRY: ; 519 { 520 while (1) { 521 while_11_continue: /* CIL Label */ ; 522 t11_pc = 1; 523 t11_st = 2; 524 525 goto return_label; 526 T11_WAIT: 527 { 528 token += 1; 529 E_M = 1; 530 immediate_notify(); 531 E_M = 2; 532 } 533 } 534 while_11_break: /* CIL Label */ ; 535 } 536 537 return_label: /* CIL Label */ 538 return; 539} 540} 541int is_master_triggered(void) 542{ int __retres1 ; 543 544 { 545 if (m_pc == 1) { 546 if (E_M == 1) { 547 __retres1 = 1; 548 goto return_label; 549 } else { 550 551 } 552 } else { 553 554 } 555 __retres1 = 0; 556 return_label: /* CIL Label */ 557 return (__retres1); 558} 559} 560int is_transmit1_triggered(void) 561{ int __retres1 ; 562 563 { 564 if (t1_pc == 1) { 565 if (E_1 == 1) { 566 __retres1 = 1; 567 goto return_label; 568 } else { 569 570 } 571 } else { 572 573 } 574 __retres1 = 0; 575 return_label: /* CIL Label */ 576 return (__retres1); 577} 578} 579int is_transmit2_triggered(void) 580{ int __retres1 ; 581 582 { 583 if (t2_pc == 1) { 584 if (E_2 == 1) { 585 __retres1 = 1; 586 goto return_label; 587 } else { 588 589 } 590 } else { 591 592 } 593 __retres1 = 0; 594 return_label: /* CIL Label */ 595 return (__retres1); 596} 597} 598int is_transmit3_triggered(void) 599{ int __retres1 ; 600 601 { 602 if (t3_pc == 1) { 603 if (E_3 == 1) { 604 __retres1 = 1; 605 goto return_label; 606 } else { 607 608 } 609 } else { 610 611 } 612 __retres1 = 0; 613 return_label: /* CIL Label */ 614 return (__retres1); 615} 616} 617int is_transmit4_triggered(void) 618{ int __retres1 ; 619 620 { 621 if (t4_pc == 1) { 622 if (E_4 == 1) { 623 __retres1 = 1; 624 goto return_label; 625 } else { 626 627 } 628 } else { 629 630 } 631 __retres1 = 0; 632 return_label: /* CIL Label */ 633 return (__retres1); 634} 635} 636int is_transmit5_triggered(void) 637{ int __retres1 ; 638 639 { 640 if (t5_pc == 1) { 641 if (E_5 == 1) { 642 __retres1 = 1; 643 goto return_label; 644 } else { 645 646 } 647 } else { 648 649 } 650 __retres1 = 0; 651 return_label: /* CIL Label */ 652 return (__retres1); 653} 654} 655int is_transmit6_triggered(void) 656{ int __retres1 ; 657 658 { 659 if (t6_pc == 1) { 660 if (E_6 == 1) { 661 __retres1 = 1; 662 goto return_label; 663 } else { 664 665 } 666 } else { 667 668 } 669 __retres1 = 0; 670 return_label: /* CIL Label */ 671 return (__retres1); 672} 673} 674int is_transmit7_triggered(void) 675{ int __retres1 ; 676 677 { 678 if (t7_pc == 1) { 679 if (E_7 == 1) { 680 __retres1 = 1; 681 goto return_label; 682 } else { 683 684 } 685 } else { 686 687 } 688 __retres1 = 0; 689 return_label: /* CIL Label */ 690 return (__retres1); 691} 692} 693int is_transmit8_triggered(void) 694{ int __retres1 ; 695 696 { 697 if (t8_pc == 1) { 698 if (E_8 == 1) { 699 __retres1 = 1; 700 goto return_label; 701 } else { 702 703 } 704 } else { 705 706 } 707 __retres1 = 0; 708 return_label: /* CIL Label */ 709 return (__retres1); 710} 711} 712int is_transmit9_triggered(void) 713{ int __retres1 ; 714 715 { 716 if (t9_pc == 1) { 717 if (E_9 == 1) { 718 __retres1 = 1; 719 goto return_label; 720 } else { 721 722 } 723 } else { 724 725 } 726 __retres1 = 0; 727 return_label: /* CIL Label */ 728 return (__retres1); 729} 730} 731int is_transmit10_triggered(void) 732{ int __retres1 ; 733 734 { 735 if (t10_pc == 1) { 736 if (E_10 == 1) { 737 __retres1 = 1; 738 goto return_label; 739 } else { 740 741 } 742 } else { 743 744 } 745 __retres1 = 0; 746 return_label: /* CIL Label */ 747 return (__retres1); 748} 749} 750int is_transmit11_triggered(void) 751{ int __retres1 ; 752 753 { 754 if (t11_pc == 1) { 755 if (E_11 == 1) { 756 __retres1 = 1; 757 goto return_label; 758 } else { 759 760 } 761 } else { 762 763 } 764 __retres1 = 0; 765 return_label: /* CIL Label */ 766 return (__retres1); 767} 768} 769void update_channels(void) 770{ 771 772 { 773 774 return; 775} 776} 777void init_threads(void) 778{ 779 780 { 781 if (m_i == 1) { 782 m_st = 0; 783 } else { 784 m_st = 2; 785 } 786 if (t1_i == 1) { 787 t1_st = 0; 788 } else { 789 t1_st = 2; 790 } 791 if (t2_i == 1) { 792 t2_st = 0; 793 } else { 794 t2_st = 2; 795 } 796 if (t3_i == 1) { 797 t3_st = 0; 798 } else { 799 t3_st = 2; 800 } 801 if (t4_i == 1) { 802 t4_st = 0; 803 } else { 804 t4_st = 2; 805 } 806 if (t5_i == 1) { 807 t5_st = 0; 808 } else { 809 t5_st = 2; 810 } 811 if (t6_i == 1) { 812 t6_st = 0; 813 } else { 814 t6_st = 2; 815 } 816 if (t7_i == 1) { 817 t7_st = 0; 818 } else { 819 t7_st = 2; 820 } 821 if (t8_i == 1) { 822 t8_st = 0; 823 } else { 824 t8_st = 2; 825 } 826 if (t9_i == 1) { 827 t9_st = 0; 828 } else { 829 t9_st = 2; 830 } 831 if (t10_i == 1) { 832 t10_st = 0; 833 } else { 834 t10_st = 2; 835 } 836 if (t11_i == 1) { 837 t11_st = 0; 838 } else { 839 t11_st = 2; 840 } 841 842 return; 843} 844} 845int exists_runnable_thread(void) 846{ int __retres1 ; 847 848 { 849 if (m_st == 0) { 850 __retres1 = 1; 851 goto return_label; 852 } else { 853 if (t1_st == 0) { 854 __retres1 = 1; 855 goto return_label; 856 } else { 857 if (t2_st == 0) { 858 __retres1 = 1; 859 goto return_label; 860 } else { 861 if (t3_st == 0) { 862 __retres1 = 1; 863 goto return_label; 864 } else { 865 if (t4_st == 0) { 866 __retres1 = 1; 867 goto return_label; 868 } else { 869 if (t5_st == 0) { 870 __retres1 = 1; 871 goto return_label; 872 } else { 873 if (t6_st == 0) { 874 __retres1 = 1; 875 goto return_label; 876 } else { 877 if (t7_st == 0) { 878 __retres1 = 1; 879 goto return_label; 880 } else { 881 if (t8_st == 0) { 882 __retres1 = 1; 883 goto return_label; 884 } else { 885 if (t9_st == 0) { 886 __retres1 = 1; 887 goto return_label; 888 } else { 889 if (t10_st == 0) { 890 __retres1 = 1; 891 goto return_label; 892 } else { 893 if (t11_st == 0) { 894 __retres1 = 1; 895 goto return_label; 896 } else { 897 898 } 899 } 900 } 901 } 902 } 903 } 904 } 905 } 906 } 907 } 908 } 909 } 910 __retres1 = 0; 911 return_label: /* CIL Label */ 912 return (__retres1); 913} 914} 915void eval(void) 916{ 917 int tmp ; 918 919 { 920 { 921 while (1) { 922 while_12_continue: /* CIL Label */ ; 923 { 924 tmp = exists_runnable_thread(); 925 } 926 if (tmp) { 927 928 } else { 929 goto while_12_break; 930 } 931 if (m_st == 0) { 932 int tmp_ndt_1; 933 tmp_ndt_1 = __VERIFIER_nondet_int(); 934 if (tmp_ndt_1) { 935 { 936 m_st = 1; 937 master(); 938 } 939 } else { 940 941 } 942 } else { 943 944 } 945 if (t1_st == 0) { 946 int tmp_ndt_2; 947 tmp_ndt_2 = __VERIFIER_nondet_int(); 948 if (tmp_ndt_2) { 949 { 950 t1_st = 1; 951 transmit1(); 952 } 953 } else { 954 955 } 956 } else { 957 958 } 959 if (t2_st == 0) { 960 int tmp_ndt_3; 961 tmp_ndt_3 = __VERIFIER_nondet_int(); 962 if (tmp_ndt_3) { 963 { 964 t2_st = 1; 965 transmit2(); 966 } 967 } else { 968 969 } 970 } else { 971 972 } 973 if (t3_st == 0) { 974 int tmp_ndt_4; 975 tmp_ndt_4 = __VERIFIER_nondet_int(); 976 if (tmp_ndt_4) { 977 { 978 t3_st = 1; 979 transmit3(); 980 } 981 } else { 982 983 } 984 } else { 985 986 } 987 if (t4_st == 0) { 988 int tmp_ndt_5; 989 tmp_ndt_5 = __VERIFIER_nondet_int(); 990 if (tmp_ndt_5) { 991 { 992 t4_st = 1; 993 transmit4(); 994 } 995 } else { 996 997 } 998 } else { 999 1000 } 1001 if (t5_st == 0) { 1002 int tmp_ndt_6; 1003 tmp_ndt_6 = __VERIFIER_nondet_int(); 1004 if (tmp_ndt_6) { 1005 { 1006 t5_st = 1; 1007 transmit5(); 1008 } 1009 } else { 1010 1011 } 1012 } else { 1013 1014 } 1015 if (t6_st == 0) { 1016 int tmp_ndt_7; 1017 tmp_ndt_7 = __VERIFIER_nondet_int(); 1018 if (tmp_ndt_7) { 1019 { 1020 t6_st = 1; 1021 transmit6(); 1022 } 1023 } else { 1024 1025 } 1026 } else { 1027 1028 } 1029 if (t7_st == 0) { 1030 int tmp_ndt_8; 1031 tmp_ndt_8 = __VERIFIER_nondet_int(); 1032 if (tmp_ndt_8) { 1033 { 1034 t7_st = 1; 1035 transmit7(); 1036 } 1037 } else { 1038 1039 } 1040 } else { 1041 1042 } 1043 if (t8_st == 0) { 1044 int tmp_ndt_9; 1045 tmp_ndt_9 = __VERIFIER_nondet_int(); 1046 if (tmp_ndt_9) { 1047 { 1048 t8_st = 1; 1049 transmit8(); 1050 } 1051 } else { 1052 1053 } 1054 } else { 1055 1056 } 1057 if (t9_st == 0) { 1058 int tmp_ndt_10; 1059 tmp_ndt_10 = __VERIFIER_nondet_int(); 1060 if (tmp_ndt_10) { 1061 { 1062 t9_st = 1; 1063 transmit9(); 1064 } 1065 } else { 1066 1067 } 1068 } else { 1069 1070 } 1071 if (t10_st == 0) { 1072 int tmp_ndt_11; 1073 tmp_ndt_11 = __VERIFIER_nondet_int(); 1074 if (tmp_ndt_11) { 1075 { 1076 t10_st = 1; 1077 transmit10(); 1078 } 1079 } else { 1080 1081 } 1082 } else { 1083 1084 } 1085 if (t11_st == 0) { 1086 int tmp_ndt_12; 1087 tmp_ndt_12 = __VERIFIER_nondet_int(); 1088 if (tmp_ndt_12) { 1089 { 1090 t11_st = 1; 1091 transmit11(); 1092 } 1093 } else { 1094 1095 } 1096 } else { 1097 1098 } 1099 } 1100 while_12_break: /* CIL Label */ ; 1101 } 1102 1103 return; 1104} 1105} 1106void fire_delta_events(void) 1107{ 1108 1109 { 1110 if (M_E == 0) { 1111 M_E = 1; 1112 } else { 1113 1114 } 1115 if (T1_E == 0) { 1116 T1_E = 1; 1117 } else { 1118 1119 } 1120 if (T2_E == 0) { 1121 T2_E = 1; 1122 } else { 1123 1124 } 1125 if (T3_E == 0) { 1126 T3_E = 1; 1127 } else { 1128 1129 } 1130 if (T4_E == 0) { 1131 T4_E = 1; 1132 } else { 1133 1134 } 1135 if (T5_E == 0) { 1136 T5_E = 1; 1137 } else { 1138 1139 } 1140 if (T6_E == 0) { 1141 T6_E = 1; 1142 } else { 1143 1144 } 1145 if (T7_E == 0) { 1146 T7_E = 1; 1147 } else { 1148 1149 } 1150 if (T8_E == 0) { 1151 T8_E = 1; 1152 } else { 1153 1154 } 1155 if (T9_E == 0) { 1156 T9_E = 1; 1157 } else { 1158 1159 } 1160 if (T10_E == 0) { 1161 T10_E = 1; 1162 } else { 1163 1164 } 1165 if (T11_E == 0) { 1166 T11_E = 1; 1167 } else { 1168 1169 } 1170 if (E_M == 0) { 1171 E_M = 1; 1172 } else { 1173 1174 } 1175 if (E_1 == 0) { 1176 E_1 = 1; 1177 } else { 1178 1179 } 1180 if (E_2 == 0) { 1181 E_2 = 1; 1182 } else { 1183 1184 } 1185 if (E_3 == 0) { 1186 E_3 = 1; 1187 } else { 1188 1189 } 1190 if (E_4 == 0) { 1191 E_4 = 1; 1192 } else { 1193 1194 } 1195 if (E_5 == 0) { 1196 E_5 = 1; 1197 } else { 1198 1199 } 1200 if (E_6 == 0) { 1201 E_6 = 1; 1202 } else { 1203 1204 } 1205 if (E_7 == 0) { 1206 E_7 = 1; 1207 } else { 1208 1209 } 1210 if (E_8 == 0) { 1211 E_8 = 1; 1212 } else { 1213 1214 } 1215 if (E_9 == 0) { 1216 E_9 = 1; 1217 } else { 1218 1219 } 1220 if (E_10 == 0) { 1221 E_10 = 1; 1222 } else { 1223 1224 } 1225 if (E_11 == 0) { 1226 E_11 = 1; 1227 } else { 1228 1229 } 1230 1231 return; 1232} 1233} 1234void reset_delta_events(void) 1235{ 1236 1237 { 1238 if (M_E == 1) { 1239 M_E = 2; 1240 } else { 1241 1242 } 1243 if (T1_E == 1) { 1244 T1_E = 2; 1245 } else { 1246 1247 } 1248 if (T2_E == 1) { 1249 T2_E = 2; 1250 } else { 1251 1252 } 1253 if (T3_E == 1) { 1254 T3_E = 2; 1255 } else { 1256 1257 } 1258 if (T4_E == 1) { 1259 T4_E = 2; 1260 } else { 1261 1262 } 1263 if (T5_E == 1) { 1264 T5_E = 2; 1265 } else { 1266 1267 } 1268 if (T6_E == 1) { 1269 T6_E = 2; 1270 } else { 1271 1272 } 1273 if (T7_E == 1) { 1274 T7_E = 2; 1275 } else { 1276 1277 } 1278 if (T8_E == 1) { 1279 T8_E = 2; 1280 } else { 1281 1282 } 1283 if (T9_E == 1) { 1284 T9_E = 2; 1285 } else { 1286 1287 } 1288 if (T10_E == 1) { 1289 T10_E = 2; 1290 } else { 1291 1292 } 1293 if (T11_E == 1) { 1294 T11_E = 2; 1295 } else { 1296 1297 } 1298 if (E_M == 1) { 1299 E_M = 2; 1300 } else { 1301 1302 } 1303 if (E_1 == 1) { 1304 E_1 = 2; 1305 } else { 1306 1307 } 1308 if (E_2 == 1) { 1309 E_2 = 2; 1310 } else { 1311 1312 } 1313 if (E_3 == 1) { 1314 E_3 = 2; 1315 } else { 1316 1317 } 1318 if (E_4 == 1) { 1319 E_4 = 2; 1320 } else { 1321 1322 } 1323 if (E_5 == 1) { 1324 E_5 = 2; 1325 } else { 1326 1327 } 1328 if (E_6 == 1) { 1329 E_6 = 2; 1330 } else { 1331 1332 } 1333 if (E_7 == 1) { 1334 E_7 = 2; 1335 } else { 1336 1337 } 1338 if (E_8 == 1) { 1339 E_8 = 2; 1340 } else { 1341 1342 } 1343 if (E_9 == 1) { 1344 E_9 = 2; 1345 } else { 1346 1347 } 1348 if (E_10 == 1) { 1349 E_10 = 2; 1350 } else { 1351 1352 } 1353 if (E_11 == 1) { 1354 E_11 = 2; 1355 } else { 1356 1357 } 1358 1359 return; 1360} 1361} 1362void activate_threads(void) 1363{ int tmp ; 1364 int tmp___0 ; 1365 int tmp___1 ; 1366 int tmp___2 ; 1367 int tmp___3 ; 1368 int tmp___4 ; 1369 int tmp___5 ; 1370 int tmp___6 ; 1371 int tmp___7 ; 1372 int tmp___8 ; 1373 int tmp___9 ; 1374 int tmp___10 ; 1375 1376 { 1377 { 1378 tmp = is_master_triggered(); 1379 } 1380 if (tmp) { 1381 m_st = 0; 1382 } else { 1383 1384 } 1385 { 1386 tmp___0 = is_transmit1_triggered(); 1387 } 1388 if (tmp___0) { 1389 t1_st = 0; 1390 } else { 1391 1392 } 1393 { 1394 tmp___1 = is_transmit2_triggered(); 1395 } 1396 if (tmp___1) { 1397 t2_st = 0; 1398 } else { 1399 1400 } 1401 { 1402 tmp___2 = is_transmit3_triggered(); 1403 } 1404 if (tmp___2) { 1405 t3_st = 0; 1406 } else { 1407 1408 } 1409 { 1410 tmp___3 = is_transmit4_triggered(); 1411 } 1412 if (tmp___3) { 1413 t4_st = 0; 1414 } else { 1415 1416 } 1417 { 1418 tmp___4 = is_transmit5_triggered(); 1419 } 1420 if (tmp___4) { 1421 t5_st = 0; 1422 } else { 1423 1424 } 1425 { 1426 tmp___5 = is_transmit6_triggered(); 1427 } 1428 if (tmp___5) { 1429 t6_st = 0; 1430 } else { 1431 1432 } 1433 { 1434 tmp___6 = is_transmit7_triggered(); 1435 } 1436 if (tmp___6) { 1437 t7_st = 0; 1438 } else { 1439 1440 } 1441 { 1442 tmp___7 = is_transmit8_triggered(); 1443 } 1444 if (tmp___7) { 1445 t8_st = 0; 1446 } else { 1447 1448 } 1449 { 1450 tmp___8 = is_transmit9_triggered(); 1451 } 1452 if (tmp___8) { 1453 t9_st = 0; 1454 } else { 1455 1456 } 1457 { 1458 tmp___9 = is_transmit10_triggered(); 1459 } 1460 if (tmp___9) { 1461 t10_st = 0; 1462 } else { 1463 1464 } 1465 { 1466 tmp___10 = is_transmit11_triggered(); 1467 } 1468 if (tmp___10) { 1469 t11_st = 0; 1470 } else { 1471 1472 } 1473 1474 return; 1475} 1476} 1477void immediate_notify(void) 1478{ 1479 1480 { 1481 { 1482 activate_threads(); 1483 } 1484 1485 return; 1486} 1487} 1488void fire_time_events(void) 1489{ 1490 1491 { 1492 M_E = 1; 1493 1494 return; 1495} 1496} 1497void reset_time_events(void) 1498{ 1499 1500 { 1501 if (M_E == 1) { 1502 M_E = 2; 1503 } else { 1504 1505 } 1506 if (T1_E == 1) { 1507 T1_E = 2; 1508 } else { 1509 1510 } 1511 if (T2_E == 1) { 1512 T2_E = 2; 1513 } else { 1514 1515 } 1516 if (T3_E == 1) { 1517 T3_E = 2; 1518 } else { 1519 1520 } 1521 if (T4_E == 1) { 1522 T4_E = 2; 1523 } else { 1524 1525 } 1526 if (T5_E == 1) { 1527 T5_E = 2; 1528 } else { 1529 1530 } 1531 if (T6_E == 1) { 1532 T6_E = 2; 1533 } else { 1534 1535 } 1536 if (T7_E == 1) { 1537 T7_E = 2; 1538 } else { 1539 1540 } 1541 if (T8_E == 1) { 1542 T8_E = 2; 1543 } else { 1544 1545 } 1546 if (T9_E == 1) { 1547 T9_E = 2; 1548 } else { 1549 1550 } 1551 if (T10_E == 1) { 1552 T10_E = 2; 1553 } else { 1554 1555 } 1556 if (T11_E == 1) { 1557 T11_E = 2; 1558 } else { 1559 1560 } 1561 if (E_M == 1) { 1562 E_M = 2; 1563 } else { 1564 1565 } 1566 if (E_1 == 1) { 1567 E_1 = 2; 1568 } else { 1569 1570 } 1571 if (E_2 == 1) { 1572 E_2 = 2; 1573 } else { 1574 1575 } 1576 if (E_3 == 1) { 1577 E_3 = 2; 1578 } else { 1579 1580 } 1581 if (E_4 == 1) { 1582 E_4 = 2; 1583 } else { 1584 1585 } 1586 if (E_5 == 1) { 1587 E_5 = 2; 1588 } else { 1589 1590 } 1591 if (E_6 == 1) { 1592 E_6 = 2; 1593 } else { 1594 1595 } 1596 if (E_7 == 1) { 1597 E_7 = 2; 1598 } else { 1599 1600 } 1601 if (E_8 == 1) { 1602 E_8 = 2; 1603 } else { 1604 1605 } 1606 if (E_9 == 1) { 1607 E_9 = 2; 1608 } else { 1609 1610 } 1611 if (E_10 == 1) { 1612 E_10 = 2; 1613 } else { 1614 1615 } 1616 if (E_11 == 1) { 1617 E_11 = 2; 1618 } else { 1619 1620 } 1621 1622 return; 1623} 1624} 1625void init_model(void) 1626{ 1627 1628 { 1629 m_i = 1; 1630 t1_i = 1; 1631 t2_i = 1; 1632 t3_i = 1; 1633 t4_i = 1; 1634 t5_i = 1; 1635 t6_i = 1; 1636 t7_i = 1; 1637 t8_i = 1; 1638 t9_i = 1; 1639 t10_i = 1; 1640 t11_i = 1; 1641 1642 return; 1643} 1644} 1645int stop_simulation(void) 1646{ int tmp ; 1647 int __retres2 ; 1648 1649 { 1650 { 1651 tmp = exists_runnable_thread(); 1652 } 1653 if (tmp) { 1654 __retres2 = 0; 1655 goto return_label; 1656 } else { 1657 1658 } 1659 __retres2 = 1; 1660 return_label: /* CIL Label */ 1661 return (__retres2); 1662} 1663} 1664void start_simulation(void) 1665{ int kernel_st ; 1666 int tmp ; 1667 int tmp___0 ; 1668 1669 { 1670 { 1671 kernel_st = 0; 1672 update_channels(); 1673 init_threads(); 1674 fire_delta_events(); 1675 activate_threads(); 1676 reset_delta_events(); 1677 } 1678 { 1679 while (1) { 1680 while_13_continue: /* CIL Label */ ; 1681 { 1682 kernel_st = 1; 1683 eval(); 1684 } 1685 { 1686 kernel_st = 2; 1687 update_channels(); 1688 } 1689 { 1690 kernel_st = 3; 1691 fire_delta_events(); 1692 activate_threads(); 1693 reset_delta_events(); 1694 } 1695 { 1696 tmp = exists_runnable_thread(); 1697 } 1698 if (tmp == 0) { 1699 { 1700 kernel_st = 4; 1701 fire_time_events(); 1702 activate_threads(); 1703 reset_time_events(); 1704 } 1705 } else { 1706 1707 } 1708 { 1709 tmp___0 = stop_simulation(); 1710 } 1711 if (tmp___0) { 1712 goto while_13_break; 1713 } else { 1714 1715 } 1716 } 1717 while_13_break: /* CIL Label */ ; 1718 } 1719 1720 return; 1721} 1722} 1723int main(void) 1724{ int __retres1 ; 1725 1726 { 1727 { 1728 init_model(); 1729 start_simulation(); 1730 } 1731 __retres1 = 0; 1732 return (__retres1); 1733} 1734}