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.06.BUG.cil.c |
Line in file: | 8 |
Project: | SV-COMP 2012 |
Tools: |
Manual Work
|
Entered: | 2012-11-19 13:47:39 UTC |
1/* Generated by CIL v. 1.3.6 */ 2/* print_CIL_Input is true */ 3 4void error(void) 5{ 6 7 { 8 ERROR: ; 9 goto ERROR; 10 return; 11} 12} 13int m_pc = 0; 14int t1_pc = 0; 15int t2_pc = 0; 16int t3_pc = 0; 17int t4_pc = 0; 18int t5_pc = 0; 19int t6_pc = 0; 20int m_st ; 21int t1_st ; 22int t2_st ; 23int t3_st ; 24int t4_st ; 25int t5_st ; 26int t6_st ; 27int m_i ; 28int t1_i ; 29int t2_i ; 30int t3_i ; 31int t4_i ; 32int t5_i ; 33int t6_i ; 34int M_E = 2; 35int T1_E = 2; 36int T2_E = 2; 37int T3_E = 2; 38int T4_E = 2; 39int T5_E = 2; 40int T6_E = 2; 41int E_M = 2; 42int E_1 = 2; 43int E_2 = 2; 44int E_3 = 2; 45int E_4 = 2; 46int E_5 = 2; 47int E_6 = 2; 48int is_master_triggered(void) ; 49int is_transmit1_triggered(void) ; 50int is_transmit2_triggered(void) ; 51int is_transmit3_triggered(void) ; 52int is_transmit4_triggered(void) ; 53int is_transmit5_triggered(void) ; 54int is_transmit6_triggered(void) ; 55void immediate_notify(void) ; 56int token ; 57int __VERIFIER_nondet_int() ; 58int local ; 59void master(void) 60{ 61int tmp_var ; 62 { 63 if (m_pc == 0) { 64 goto M_ENTRY; 65 } else { 66 if (m_pc == 1) { 67 goto M_WAIT; 68 } else { 69 70 } 71 } 72 M_ENTRY: ; 73 { 74 while (1) { 75 while_0_continue: /* CIL Label */ ; 76 { 77 token = __VERIFIER_nondet_int(); 78 local = token; 79 E_1 = 1; 80 immediate_notify(); 81 E_1 = 2; 82 m_pc = 1; 83 m_st = 2; 84 } 85 86 goto return_label; 87 M_WAIT: ; 88 if (token != local + 6) { 89 { 90 error(); 91 } 92 } else { 93 if(tmp_var <= 5){ 94 if(tmp_var >= 5){ 95 96 } 97 } 98 99 if(tmp_var <= 5){ 100 if(tmp_var >= 5){ 101 if(tmp_var == 5){ 102 error(); 103 } 104 } 105 } 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_1_continue: /* CIL Label */ ; 132 t1_pc = 1; 133 t1_st = 2; 134 135 goto return_label; 136 T1_WAIT: 137 { 138 token += 1; 139 E_2 = 1; 140 immediate_notify(); 141 E_2 = 2; 142 } 143 } 144 while_1_break: /* CIL Label */ ; 145 } 146 147 return_label: /* CIL Label */ 148 return; 149} 150} 151void transmit2(void) 152{ 153 154 { 155 if (t2_pc == 0) { 156 goto T2_ENTRY; 157 } else { 158 if (t2_pc == 1) { 159 goto T2_WAIT; 160 } else { 161 162 } 163 } 164 T2_ENTRY: ; 165 { 166 while (1) { 167 while_2_continue: /* CIL Label */ ; 168 t2_pc = 1; 169 t2_st = 2; 170 171 goto return_label; 172 T2_WAIT: 173 { 174 token += 1; 175 E_3 = 1; 176 immediate_notify(); 177 E_3 = 2; 178 } 179 } 180 while_2_break: /* CIL Label */ ; 181 } 182 183 return_label: /* CIL Label */ 184 return; 185} 186} 187void transmit3(void) 188{ 189 190 { 191 if (t3_pc == 0) { 192 goto T3_ENTRY; 193 } else { 194 if (t3_pc == 1) { 195 goto T3_WAIT; 196 } else { 197 198 } 199 } 200 T3_ENTRY: ; 201 { 202 while (1) { 203 while_3_continue: /* CIL Label */ ; 204 t3_pc = 1; 205 t3_st = 2; 206 207 goto return_label; 208 T3_WAIT: 209 { 210 token += 1; 211 E_4 = 1; 212 immediate_notify(); 213 E_4 = 2; 214 } 215 } 216 while_3_break: /* CIL Label */ ; 217 } 218 219 return_label: /* CIL Label */ 220 return; 221} 222} 223void transmit4(void) 224{ 225 226 { 227 if (t4_pc == 0) { 228 goto T4_ENTRY; 229 } else { 230 if (t4_pc == 1) { 231 goto T4_WAIT; 232 } else { 233 234 } 235 } 236 T4_ENTRY: ; 237 { 238 while (1) { 239 while_4_continue: /* CIL Label */ ; 240 t4_pc = 1; 241 t4_st = 2; 242 243 goto return_label; 244 T4_WAIT: 245 { 246 token += 1; 247 E_5 = 1; 248 immediate_notify(); 249 E_5 = 2; 250 } 251 } 252 while_4_break: /* CIL Label */ ; 253 } 254 255 return_label: /* CIL Label */ 256 return; 257} 258} 259void transmit5(void) 260{ 261 262 { 263 if (t5_pc == 0) { 264 goto T5_ENTRY; 265 } else { 266 if (t5_pc == 1) { 267 goto T5_WAIT; 268 } else { 269 270 } 271 } 272 T5_ENTRY: ; 273 { 274 while (1) { 275 while_5_continue: /* CIL Label */ ; 276 t5_pc = 1; 277 t5_st = 2; 278 279 goto return_label; 280 T5_WAIT: 281 { 282 token += 1; 283 E_6 = 1; 284 immediate_notify(); 285 E_6 = 2; 286 } 287 } 288 while_5_break: /* CIL Label */ ; 289 } 290 291 return_label: /* CIL Label */ 292 return; 293} 294} 295void transmit6(void) 296{ 297 298 { 299 if (t6_pc == 0) { 300 goto T6_ENTRY; 301 } else { 302 if (t6_pc == 1) { 303 goto T6_WAIT; 304 } else { 305 306 } 307 } 308 T6_ENTRY: ; 309 { 310 while (1) { 311 while_6_continue: /* CIL Label */ ; 312 t6_pc = 1; 313 t6_st = 2; 314 315 goto return_label; 316 T6_WAIT: 317 { 318 token += 1; 319 E_M = 1; 320 immediate_notify(); 321 E_M = 2; 322 } 323 } 324 while_6_break: /* CIL Label */ ; 325 } 326 327 return_label: /* CIL Label */ 328 return; 329} 330} 331int is_master_triggered(void) 332{ int __retres1 ; 333 334 { 335 if (m_pc == 1) { 336 if (E_M == 1) { 337 __retres1 = 1; 338 goto return_label; 339 } else { 340 341 } 342 } else { 343 344 } 345 __retres1 = 0; 346 return_label: /* CIL Label */ 347 return (__retres1); 348} 349} 350int is_transmit1_triggered(void) 351{ int __retres1 ; 352 353 { 354 if (t1_pc == 1) { 355 if (E_1 == 1) { 356 __retres1 = 1; 357 goto return_label; 358 } else { 359 360 } 361 } else { 362 363 } 364 __retres1 = 0; 365 return_label: /* CIL Label */ 366 return (__retres1); 367} 368} 369int is_transmit2_triggered(void) 370{ int __retres1 ; 371 372 { 373 if (t2_pc == 1) { 374 if (E_2 == 1) { 375 __retres1 = 1; 376 goto return_label; 377 } else { 378 379 } 380 } else { 381 382 } 383 __retres1 = 0; 384 return_label: /* CIL Label */ 385 return (__retres1); 386} 387} 388int is_transmit3_triggered(void) 389{ int __retres1 ; 390 391 { 392 if (t3_pc == 1) { 393 if (E_3 == 1) { 394 __retres1 = 1; 395 goto return_label; 396 } else { 397 398 } 399 } else { 400 401 } 402 __retres1 = 0; 403 return_label: /* CIL Label */ 404 return (__retres1); 405} 406} 407int is_transmit4_triggered(void) 408{ int __retres1 ; 409 410 { 411 if (t4_pc == 1) { 412 if (E_4 == 1) { 413 __retres1 = 1; 414 goto return_label; 415 } else { 416 417 } 418 } else { 419 420 } 421 __retres1 = 0; 422 return_label: /* CIL Label */ 423 return (__retres1); 424} 425} 426int is_transmit5_triggered(void) 427{ int __retres1 ; 428 429 { 430 if (t5_pc == 1) { 431 if (E_5 == 1) { 432 __retres1 = 1; 433 goto return_label; 434 } else { 435 436 } 437 } else { 438 439 } 440 __retres1 = 0; 441 return_label: /* CIL Label */ 442 return (__retres1); 443} 444} 445int is_transmit6_triggered(void) 446{ int __retres1 ; 447 448 { 449 if (t6_pc == 1) { 450 if (E_6 == 1) { 451 __retres1 = 1; 452 goto return_label; 453 } else { 454 455 } 456 } else { 457 458 } 459 __retres1 = 0; 460 return_label: /* CIL Label */ 461 return (__retres1); 462} 463} 464void update_channels(void) 465{ 466 467 { 468 469 return; 470} 471} 472void init_threads(void) 473{ 474 475 { 476 if (m_i == 1) { 477 m_st = 0; 478 } else { 479 m_st = 2; 480 } 481 if (t1_i == 1) { 482 t1_st = 0; 483 } else { 484 t1_st = 2; 485 } 486 if (t2_i == 1) { 487 t2_st = 0; 488 } else { 489 t2_st = 2; 490 } 491 if (t3_i == 1) { 492 t3_st = 0; 493 } else { 494 t3_st = 2; 495 } 496 if (t4_i == 1) { 497 t4_st = 0; 498 } else { 499 t4_st = 2; 500 } 501 if (t5_i == 1) { 502 t5_st = 0; 503 } else { 504 t5_st = 2; 505 } 506 if (t6_i == 1) { 507 t6_st = 0; 508 } else { 509 t6_st = 2; 510 } 511 512 return; 513} 514} 515int exists_runnable_thread(void) 516{ int __retres1 ; 517 518 { 519 if (m_st == 0) { 520 __retres1 = 1; 521 goto return_label; 522 } else { 523 if (t1_st == 0) { 524 __retres1 = 1; 525 goto return_label; 526 } else { 527 if (t2_st == 0) { 528 __retres1 = 1; 529 goto return_label; 530 } else { 531 if (t3_st == 0) { 532 __retres1 = 1; 533 goto return_label; 534 } else { 535 if (t4_st == 0) { 536 __retres1 = 1; 537 goto return_label; 538 } else { 539 if (t5_st == 0) { 540 __retres1 = 1; 541 goto return_label; 542 } else { 543 if (t6_st == 0) { 544 __retres1 = 1; 545 goto return_label; 546 } else { 547 548 } 549 } 550 } 551 } 552 } 553 } 554 } 555 __retres1 = 0; 556 return_label: /* CIL Label */ 557 return (__retres1); 558} 559} 560void eval(void) 561{// int __VERIFIER_nondet_int() ; 562 int tmp ; 563 564 { 565 { 566 while (1) { 567 while_7_continue: /* CIL Label */ ; 568 { 569 tmp = exists_runnable_thread(); 570 } 571 if (tmp) { 572 573 } else { 574 goto while_7_break; 575 } 576 if (m_st == 0) { 577 int tmp_ndt_1; 578 tmp_ndt_1 = __VERIFIER_nondet_int(); 579 if (tmp_ndt_1) { 580 { 581 m_st = 1; 582 master(); 583 } 584 } else { 585 586 } 587 } else { 588 589 } 590 if (t1_st == 0) { 591 int tmp_ndt_2; 592 tmp_ndt_2 = __VERIFIER_nondet_int(); 593 if (tmp_ndt_2) { 594 { 595 t1_st = 1; 596 transmit1(); 597 } 598 } else { 599 600 } 601 } else { 602 603 } 604 if (t2_st == 0) { 605 int tmp_ndt_3; 606 tmp_ndt_3 = __VERIFIER_nondet_int(); 607 if (tmp_ndt_3) { 608 { 609 t2_st = 1; 610 transmit2(); 611 } 612 } else { 613 614 } 615 } else { 616 617 } 618 if (t3_st == 0) { 619 int tmp_ndt_4; 620 tmp_ndt_4 = __VERIFIER_nondet_int(); 621 if (tmp_ndt_4) { 622 { 623 t3_st = 1; 624 transmit3(); 625 } 626 } else { 627 628 } 629 } else { 630 631 } 632 if (t4_st == 0) { 633 int tmp_ndt_5; 634 tmp_ndt_5 = __VERIFIER_nondet_int(); 635 if (tmp_ndt_5) { 636 { 637 t4_st = 1; 638 transmit4(); 639 } 640 } else { 641 642 } 643 } else { 644 645 } 646 if (t5_st == 0) { 647 int tmp_ndt_6; 648 tmp_ndt_6 = __VERIFIER_nondet_int(); 649 if (tmp_ndt_6) { 650 { 651 t5_st = 1; 652 transmit5(); 653 } 654 } else { 655 656 } 657 } else { 658 659 } 660 if (t6_st == 0) { 661 int tmp_ndt_7; 662 tmp_ndt_7 = __VERIFIER_nondet_int(); 663 if (tmp_ndt_7) { 664 { 665 t6_st = 1; 666 transmit6(); 667 } 668 } else { 669 670 } 671 } else { 672 673 } 674 } 675 while_7_break: /* CIL Label */ ; 676 } 677 678 return; 679} 680} 681void fire_delta_events(void) 682{ 683 684 { 685 if (M_E == 0) { 686 M_E = 1; 687 } else { 688 689 } 690 if (T1_E == 0) { 691 T1_E = 1; 692 } else { 693 694 } 695 if (T2_E == 0) { 696 T2_E = 1; 697 } else { 698 699 } 700 if (T3_E == 0) { 701 T3_E = 1; 702 } else { 703 704 } 705 if (T4_E == 0) { 706 T4_E = 1; 707 } else { 708 709 } 710 if (T5_E == 0) { 711 T5_E = 1; 712 } else { 713 714 } 715 if (T6_E == 0) { 716 T6_E = 1; 717 } else { 718 719 } 720 if (E_M == 0) { 721 E_M = 1; 722 } else { 723 724 } 725 if (E_1 == 0) { 726 E_1 = 1; 727 } else { 728 729 } 730 if (E_2 == 0) { 731 E_2 = 1; 732 } else { 733 734 } 735 if (E_3 == 0) { 736 E_3 = 1; 737 } else { 738 739 } 740 if (E_4 == 0) { 741 E_4 = 1; 742 } else { 743 744 } 745 if (E_5 == 0) { 746 E_5 = 1; 747 } else { 748 749 } 750 if (E_6 == 0) { 751 E_6 = 1; 752 } else { 753 754 } 755 756 return; 757} 758} 759void reset_delta_events(void) 760{ 761 762 { 763 if (M_E == 1) { 764 M_E = 2; 765 } else { 766 767 } 768 if (T1_E == 1) { 769 T1_E = 2; 770 } else { 771 772 } 773 if (T2_E == 1) { 774 T2_E = 2; 775 } else { 776 777 } 778 if (T3_E == 1) { 779 T3_E = 2; 780 } else { 781 782 } 783 if (T4_E == 1) { 784 T4_E = 2; 785 } else { 786 787 } 788 if (T5_E == 1) { 789 T5_E = 2; 790 } else { 791 792 } 793 if (T6_E == 1) { 794 T6_E = 2; 795 } else { 796 797 } 798 if (E_M == 1) { 799 E_M = 2; 800 } else { 801 802 } 803 if (E_1 == 1) { 804 E_1 = 2; 805 } else { 806 807 } 808 if (E_2 == 1) { 809 E_2 = 2; 810 } else { 811 812 } 813 if (E_3 == 1) { 814 E_3 = 2; 815 } else { 816 817 } 818 if (E_4 == 1) { 819 E_4 = 2; 820 } else { 821 822 } 823 if (E_5 == 1) { 824 E_5 = 2; 825 } else { 826 827 } 828 if (E_6 == 1) { 829 E_6 = 2; 830 } else { 831 832 } 833 834 return; 835} 836} 837void activate_threads(void) 838{ int tmp ; 839 int tmp___0 ; 840 int tmp___1 ; 841 int tmp___2 ; 842 int tmp___3 ; 843 int tmp___4 ; 844 int tmp___5 ; 845 846 { 847 { 848 tmp = is_master_triggered(); 849 } 850 if (tmp) { 851 m_st = 0; 852 } else { 853 854 } 855 { 856 tmp___0 = is_transmit1_triggered(); 857 } 858 if (tmp___0) { 859 t1_st = 0; 860 } else { 861 862 } 863 { 864 tmp___1 = is_transmit2_triggered(); 865 } 866 if (tmp___1) { 867 t2_st = 0; 868 } else { 869 870 } 871 { 872 tmp___2 = is_transmit3_triggered(); 873 } 874 if (tmp___2) { 875 t3_st = 0; 876 } else { 877 878 } 879 { 880 tmp___3 = is_transmit4_triggered(); 881 } 882 if (tmp___3) { 883 t4_st = 0; 884 } else { 885 886 } 887 { 888 tmp___4 = is_transmit5_triggered(); 889 } 890 if (tmp___4) { 891 t5_st = 0; 892 } else { 893 894 } 895 { 896 tmp___5 = is_transmit6_triggered(); 897 } 898 if (tmp___5) { 899 t6_st = 0; 900 } else { 901 902 } 903 904 return; 905} 906} 907void immediate_notify(void) 908{ 909 910 { 911 { 912 activate_threads(); 913 } 914 915 return; 916} 917} 918void fire_time_events(void) 919{ 920 921 { 922 M_E = 1; 923 924 return; 925} 926} 927void reset_time_events(void) 928{ 929 930 { 931 if (M_E == 1) { 932 M_E = 2; 933 } else { 934 935 } 936 if (T1_E == 1) { 937 T1_E = 2; 938 } else { 939 940 } 941 if (T2_E == 1) { 942 T2_E = 2; 943 } else { 944 945 } 946 if (T3_E == 1) { 947 T3_E = 2; 948 } else { 949 950 } 951 if (T4_E == 1) { 952 T4_E = 2; 953 } else { 954 955 } 956 if (T5_E == 1) { 957 T5_E = 2; 958 } else { 959 960 } 961 if (T6_E == 1) { 962 T6_E = 2; 963 } else { 964 965 } 966 if (E_M == 1) { 967 E_M = 2; 968 } else { 969 970 } 971 if (E_1 == 1) { 972 E_1 = 2; 973 } else { 974 975 } 976 if (E_2 == 1) { 977 E_2 = 2; 978 } else { 979 980 } 981 if (E_3 == 1) { 982 E_3 = 2; 983 } else { 984 985 } 986 if (E_4 == 1) { 987 E_4 = 2; 988 } else { 989 990 } 991 if (E_5 == 1) { 992 E_5 = 2; 993 } else { 994 995 } 996 if (E_6 == 1) { 997 E_6 = 2; 998 } else { 999 1000 } 1001 1002 return; 1003} 1004} 1005void init_model(void) 1006{ 1007 1008 { 1009 m_i = 1; 1010 t1_i = 1; 1011 t2_i = 1; 1012 t3_i = 1; 1013 t4_i = 1; 1014 t5_i = 1; 1015 t6_i = 1; 1016 1017 return; 1018} 1019} 1020int stop_simulation(void) 1021{ int tmp ; 1022 int __retres2 ; 1023 1024 { 1025 { 1026 tmp = exists_runnable_thread(); 1027 } 1028 if (tmp) { 1029 __retres2 = 0; 1030 goto return_label; 1031 } else { 1032 1033 } 1034 __retres2 = 1; 1035 return_label: /* CIL Label */ 1036 return (__retres2); 1037} 1038} 1039void start_simulation(void) 1040{ int kernel_st ; 1041 int tmp ; 1042 int tmp___0 ; 1043 1044 { 1045 { 1046 kernel_st = 0; 1047 update_channels(); 1048 init_threads(); 1049 fire_delta_events(); 1050 activate_threads(); 1051 reset_delta_events(); 1052 } 1053 { 1054 while (1) { 1055 while_8_continue: /* CIL Label */ ; 1056 { 1057 kernel_st = 1; 1058 eval(); 1059 } 1060 { 1061 kernel_st = 2; 1062 update_channels(); 1063 } 1064 { 1065 kernel_st = 3; 1066 fire_delta_events(); 1067 activate_threads(); 1068 reset_delta_events(); 1069 } 1070 { 1071 tmp = exists_runnable_thread(); 1072 } 1073 if (tmp == 0) { 1074 { 1075 kernel_st = 4; 1076 fire_time_events(); 1077 activate_threads(); 1078 reset_time_events(); 1079 } 1080 } else { 1081 1082 } 1083 { 1084 tmp___0 = stop_simulation(); 1085 } 1086 if (tmp___0) { 1087 goto while_8_break; 1088 } else { 1089 1090 } 1091 } 1092 while_8_break: /* CIL Label */ ; 1093 } 1094 1095 return; 1096} 1097} 1098int main(void) 1099{ int __retres1 ; 1100 1101 { 1102 { 1103 init_model(); 1104 start_simulation(); 1105 } 1106 __retres1 = 0; 1107 return (__retres1); 1108} 1109}