Showing error 2302

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

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