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