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.04_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 m_st ; 19int t1_st ; 20int t2_st ; 21int t3_st ; 22int t4_st ; 23int m_i ; 24int t1_i ; 25int t2_i ; 26int t3_i ; 27int t4_i ; 28int M_E = 2; 29int T1_E = 2; 30int T2_E = 2; 31int T3_E = 2; 32int T4_E = 2; 33int E_M = 2; 34int E_1 = 2; 35int E_2 = 2; 36int E_3 = 2; 37int E_4 = 2; 38int is_master_triggered(void) ; 39int is_transmit1_triggered(void) ; 40int is_transmit2_triggered(void) ; 41int is_transmit3_triggered(void) ; 42int is_transmit4_triggered(void) ; 43void immediate_notify(void) ; 44int token ; 45int __VERIFIER_nondet_int() ; 46int local ; 47void master(void) 48{ 49 50 { 51 if (m_pc == 0) { 52 goto M_ENTRY; 53 } else { 54 if (m_pc == 1) { 55 goto M_WAIT; 56 } else { 57 58 } 59 } 60 M_ENTRY: ; 61 { 62 while (1) { 63 while_0_continue: /* CIL Label */ ; 64 { 65 token = __VERIFIER_nondet_int(); 66 local = token; 67 E_1 = 1; 68 immediate_notify(); 69 E_1 = 2; 70 m_pc = 1; 71 m_st = 2; 72 } 73 74 goto return_label; 75 M_WAIT: ; 76 if (token != local + 4) { 77 { 78 error(); 79 } 80 } else { 81 82 } 83 } 84 while_0_break: /* CIL Label */ ; 85 } 86 87 return_label: /* CIL Label */ 88 return; 89} 90} 91void transmit1(void) 92{ 93 94 { 95 if (t1_pc == 0) { 96 goto T1_ENTRY; 97 } else { 98 if (t1_pc == 1) { 99 goto T1_WAIT; 100 } else { 101 102 } 103 } 104 T1_ENTRY: ; 105 { 106 while (1) { 107 while_1_continue: /* CIL Label */ ; 108 t1_pc = 1; 109 t1_st = 2; 110 111 goto return_label; 112 T1_WAIT: 113 { 114 token += 1; 115 E_2 = 1; 116 immediate_notify(); 117 E_2 = 2; 118 } 119 } 120 while_1_break: /* CIL Label */ ; 121 } 122 123 return_label: /* CIL Label */ 124 return; 125} 126} 127void transmit2(void) 128{ 129 130 { 131 if (t2_pc == 0) { 132 goto T2_ENTRY; 133 } else { 134 if (t2_pc == 1) { 135 goto T2_WAIT; 136 } else { 137 138 } 139 } 140 T2_ENTRY: ; 141 { 142 while (1) { 143 while_2_continue: /* CIL Label */ ; 144 t2_pc = 1; 145 t2_st = 2; 146 147 goto return_label; 148 T2_WAIT: 149 { 150 token += 1; 151 E_3 = 1; 152 immediate_notify(); 153 E_3 = 2; 154 } 155 } 156 while_2_break: /* CIL Label */ ; 157 } 158 159 return_label: /* CIL Label */ 160 return; 161} 162} 163void transmit3(void) 164{ 165 166 { 167 if (t3_pc == 0) { 168 goto T3_ENTRY; 169 } else { 170 if (t3_pc == 1) { 171 goto T3_WAIT; 172 } else { 173 174 } 175 } 176 T3_ENTRY: ; 177 { 178 while (1) { 179 while_3_continue: /* CIL Label */ ; 180 t3_pc = 1; 181 t3_st = 2; 182 183 goto return_label; 184 T3_WAIT: 185 { 186 token += 1; 187 E_4 = 1; 188 immediate_notify(); 189 E_4 = 2; 190 } 191 } 192 while_3_break: /* CIL Label */ ; 193 } 194 195 return_label: /* CIL Label */ 196 return; 197} 198} 199void transmit4(void) 200{ 201 202 { 203 if (t4_pc == 0) { 204 goto T4_ENTRY; 205 } else { 206 if (t4_pc == 1) { 207 goto T4_WAIT; 208 } else { 209 210 } 211 } 212 T4_ENTRY: ; 213 { 214 while (1) { 215 while_4_continue: /* CIL Label */ ; 216 t4_pc = 1; 217 t4_st = 2; 218 219 goto return_label; 220 T4_WAIT: 221 { 222 token += 1; 223 E_M = 1; 224 immediate_notify(); 225 E_M = 2; 226 } 227 } 228 while_4_break: /* CIL Label */ ; 229 } 230 231 return_label: /* CIL Label */ 232 return; 233} 234} 235int is_master_triggered(void) 236{ int __retres1 ; 237 238 { 239 if (m_pc == 1) { 240 if (E_M == 1) { 241 __retres1 = 1; 242 goto return_label; 243 } else { 244 245 } 246 } else { 247 248 } 249 __retres1 = 0; 250 return_label: /* CIL Label */ 251 return (__retres1); 252} 253} 254int is_transmit1_triggered(void) 255{ int __retres1 ; 256 257 { 258 if (t1_pc == 1) { 259 if (E_1 == 1) { 260 __retres1 = 1; 261 goto return_label; 262 } else { 263 264 } 265 } else { 266 267 } 268 __retres1 = 0; 269 return_label: /* CIL Label */ 270 return (__retres1); 271} 272} 273int is_transmit2_triggered(void) 274{ int __retres1 ; 275 276 { 277 if (t2_pc == 1) { 278 if (E_2 == 1) { 279 __retres1 = 1; 280 goto return_label; 281 } else { 282 283 } 284 } else { 285 286 } 287 __retres1 = 0; 288 return_label: /* CIL Label */ 289 return (__retres1); 290} 291} 292int is_transmit3_triggered(void) 293{ int __retres1 ; 294 295 { 296 if (t3_pc == 1) { 297 if (E_3 == 1) { 298 __retres1 = 1; 299 goto return_label; 300 } else { 301 302 } 303 } else { 304 305 } 306 __retres1 = 0; 307 return_label: /* CIL Label */ 308 return (__retres1); 309} 310} 311int is_transmit4_triggered(void) 312{ int __retres1 ; 313 314 { 315 if (t4_pc == 1) { 316 if (E_4 == 1) { 317 __retres1 = 1; 318 goto return_label; 319 } else { 320 321 } 322 } else { 323 324 } 325 __retres1 = 0; 326 return_label: /* CIL Label */ 327 return (__retres1); 328} 329} 330void update_channels(void) 331{ 332 333 { 334 335 return; 336} 337} 338void init_threads(void) 339{ 340 341 { 342 if (m_i == 1) { 343 m_st = 0; 344 } else { 345 m_st = 2; 346 } 347 if (t1_i == 1) { 348 t1_st = 0; 349 } else { 350 t1_st = 2; 351 } 352 if (t2_i == 1) { 353 t2_st = 0; 354 } else { 355 t2_st = 2; 356 } 357 if (t3_i == 1) { 358 t3_st = 0; 359 } else { 360 t3_st = 2; 361 } 362 if (t4_i == 1) { 363 t4_st = 0; 364 } else { 365 t4_st = 2; 366 } 367 368 return; 369} 370} 371int exists_runnable_thread(void) 372{ int __retres1 ; 373 374 { 375 if (m_st == 0) { 376 __retres1 = 1; 377 goto return_label; 378 } else { 379 if (t1_st == 0) { 380 __retres1 = 1; 381 goto return_label; 382 } else { 383 if (t2_st == 0) { 384 __retres1 = 1; 385 goto return_label; 386 } else { 387 if (t3_st == 0) { 388 __retres1 = 1; 389 goto return_label; 390 } else { 391 if (t4_st == 0) { 392 __retres1 = 1; 393 goto return_label; 394 } else { 395 396 } 397 } 398 } 399 } 400 } 401 __retres1 = 0; 402 return_label: /* CIL Label */ 403 return (__retres1); 404} 405} 406void eval(void) 407{ 408 int tmp ; 409 410 { 411 { 412 while (1) { 413 while_5_continue: /* CIL Label */ ; 414 { 415 tmp = exists_runnable_thread(); 416 } 417 if (tmp) { 418 419 } else { 420 goto while_5_break; 421 } 422 if (m_st == 0) { 423 int tmp_ndt_1; 424 tmp_ndt_1 = __VERIFIER_nondet_int(); 425 if (tmp_ndt_1) { 426 { 427 m_st = 1; 428 master(); 429 } 430 } else { 431 432 } 433 } else { 434 435 } 436 if (t1_st == 0) { 437 int tmp_ndt_2; 438 tmp_ndt_2 = __VERIFIER_nondet_int(); 439 if (tmp_ndt_2) { 440 { 441 t1_st = 1; 442 transmit1(); 443 } 444 } else { 445 446 } 447 } else { 448 449 } 450 if (t2_st == 0) { 451 int tmp_ndt_3; 452 tmp_ndt_3 = __VERIFIER_nondet_int(); 453 if (tmp_ndt_3) { 454 { 455 t2_st = 1; 456 transmit2(); 457 } 458 } else { 459 460 } 461 } else { 462 463 } 464 if (t3_st == 0) { 465 int tmp_ndt_4; 466 tmp_ndt_4 = __VERIFIER_nondet_int(); 467 if (tmp_ndt_4) { 468 { 469 t3_st = 1; 470 transmit3(); 471 } 472 } else { 473 474 } 475 } else { 476 477 } 478 if (t4_st == 0) { 479 int tmp_ndt_5; 480 tmp_ndt_5 = __VERIFIER_nondet_int(); 481 if (tmp_ndt_5) { 482 { 483 t4_st = 1; 484 transmit4(); 485 } 486 } else { 487 488 } 489 } else { 490 491 } 492 } 493 while_5_break: /* CIL Label */ ; 494 } 495 496 return; 497} 498} 499void fire_delta_events(void) 500{ 501 502 { 503 if (M_E == 0) { 504 M_E = 1; 505 } else { 506 507 } 508 if (T1_E == 0) { 509 T1_E = 1; 510 } else { 511 512 } 513 if (T2_E == 0) { 514 T2_E = 1; 515 } else { 516 517 } 518 if (T3_E == 0) { 519 T3_E = 1; 520 } else { 521 522 } 523 if (T4_E == 0) { 524 T4_E = 1; 525 } else { 526 527 } 528 if (E_M == 0) { 529 E_M = 1; 530 } else { 531 532 } 533 if (E_1 == 0) { 534 E_1 = 1; 535 } else { 536 537 } 538 if (E_2 == 0) { 539 E_2 = 1; 540 } else { 541 542 } 543 if (E_3 == 0) { 544 E_3 = 1; 545 } else { 546 547 } 548 if (E_4 == 0) { 549 E_4 = 1; 550 } else { 551 552 } 553 554 return; 555} 556} 557void reset_delta_events(void) 558{ 559 560 { 561 if (M_E == 1) { 562 M_E = 2; 563 } else { 564 565 } 566 if (T1_E == 1) { 567 T1_E = 2; 568 } else { 569 570 } 571 if (T2_E == 1) { 572 T2_E = 2; 573 } else { 574 575 } 576 if (T3_E == 1) { 577 T3_E = 2; 578 } else { 579 580 } 581 if (T4_E == 1) { 582 T4_E = 2; 583 } else { 584 585 } 586 if (E_M == 1) { 587 E_M = 2; 588 } else { 589 590 } 591 if (E_1 == 1) { 592 E_1 = 2; 593 } else { 594 595 } 596 if (E_2 == 1) { 597 E_2 = 2; 598 } else { 599 600 } 601 if (E_3 == 1) { 602 E_3 = 2; 603 } else { 604 605 } 606 if (E_4 == 1) { 607 E_4 = 2; 608 } else { 609 610 } 611 612 return; 613} 614} 615void activate_threads(void) 616{ int tmp ; 617 int tmp___0 ; 618 int tmp___1 ; 619 int tmp___2 ; 620 int tmp___3 ; 621 622 { 623 { 624 tmp = is_master_triggered(); 625 } 626 if (tmp) { 627 m_st = 0; 628 } else { 629 630 } 631 { 632 tmp___0 = is_transmit1_triggered(); 633 } 634 if (tmp___0) { 635 t1_st = 0; 636 } else { 637 638 } 639 { 640 tmp___1 = is_transmit2_triggered(); 641 } 642 if (tmp___1) { 643 t2_st = 0; 644 } else { 645 646 } 647 { 648 tmp___2 = is_transmit3_triggered(); 649 } 650 if (tmp___2) { 651 t3_st = 0; 652 } else { 653 654 } 655 { 656 tmp___3 = is_transmit4_triggered(); 657 } 658 if (tmp___3) { 659 t4_st = 0; 660 } else { 661 662 } 663 664 return; 665} 666} 667void immediate_notify(void) 668{ 669 670 { 671 { 672 activate_threads(); 673 } 674 675 return; 676} 677} 678void fire_time_events(void) 679{ 680 681 { 682 M_E = 1; 683 684 return; 685} 686} 687void reset_time_events(void) 688{ 689 690 { 691 if (M_E == 1) { 692 M_E = 2; 693 } else { 694 695 } 696 if (T1_E == 1) { 697 T1_E = 2; 698 } else { 699 700 } 701 if (T2_E == 1) { 702 T2_E = 2; 703 } else { 704 705 } 706 if (T3_E == 1) { 707 T3_E = 2; 708 } else { 709 710 } 711 if (T4_E == 1) { 712 T4_E = 2; 713 } else { 714 715 } 716 if (E_M == 1) { 717 E_M = 2; 718 } else { 719 720 } 721 if (E_1 == 1) { 722 E_1 = 2; 723 } else { 724 725 } 726 if (E_2 == 1) { 727 E_2 = 2; 728 } else { 729 730 } 731 if (E_3 == 1) { 732 E_3 = 2; 733 } else { 734 735 } 736 if (E_4 == 1) { 737 E_4 = 2; 738 } else { 739 740 } 741 742 return; 743} 744} 745void init_model(void) 746{ 747 748 { 749 m_i = 1; 750 t1_i = 1; 751 t2_i = 1; 752 t3_i = 1; 753 t4_i = 1; 754 755 return; 756} 757} 758int stop_simulation(void) 759{ int tmp ; 760 int __retres2 ; 761 762 { 763 { 764 tmp = exists_runnable_thread(); 765 } 766 if (tmp) { 767 __retres2 = 0; 768 goto return_label; 769 } else { 770 771 } 772 __retres2 = 1; 773 return_label: /* CIL Label */ 774 return (__retres2); 775} 776} 777void start_simulation(void) 778{ int kernel_st ; 779 int tmp ; 780 int tmp___0 ; 781 782 { 783 { 784 kernel_st = 0; 785 update_channels(); 786 init_threads(); 787 fire_delta_events(); 788 activate_threads(); 789 reset_delta_events(); 790 } 791 { 792 while (1) { 793 while_6_continue: /* CIL Label */ ; 794 { 795 kernel_st = 1; 796 eval(); 797 } 798 { 799 kernel_st = 2; 800 update_channels(); 801 } 802 { 803 kernel_st = 3; 804 fire_delta_events(); 805 activate_threads(); 806 reset_delta_events(); 807 } 808 { 809 tmp = exists_runnable_thread(); 810 } 811 if (tmp == 0) { 812 { 813 kernel_st = 4; 814 fire_time_events(); 815 activate_threads(); 816 reset_time_events(); 817 } 818 } else { 819 820 } 821 { 822 tmp___0 = stop_simulation(); 823 } 824 if (tmp___0) { 825 goto while_6_break; 826 } else { 827 828 } 829 } 830 while_6_break: /* CIL Label */ ; 831 } 832 833 return; 834} 835} 836int main(void) 837{ int __retres1 ; 838 839 { 840 { 841 init_model(); 842 start_simulation(); 843 } 844 __retres1 = 0; 845 return (__retres1); 846} 847}