Showing error 277

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