Showing error 2303

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_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

Source: 

   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{
 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}
↑