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.12_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 t9_pc = 0; 23int t10_pc = 0; 24int t11_pc = 0; 25int t12_pc = 0; 26int m_st ; 27int t1_st ; 28int t2_st ; 29int t3_st ; 30int t4_st ; 31int t5_st ; 32int t6_st ; 33int t7_st ; 34int t8_st ; 35int t9_st ; 36int t10_st ; 37int t11_st ; 38int t12_st ; 39int m_i ; 40int t1_i ; 41int t2_i ; 42int t3_i ; 43int t4_i ; 44int t5_i ; 45int t6_i ; 46int t7_i ; 47int t8_i ; 48int t9_i ; 49int t10_i ; 50int t11_i ; 51int t12_i ; 52int M_E = 2; 53int T1_E = 2; 54int T2_E = 2; 55int T3_E = 2; 56int T4_E = 2; 57int T5_E = 2; 58int T6_E = 2; 59int T7_E = 2; 60int T8_E = 2; 61int T9_E = 2; 62int T10_E = 2; 63int T11_E = 2; 64int T12_E = 2; 65int E_M = 2; 66int E_1 = 2; 67int E_2 = 2; 68int E_3 = 2; 69int E_4 = 2; 70int E_5 = 2; 71int E_6 = 2; 72int E_7 = 2; 73int E_8 = 2; 74int E_9 = 2; 75int E_10 = 2; 76int E_11 = 2; 77int E_12 = 2; 78int is_master_triggered(void) ; 79int is_transmit1_triggered(void) ; 80int is_transmit2_triggered(void) ; 81int is_transmit3_triggered(void) ; 82int is_transmit4_triggered(void) ; 83int is_transmit5_triggered(void) ; 84int is_transmit6_triggered(void) ; 85int is_transmit7_triggered(void) ; 86int is_transmit8_triggered(void) ; 87int is_transmit9_triggered(void) ; 88int is_transmit10_triggered(void) ; 89int is_transmit11_triggered(void) ; 90int is_transmit12_triggered(void) ; 91void immediate_notify(void) ; 92int token ; 93int __VERIFIER_nondet_int() ; 94int local ; 95void master(void) 96{ 97 98 { 99 if (m_pc == 0) { 100 goto M_ENTRY; 101 } else { 102 if (m_pc == 1) { 103 goto M_WAIT; 104 } else { 105 106 } 107 } 108 M_ENTRY: ; 109 { 110 while (1) { 111 while_0_continue: /* CIL Label */ ; 112 { 113 token = __VERIFIER_nondet_int(); 114 local = token; 115 E_1 = 1; 116 immediate_notify(); 117 E_1 = 2; 118 m_pc = 1; 119 m_st = 2; 120 } 121 122 goto return_label; 123 M_WAIT: ; 124 if (token != local + 12) { 125 { 126 error(); 127 } 128 } else { 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_11 = 1; 488 immediate_notify(); 489 E_11 = 2; 490 } 491 } 492 while_10_break: /* CIL Label */ ; 493 } 494 495 return_label: /* CIL Label */ 496 return; 497} 498} 499void transmit11(void) 500{ 501 502 { 503 if (t11_pc == 0) { 504 goto T11_ENTRY; 505 } else { 506 if (t11_pc == 1) { 507 goto T11_WAIT; 508 } else { 509 510 } 511 } 512 T11_ENTRY: ; 513 { 514 while (1) { 515 while_11_continue: /* CIL Label */ ; 516 t11_pc = 1; 517 t11_st = 2; 518 519 goto return_label; 520 T11_WAIT: 521 { 522 token += 1; 523 E_12 = 1; 524 immediate_notify(); 525 E_12 = 2; 526 } 527 } 528 while_11_break: /* CIL Label */ ; 529 } 530 531 return_label: /* CIL Label */ 532 return; 533} 534} 535void transmit12(void) 536{ 537 538 { 539 if (t12_pc == 0) { 540 goto T12_ENTRY; 541 } else { 542 if (t12_pc == 1) { 543 goto T12_WAIT; 544 } else { 545 546 } 547 } 548 T12_ENTRY: ; 549 { 550 while (1) { 551 while_12_continue: /* CIL Label */ ; 552 t12_pc = 1; 553 t12_st = 2; 554 555 goto return_label; 556 T12_WAIT: 557 { 558 token += 1; 559 E_M = 1; 560 immediate_notify(); 561 E_M = 2; 562 } 563 } 564 while_12_break: /* CIL Label */ ; 565 } 566 567 return_label: /* CIL Label */ 568 return; 569} 570} 571int is_master_triggered(void) 572{ int __retres1 ; 573 574 { 575 if (m_pc == 1) { 576 if (E_M == 1) { 577 __retres1 = 1; 578 goto return_label; 579 } else { 580 581 } 582 } else { 583 584 } 585 __retres1 = 0; 586 return_label: /* CIL Label */ 587 return (__retres1); 588} 589} 590int is_transmit1_triggered(void) 591{ int __retres1 ; 592 593 { 594 if (t1_pc == 1) { 595 if (E_1 == 1) { 596 __retres1 = 1; 597 goto return_label; 598 } else { 599 600 } 601 } else { 602 603 } 604 __retres1 = 0; 605 return_label: /* CIL Label */ 606 return (__retres1); 607} 608} 609int is_transmit2_triggered(void) 610{ int __retres1 ; 611 612 { 613 if (t2_pc == 1) { 614 if (E_2 == 1) { 615 __retres1 = 1; 616 goto return_label; 617 } else { 618 619 } 620 } else { 621 622 } 623 __retres1 = 0; 624 return_label: /* CIL Label */ 625 return (__retres1); 626} 627} 628int is_transmit3_triggered(void) 629{ int __retres1 ; 630 631 { 632 if (t3_pc == 1) { 633 if (E_3 == 1) { 634 __retres1 = 1; 635 goto return_label; 636 } else { 637 638 } 639 } else { 640 641 } 642 __retres1 = 0; 643 return_label: /* CIL Label */ 644 return (__retres1); 645} 646} 647int is_transmit4_triggered(void) 648{ int __retres1 ; 649 650 { 651 if (t4_pc == 1) { 652 if (E_4 == 1) { 653 __retres1 = 1; 654 goto return_label; 655 } else { 656 657 } 658 } else { 659 660 } 661 __retres1 = 0; 662 return_label: /* CIL Label */ 663 return (__retres1); 664} 665} 666int is_transmit5_triggered(void) 667{ int __retres1 ; 668 669 { 670 if (t5_pc == 1) { 671 if (E_5 == 1) { 672 __retres1 = 1; 673 goto return_label; 674 } else { 675 676 } 677 } else { 678 679 } 680 __retres1 = 0; 681 return_label: /* CIL Label */ 682 return (__retres1); 683} 684} 685int is_transmit6_triggered(void) 686{ int __retres1 ; 687 688 { 689 if (t6_pc == 1) { 690 if (E_6 == 1) { 691 __retres1 = 1; 692 goto return_label; 693 } else { 694 695 } 696 } else { 697 698 } 699 __retres1 = 0; 700 return_label: /* CIL Label */ 701 return (__retres1); 702} 703} 704int is_transmit7_triggered(void) 705{ int __retres1 ; 706 707 { 708 if (t7_pc == 1) { 709 if (E_7 == 1) { 710 __retres1 = 1; 711 goto return_label; 712 } else { 713 714 } 715 } else { 716 717 } 718 __retres1 = 0; 719 return_label: /* CIL Label */ 720 return (__retres1); 721} 722} 723int is_transmit8_triggered(void) 724{ int __retres1 ; 725 726 { 727 if (t8_pc == 1) { 728 if (E_8 == 1) { 729 __retres1 = 1; 730 goto return_label; 731 } else { 732 733 } 734 } else { 735 736 } 737 __retres1 = 0; 738 return_label: /* CIL Label */ 739 return (__retres1); 740} 741} 742int is_transmit9_triggered(void) 743{ int __retres1 ; 744 745 { 746 if (t9_pc == 1) { 747 if (E_9 == 1) { 748 __retres1 = 1; 749 goto return_label; 750 } else { 751 752 } 753 } else { 754 755 } 756 __retres1 = 0; 757 return_label: /* CIL Label */ 758 return (__retres1); 759} 760} 761int is_transmit10_triggered(void) 762{ int __retres1 ; 763 764 { 765 if (t10_pc == 1) { 766 if (E_10 == 1) { 767 __retres1 = 1; 768 goto return_label; 769 } else { 770 771 } 772 } else { 773 774 } 775 __retres1 = 0; 776 return_label: /* CIL Label */ 777 return (__retres1); 778} 779} 780int is_transmit11_triggered(void) 781{ int __retres1 ; 782 783 { 784 if (t11_pc == 1) { 785 if (E_11 == 1) { 786 __retres1 = 1; 787 goto return_label; 788 } else { 789 790 } 791 } else { 792 793 } 794 __retres1 = 0; 795 return_label: /* CIL Label */ 796 return (__retres1); 797} 798} 799int is_transmit12_triggered(void) 800{ int __retres1 ; 801 802 { 803 if (t12_pc == 1) { 804 if (E_12 == 1) { 805 __retres1 = 1; 806 goto return_label; 807 } else { 808 809 } 810 } else { 811 812 } 813 __retres1 = 0; 814 return_label: /* CIL Label */ 815 return (__retres1); 816} 817} 818void update_channels(void) 819{ 820 821 { 822 823 return; 824} 825} 826void init_threads(void) 827{ 828 829 { 830 if (m_i == 1) { 831 m_st = 0; 832 } else { 833 m_st = 2; 834 } 835 if (t1_i == 1) { 836 t1_st = 0; 837 } else { 838 t1_st = 2; 839 } 840 if (t2_i == 1) { 841 t2_st = 0; 842 } else { 843 t2_st = 2; 844 } 845 if (t3_i == 1) { 846 t3_st = 0; 847 } else { 848 t3_st = 2; 849 } 850 if (t4_i == 1) { 851 t4_st = 0; 852 } else { 853 t4_st = 2; 854 } 855 if (t5_i == 1) { 856 t5_st = 0; 857 } else { 858 t5_st = 2; 859 } 860 if (t6_i == 1) { 861 t6_st = 0; 862 } else { 863 t6_st = 2; 864 } 865 if (t7_i == 1) { 866 t7_st = 0; 867 } else { 868 t7_st = 2; 869 } 870 if (t8_i == 1) { 871 t8_st = 0; 872 } else { 873 t8_st = 2; 874 } 875 if (t9_i == 1) { 876 t9_st = 0; 877 } else { 878 t9_st = 2; 879 } 880 if (t10_i == 1) { 881 t10_st = 0; 882 } else { 883 t10_st = 2; 884 } 885 if (t11_i == 1) { 886 t11_st = 0; 887 } else { 888 t11_st = 2; 889 } 890 if (t12_i == 1) { 891 t12_st = 0; 892 } else { 893 t12_st = 2; 894 } 895 896 return; 897} 898} 899int exists_runnable_thread(void) 900{ int __retres1 ; 901 902 { 903 if (m_st == 0) { 904 __retres1 = 1; 905 goto return_label; 906 } else { 907 if (t1_st == 0) { 908 __retres1 = 1; 909 goto return_label; 910 } else { 911 if (t2_st == 0) { 912 __retres1 = 1; 913 goto return_label; 914 } else { 915 if (t3_st == 0) { 916 __retres1 = 1; 917 goto return_label; 918 } else { 919 if (t4_st == 0) { 920 __retres1 = 1; 921 goto return_label; 922 } else { 923 if (t5_st == 0) { 924 __retres1 = 1; 925 goto return_label; 926 } else { 927 if (t6_st == 0) { 928 __retres1 = 1; 929 goto return_label; 930 } else { 931 if (t7_st == 0) { 932 __retres1 = 1; 933 goto return_label; 934 } else { 935 if (t8_st == 0) { 936 __retres1 = 1; 937 goto return_label; 938 } else { 939 if (t9_st == 0) { 940 __retres1 = 1; 941 goto return_label; 942 } else { 943 if (t10_st == 0) { 944 __retres1 = 1; 945 goto return_label; 946 } else { 947 if (t11_st == 0) { 948 __retres1 = 1; 949 goto return_label; 950 } else { 951 if (t12_st == 0) { 952 __retres1 = 1; 953 goto return_label; 954 } else { 955 956 } 957 } 958 } 959 } 960 } 961 } 962 } 963 } 964 } 965 } 966 } 967 } 968 } 969 __retres1 = 0; 970 return_label: /* CIL Label */ 971 return (__retres1); 972} 973} 974void eval(void) 975{ 976 int tmp ; 977 978 { 979 { 980 while (1) { 981 while_13_continue: /* CIL Label */ ; 982 { 983 tmp = exists_runnable_thread(); 984 } 985 if (tmp) { 986 987 } else { 988 goto while_13_break; 989 } 990 if (m_st == 0) { 991 int tmp_ndt_1; 992 tmp_ndt_1 = __VERIFIER_nondet_int(); 993 if (tmp_ndt_1) { 994 { 995 m_st = 1; 996 master(); 997 } 998 } else { 999 1000 } 1001 } else { 1002 1003 } 1004 if (t1_st == 0) { 1005 int tmp_ndt_2; 1006 tmp_ndt_2 = __VERIFIER_nondet_int(); 1007 if (tmp_ndt_2) { 1008 { 1009 t1_st = 1; 1010 transmit1(); 1011 } 1012 } else { 1013 1014 } 1015 } else { 1016 1017 } 1018 if (t2_st == 0) { 1019 int tmp_ndt_3; 1020 tmp_ndt_3 = __VERIFIER_nondet_int(); 1021 if (tmp_ndt_3) { 1022 { 1023 t2_st = 1; 1024 transmit2(); 1025 } 1026 } else { 1027 1028 } 1029 } else { 1030 1031 } 1032 if (t3_st == 0) { 1033 int tmp_ndt_4; 1034 tmp_ndt_4 = __VERIFIER_nondet_int(); 1035 if (tmp_ndt_4) { 1036 { 1037 t3_st = 1; 1038 transmit3(); 1039 } 1040 } else { 1041 1042 } 1043 } else { 1044 1045 } 1046 if (t4_st == 0) { 1047 int tmp_ndt_5; 1048 tmp_ndt_5 = __VERIFIER_nondet_int(); 1049 if (tmp_ndt_5) { 1050 { 1051 t4_st = 1; 1052 transmit4(); 1053 } 1054 } else { 1055 1056 } 1057 } else { 1058 1059 } 1060 if (t5_st == 0) { 1061 int tmp_ndt_6; 1062 tmp_ndt_6 = __VERIFIER_nondet_int(); 1063 if (tmp_ndt_6) { 1064 { 1065 t5_st = 1; 1066 transmit5(); 1067 } 1068 } else { 1069 1070 } 1071 } else { 1072 1073 } 1074 if (t6_st == 0) { 1075 int tmp_ndt_7; 1076 tmp_ndt_7 = __VERIFIER_nondet_int(); 1077 if (tmp_ndt_7) { 1078 { 1079 t6_st = 1; 1080 transmit6(); 1081 } 1082 } else { 1083 1084 } 1085 } else { 1086 1087 } 1088 if (t7_st == 0) { 1089 int tmp_ndt_8; 1090 tmp_ndt_8 = __VERIFIER_nondet_int(); 1091 if (tmp_ndt_8) { 1092 { 1093 t7_st = 1; 1094 transmit7(); 1095 } 1096 } else { 1097 1098 } 1099 } else { 1100 1101 } 1102 if (t8_st == 0) { 1103 int tmp_ndt_9; 1104 tmp_ndt_9 = __VERIFIER_nondet_int(); 1105 if (tmp_ndt_9) { 1106 { 1107 t8_st = 1; 1108 transmit8(); 1109 } 1110 } else { 1111 1112 } 1113 } else { 1114 1115 } 1116 if (t9_st == 0) { 1117 int tmp_ndt_10; 1118 tmp_ndt_10 = __VERIFIER_nondet_int(); 1119 if (tmp_ndt_10) { 1120 { 1121 t9_st = 1; 1122 transmit9(); 1123 } 1124 } else { 1125 1126 } 1127 } else { 1128 1129 } 1130 if (t10_st == 0) { 1131 int tmp_ndt_11; 1132 tmp_ndt_11 = __VERIFIER_nondet_int(); 1133 if (tmp_ndt_11) { 1134 { 1135 t10_st = 1; 1136 transmit10(); 1137 } 1138 } else { 1139 1140 } 1141 } else { 1142 1143 } 1144 if (t11_st == 0) { 1145 int tmp_ndt_12; 1146 tmp_ndt_12 = __VERIFIER_nondet_int(); 1147 if (tmp_ndt_12) { 1148 { 1149 t11_st = 1; 1150 transmit11(); 1151 } 1152 } else { 1153 1154 } 1155 } else { 1156 1157 } 1158 if (t12_st == 0) { 1159 int tmp_ndt_13; 1160 tmp_ndt_13 = __VERIFIER_nondet_int(); 1161 if (tmp_ndt_13) { 1162 { 1163 t12_st = 1; 1164 transmit12(); 1165 } 1166 } else { 1167 1168 } 1169 } else { 1170 1171 } 1172 } 1173 while_13_break: /* CIL Label */ ; 1174 } 1175 1176 return; 1177} 1178} 1179void fire_delta_events(void) 1180{ 1181 1182 { 1183 if (M_E == 0) { 1184 M_E = 1; 1185 } else { 1186 1187 } 1188 if (T1_E == 0) { 1189 T1_E = 1; 1190 } else { 1191 1192 } 1193 if (T2_E == 0) { 1194 T2_E = 1; 1195 } else { 1196 1197 } 1198 if (T3_E == 0) { 1199 T3_E = 1; 1200 } else { 1201 1202 } 1203 if (T4_E == 0) { 1204 T4_E = 1; 1205 } else { 1206 1207 } 1208 if (T5_E == 0) { 1209 T5_E = 1; 1210 } else { 1211 1212 } 1213 if (T6_E == 0) { 1214 T6_E = 1; 1215 } else { 1216 1217 } 1218 if (T7_E == 0) { 1219 T7_E = 1; 1220 } else { 1221 1222 } 1223 if (T8_E == 0) { 1224 T8_E = 1; 1225 } else { 1226 1227 } 1228 if (T9_E == 0) { 1229 T9_E = 1; 1230 } else { 1231 1232 } 1233 if (T10_E == 0) { 1234 T10_E = 1; 1235 } else { 1236 1237 } 1238 if (T11_E == 0) { 1239 T11_E = 1; 1240 } else { 1241 1242 } 1243 if (T12_E == 0) { 1244 T12_E = 1; 1245 } else { 1246 1247 } 1248 if (E_M == 0) { 1249 E_M = 1; 1250 } else { 1251 1252 } 1253 if (E_1 == 0) { 1254 E_1 = 1; 1255 } else { 1256 1257 } 1258 if (E_2 == 0) { 1259 E_2 = 1; 1260 } else { 1261 1262 } 1263 if (E_3 == 0) { 1264 E_3 = 1; 1265 } else { 1266 1267 } 1268 if (E_4 == 0) { 1269 E_4 = 1; 1270 } else { 1271 1272 } 1273 if (E_5 == 0) { 1274 E_5 = 1; 1275 } else { 1276 1277 } 1278 if (E_6 == 0) { 1279 E_6 = 1; 1280 } else { 1281 1282 } 1283 if (E_7 == 0) { 1284 E_7 = 1; 1285 } else { 1286 1287 } 1288 if (E_8 == 0) { 1289 E_8 = 1; 1290 } else { 1291 1292 } 1293 if (E_9 == 0) { 1294 E_9 = 1; 1295 } else { 1296 1297 } 1298 if (E_10 == 0) { 1299 E_10 = 1; 1300 } else { 1301 1302 } 1303 if (E_11 == 0) { 1304 E_11 = 1; 1305 } else { 1306 1307 } 1308 if (E_12 == 0) { 1309 E_12 = 1; 1310 } else { 1311 1312 } 1313 1314 return; 1315} 1316} 1317void reset_delta_events(void) 1318{ 1319 1320 { 1321 if (M_E == 1) { 1322 M_E = 2; 1323 } else { 1324 1325 } 1326 if (T1_E == 1) { 1327 T1_E = 2; 1328 } else { 1329 1330 } 1331 if (T2_E == 1) { 1332 T2_E = 2; 1333 } else { 1334 1335 } 1336 if (T3_E == 1) { 1337 T3_E = 2; 1338 } else { 1339 1340 } 1341 if (T4_E == 1) { 1342 T4_E = 2; 1343 } else { 1344 1345 } 1346 if (T5_E == 1) { 1347 T5_E = 2; 1348 } else { 1349 1350 } 1351 if (T6_E == 1) { 1352 T6_E = 2; 1353 } else { 1354 1355 } 1356 if (T7_E == 1) { 1357 T7_E = 2; 1358 } else { 1359 1360 } 1361 if (T8_E == 1) { 1362 T8_E = 2; 1363 } else { 1364 1365 } 1366 if (T9_E == 1) { 1367 T9_E = 2; 1368 } else { 1369 1370 } 1371 if (T10_E == 1) { 1372 T10_E = 2; 1373 } else { 1374 1375 } 1376 if (T11_E == 1) { 1377 T11_E = 2; 1378 } else { 1379 1380 } 1381 if (T12_E == 1) { 1382 T12_E = 2; 1383 } else { 1384 1385 } 1386 if (E_M == 1) { 1387 E_M = 2; 1388 } else { 1389 1390 } 1391 if (E_1 == 1) { 1392 E_1 = 2; 1393 } else { 1394 1395 } 1396 if (E_2 == 1) { 1397 E_2 = 2; 1398 } else { 1399 1400 } 1401 if (E_3 == 1) { 1402 E_3 = 2; 1403 } else { 1404 1405 } 1406 if (E_4 == 1) { 1407 E_4 = 2; 1408 } else { 1409 1410 } 1411 if (E_5 == 1) { 1412 E_5 = 2; 1413 } else { 1414 1415 } 1416 if (E_6 == 1) { 1417 E_6 = 2; 1418 } else { 1419 1420 } 1421 if (E_7 == 1) { 1422 E_7 = 2; 1423 } else { 1424 1425 } 1426 if (E_8 == 1) { 1427 E_8 = 2; 1428 } else { 1429 1430 } 1431 if (E_9 == 1) { 1432 E_9 = 2; 1433 } else { 1434 1435 } 1436 if (E_10 == 1) { 1437 E_10 = 2; 1438 } else { 1439 1440 } 1441 if (E_11 == 1) { 1442 E_11 = 2; 1443 } else { 1444 1445 } 1446 if (E_12 == 1) { 1447 E_12 = 2; 1448 } else { 1449 1450 } 1451 1452 return; 1453} 1454} 1455void activate_threads(void) 1456{ int tmp ; 1457 int tmp___0 ; 1458 int tmp___1 ; 1459 int tmp___2 ; 1460 int tmp___3 ; 1461 int tmp___4 ; 1462 int tmp___5 ; 1463 int tmp___6 ; 1464 int tmp___7 ; 1465 int tmp___8 ; 1466 int tmp___9 ; 1467 int tmp___10 ; 1468 int tmp___11 ; 1469 1470 { 1471 { 1472 tmp = is_master_triggered(); 1473 } 1474 if (tmp) { 1475 m_st = 0; 1476 } else { 1477 1478 } 1479 { 1480 tmp___0 = is_transmit1_triggered(); 1481 } 1482 if (tmp___0) { 1483 t1_st = 0; 1484 } else { 1485 1486 } 1487 { 1488 tmp___1 = is_transmit2_triggered(); 1489 } 1490 if (tmp___1) { 1491 t2_st = 0; 1492 } else { 1493 1494 } 1495 { 1496 tmp___2 = is_transmit3_triggered(); 1497 } 1498 if (tmp___2) { 1499 t3_st = 0; 1500 } else { 1501 1502 } 1503 { 1504 tmp___3 = is_transmit4_triggered(); 1505 } 1506 if (tmp___3) { 1507 t4_st = 0; 1508 } else { 1509 1510 } 1511 { 1512 tmp___4 = is_transmit5_triggered(); 1513 } 1514 if (tmp___4) { 1515 t5_st = 0; 1516 } else { 1517 1518 } 1519 { 1520 tmp___5 = is_transmit6_triggered(); 1521 } 1522 if (tmp___5) { 1523 t6_st = 0; 1524 } else { 1525 1526 } 1527 { 1528 tmp___6 = is_transmit7_triggered(); 1529 } 1530 if (tmp___6) { 1531 t7_st = 0; 1532 } else { 1533 1534 } 1535 { 1536 tmp___7 = is_transmit8_triggered(); 1537 } 1538 if (tmp___7) { 1539 t8_st = 0; 1540 } else { 1541 1542 } 1543 { 1544 tmp___8 = is_transmit9_triggered(); 1545 } 1546 if (tmp___8) { 1547 t9_st = 0; 1548 } else { 1549 1550 } 1551 { 1552 tmp___9 = is_transmit10_triggered(); 1553 } 1554 if (tmp___9) { 1555 t10_st = 0; 1556 } else { 1557 1558 } 1559 { 1560 tmp___10 = is_transmit11_triggered(); 1561 } 1562 if (tmp___10) { 1563 t11_st = 0; 1564 } else { 1565 1566 } 1567 { 1568 tmp___11 = is_transmit12_triggered(); 1569 } 1570 if (tmp___11) { 1571 t12_st = 0; 1572 } else { 1573 1574 } 1575 1576 return; 1577} 1578} 1579void immediate_notify(void) 1580{ 1581 1582 { 1583 { 1584 activate_threads(); 1585 } 1586 1587 return; 1588} 1589} 1590void fire_time_events(void) 1591{ 1592 1593 { 1594 M_E = 1; 1595 1596 return; 1597} 1598} 1599void reset_time_events(void) 1600{ 1601 1602 { 1603 if (M_E == 1) { 1604 M_E = 2; 1605 } else { 1606 1607 } 1608 if (T1_E == 1) { 1609 T1_E = 2; 1610 } else { 1611 1612 } 1613 if (T2_E == 1) { 1614 T2_E = 2; 1615 } else { 1616 1617 } 1618 if (T3_E == 1) { 1619 T3_E = 2; 1620 } else { 1621 1622 } 1623 if (T4_E == 1) { 1624 T4_E = 2; 1625 } else { 1626 1627 } 1628 if (T5_E == 1) { 1629 T5_E = 2; 1630 } else { 1631 1632 } 1633 if (T6_E == 1) { 1634 T6_E = 2; 1635 } else { 1636 1637 } 1638 if (T7_E == 1) { 1639 T7_E = 2; 1640 } else { 1641 1642 } 1643 if (T8_E == 1) { 1644 T8_E = 2; 1645 } else { 1646 1647 } 1648 if (T9_E == 1) { 1649 T9_E = 2; 1650 } else { 1651 1652 } 1653 if (T10_E == 1) { 1654 T10_E = 2; 1655 } else { 1656 1657 } 1658 if (T11_E == 1) { 1659 T11_E = 2; 1660 } else { 1661 1662 } 1663 if (T12_E == 1) { 1664 T12_E = 2; 1665 } else { 1666 1667 } 1668 if (E_M == 1) { 1669 E_M = 2; 1670 } else { 1671 1672 } 1673 if (E_1 == 1) { 1674 E_1 = 2; 1675 } else { 1676 1677 } 1678 if (E_2 == 1) { 1679 E_2 = 2; 1680 } else { 1681 1682 } 1683 if (E_3 == 1) { 1684 E_3 = 2; 1685 } else { 1686 1687 } 1688 if (E_4 == 1) { 1689 E_4 = 2; 1690 } else { 1691 1692 } 1693 if (E_5 == 1) { 1694 E_5 = 2; 1695 } else { 1696 1697 } 1698 if (E_6 == 1) { 1699 E_6 = 2; 1700 } else { 1701 1702 } 1703 if (E_7 == 1) { 1704 E_7 = 2; 1705 } else { 1706 1707 } 1708 if (E_8 == 1) { 1709 E_8 = 2; 1710 } else { 1711 1712 } 1713 if (E_9 == 1) { 1714 E_9 = 2; 1715 } else { 1716 1717 } 1718 if (E_10 == 1) { 1719 E_10 = 2; 1720 } else { 1721 1722 } 1723 if (E_11 == 1) { 1724 E_11 = 2; 1725 } else { 1726 1727 } 1728 if (E_12 == 1) { 1729 E_12 = 2; 1730 } else { 1731 1732 } 1733 1734 return; 1735} 1736} 1737void init_model(void) 1738{ 1739 1740 { 1741 m_i = 1; 1742 t1_i = 1; 1743 t2_i = 1; 1744 t3_i = 1; 1745 t4_i = 1; 1746 t5_i = 1; 1747 t6_i = 1; 1748 t7_i = 1; 1749 t8_i = 1; 1750 t9_i = 1; 1751 t10_i = 1; 1752 t11_i = 1; 1753 t12_i = 1; 1754 1755 return; 1756} 1757} 1758int stop_simulation(void) 1759{ int tmp ; 1760 int __retres2 ; 1761 1762 { 1763 { 1764 tmp = exists_runnable_thread(); 1765 } 1766 if (tmp) { 1767 __retres2 = 0; 1768 goto return_label; 1769 } else { 1770 1771 } 1772 __retres2 = 1; 1773 return_label: /* CIL Label */ 1774 return (__retres2); 1775} 1776} 1777void start_simulation(void) 1778{ int kernel_st ; 1779 int tmp ; 1780 int tmp___0 ; 1781 1782 { 1783 { 1784 kernel_st = 0; 1785 update_channels(); 1786 init_threads(); 1787 fire_delta_events(); 1788 activate_threads(); 1789 reset_delta_events(); 1790 } 1791 { 1792 while (1) { 1793 while_14_continue: /* CIL Label */ ; 1794 { 1795 kernel_st = 1; 1796 eval(); 1797 } 1798 { 1799 kernel_st = 2; 1800 update_channels(); 1801 } 1802 { 1803 kernel_st = 3; 1804 fire_delta_events(); 1805 activate_threads(); 1806 reset_delta_events(); 1807 } 1808 { 1809 tmp = exists_runnable_thread(); 1810 } 1811 if (tmp == 0) { 1812 { 1813 kernel_st = 4; 1814 fire_time_events(); 1815 activate_threads(); 1816 reset_time_events(); 1817 } 1818 } else { 1819 1820 } 1821 { 1822 tmp___0 = stop_simulation(); 1823 } 1824 if (tmp___0) { 1825 goto while_14_break; 1826 } else { 1827 1828 } 1829 } 1830 while_14_break: /* CIL Label */ ; 1831 } 1832 1833 return; 1834} 1835} 1836int main(void) 1837{ int __retres1 ; 1838 1839 { 1840 { 1841 init_model(); 1842 start_simulation(); 1843 } 1844 __retres1 = 0; 1845 return (__retres1); 1846} 1847}