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