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