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