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