Showing error 2328

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.06_unsafe.cil.c
Line in file: 9
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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