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