Showing error 2307

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.08_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 t7_pc  =    0;
  21int t8_pc  =    0;
  22int m_st  ;
  23int t1_st  ;
  24int t2_st  ;
  25int t3_st  ;
  26int t4_st  ;
  27int t5_st  ;
  28int t6_st  ;
  29int t7_st  ;
  30int t8_st  ;
  31int m_i  ;
  32int t1_i  ;
  33int t2_i  ;
  34int t3_i  ;
  35int t4_i  ;
  36int t5_i  ;
  37int t6_i  ;
  38int t7_i  ;
  39int t8_i  ;
  40int M_E  =    2;
  41int T1_E  =    2;
  42int T2_E  =    2;
  43int T3_E  =    2;
  44int T4_E  =    2;
  45int T5_E  =    2;
  46int T6_E  =    2;
  47int T7_E  =    2;
  48int T8_E  =    2;
  49int E_M  =    2;
  50int E_1  =    2;
  51int E_2  =    2;
  52int E_3  =    2;
  53int E_4  =    2;
  54int E_5  =    2;
  55int E_6  =    2;
  56int E_7  =    2;
  57int E_8  =    2;
  58int is_master_triggered(void) ;
  59int is_transmit1_triggered(void) ;
  60int is_transmit2_triggered(void) ;
  61int is_transmit3_triggered(void) ;
  62int is_transmit4_triggered(void) ;
  63int is_transmit5_triggered(void) ;
  64int is_transmit6_triggered(void) ;
  65int is_transmit7_triggered(void) ;
  66int is_transmit8_triggered(void) ;
  67void immediate_notify(void) ;
  68int token  ;
  69int __VERIFIER_nondet_int()  ;
  70int local  ;
  71void master(void) 
  72{ 
  73int tmp_var ;
  74  {
  75  if (m_pc == 0) {
  76    goto M_ENTRY;
  77  } else {
  78    if (m_pc == 1) {
  79      goto M_WAIT;
  80    } else {
  81
  82    }
  83  }
  84  M_ENTRY: ;
  85  {
  86  while (1) {
  87    while_0_continue: /* CIL Label */ ;
  88    {
  89    token = __VERIFIER_nondet_int();
  90    local = token;
  91    E_1 = 1;
  92    immediate_notify();
  93    E_1 = 2;
  94    m_pc = 1;
  95    m_st = 2;
  96    }
  97
  98    goto return_label;
  99    M_WAIT: ;
 100    if (token != local + 8) {
 101      {
 102      error();
 103      }
 104    } else {
 105       if(tmp_var <= 5){
 106           if(tmp_var >= 5){
 107             
 108           }
 109        }
 110
 111        if(tmp_var <= 5){
 112           if(tmp_var >= 5){
 113             if(tmp_var == 5){
 114             error();
 115             }
 116          }
 117        }
 118    }
 119  }
 120  while_0_break: /* CIL Label */ ;
 121  }
 122
 123  return_label: /* CIL Label */ 
 124  return;
 125}
 126}
 127void transmit1(void) 
 128{ 
 129
 130  {
 131  if (t1_pc == 0) {
 132    goto T1_ENTRY;
 133  } else {
 134    if (t1_pc == 1) {
 135      goto T1_WAIT;
 136    } else {
 137
 138    }
 139  }
 140  T1_ENTRY: ;
 141  {
 142  while (1) {
 143    while_1_continue: /* CIL Label */ ;
 144    t1_pc = 1;
 145    t1_st = 2;
 146
 147    goto return_label;
 148    T1_WAIT: 
 149    {
 150    token += 1;
 151    E_2 = 1;
 152    immediate_notify();
 153    E_2 = 2;
 154    }
 155  }
 156  while_1_break: /* CIL Label */ ;
 157  }
 158
 159  return_label: /* CIL Label */ 
 160  return;
 161}
 162}
 163void transmit2(void) 
 164{ 
 165
 166  {
 167  if (t2_pc == 0) {
 168    goto T2_ENTRY;
 169  } else {
 170    if (t2_pc == 1) {
 171      goto T2_WAIT;
 172    } else {
 173
 174    }
 175  }
 176  T2_ENTRY: ;
 177  {
 178  while (1) {
 179    while_2_continue: /* CIL Label */ ;
 180    t2_pc = 1;
 181    t2_st = 2;
 182
 183    goto return_label;
 184    T2_WAIT: 
 185    {
 186    token += 1;
 187    E_3 = 1;
 188    immediate_notify();
 189    E_3 = 2;
 190    }
 191  }
 192  while_2_break: /* CIL Label */ ;
 193  }
 194
 195  return_label: /* CIL Label */ 
 196  return;
 197}
 198}
 199void transmit3(void) 
 200{ 
 201
 202  {
 203  if (t3_pc == 0) {
 204    goto T3_ENTRY;
 205  } else {
 206    if (t3_pc == 1) {
 207      goto T3_WAIT;
 208    } else {
 209
 210    }
 211  }
 212  T3_ENTRY: ;
 213  {
 214  while (1) {
 215    while_3_continue: /* CIL Label */ ;
 216    t3_pc = 1;
 217    t3_st = 2;
 218
 219    goto return_label;
 220    T3_WAIT: 
 221    {
 222    token += 1;
 223    E_4 = 1;
 224    immediate_notify();
 225    E_4 = 2;
 226    }
 227  }
 228  while_3_break: /* CIL Label */ ;
 229  }
 230
 231  return_label: /* CIL Label */ 
 232  return;
 233}
 234}
 235void transmit4(void) 
 236{ 
 237
 238  {
 239  if (t4_pc == 0) {
 240    goto T4_ENTRY;
 241  } else {
 242    if (t4_pc == 1) {
 243      goto T4_WAIT;
 244    } else {
 245
 246    }
 247  }
 248  T4_ENTRY: ;
 249  {
 250  while (1) {
 251    while_4_continue: /* CIL Label */ ;
 252    t4_pc = 1;
 253    t4_st = 2;
 254
 255    goto return_label;
 256    T4_WAIT: 
 257    {
 258    token += 1;
 259    E_5 = 1;
 260    immediate_notify();
 261    E_5 = 2;
 262    }
 263  }
 264  while_4_break: /* CIL Label */ ;
 265  }
 266
 267  return_label: /* CIL Label */ 
 268  return;
 269}
 270}
 271void transmit5(void) 
 272{ 
 273
 274  {
 275  if (t5_pc == 0) {
 276    goto T5_ENTRY;
 277  } else {
 278    if (t5_pc == 1) {
 279      goto T5_WAIT;
 280    } else {
 281
 282    }
 283  }
 284  T5_ENTRY: ;
 285  {
 286  while (1) {
 287    while_5_continue: /* CIL Label */ ;
 288    t5_pc = 1;
 289    t5_st = 2;
 290
 291    goto return_label;
 292    T5_WAIT: 
 293    {
 294    token += 1;
 295    E_6 = 1;
 296    immediate_notify();
 297    E_6 = 2;
 298    }
 299  }
 300  while_5_break: /* CIL Label */ ;
 301  }
 302
 303  return_label: /* CIL Label */ 
 304  return;
 305}
 306}
 307void transmit6(void) 
 308{ 
 309
 310  {
 311  if (t6_pc == 0) {
 312    goto T6_ENTRY;
 313  } else {
 314    if (t6_pc == 1) {
 315      goto T6_WAIT;
 316    } else {
 317
 318    }
 319  }
 320  T6_ENTRY: ;
 321  {
 322  while (1) {
 323    while_6_continue: /* CIL Label */ ;
 324    t6_pc = 1;
 325    t6_st = 2;
 326
 327    goto return_label;
 328    T6_WAIT: 
 329    {
 330    token += 1;
 331    E_7 = 1;
 332    immediate_notify();
 333    E_7 = 2;
 334    }
 335  }
 336  while_6_break: /* CIL Label */ ;
 337  }
 338
 339  return_label: /* CIL Label */ 
 340  return;
 341}
 342}
 343void transmit7(void) 
 344{ 
 345
 346  {
 347  if (t7_pc == 0) {
 348    goto T7_ENTRY;
 349  } else {
 350    if (t7_pc == 1) {
 351      goto T7_WAIT;
 352    } else {
 353
 354    }
 355  }
 356  T7_ENTRY: ;
 357  {
 358  while (1) {
 359    while_7_continue: /* CIL Label */ ;
 360    t7_pc = 1;
 361    t7_st = 2;
 362
 363    goto return_label;
 364    T7_WAIT: 
 365    {
 366    token += 1;
 367    E_8 = 1;
 368    immediate_notify();
 369    E_8 = 2;
 370    }
 371  }
 372  while_7_break: /* CIL Label */ ;
 373  }
 374
 375  return_label: /* CIL Label */ 
 376  return;
 377}
 378}
 379void transmit8(void) 
 380{ 
 381
 382  {
 383  if (t8_pc == 0) {
 384    goto T8_ENTRY;
 385  } else {
 386    if (t8_pc == 1) {
 387      goto T8_WAIT;
 388    } else {
 389
 390    }
 391  }
 392  T8_ENTRY: ;
 393  {
 394  while (1) {
 395    while_8_continue: /* CIL Label */ ;
 396    t8_pc = 1;
 397    t8_st = 2;
 398
 399    goto return_label;
 400    T8_WAIT: 
 401    {
 402    token += 1;
 403    E_M = 1;
 404    immediate_notify();
 405    E_M = 2;
 406    }
 407  }
 408  while_8_break: /* CIL Label */ ;
 409  }
 410
 411  return_label: /* CIL Label */ 
 412  return;
 413}
 414}
 415int is_master_triggered(void) 
 416{ int __retres1 ;
 417
 418  {
 419  if (m_pc == 1) {
 420    if (E_M == 1) {
 421      __retres1 = 1;
 422      goto return_label;
 423    } else {
 424
 425    }
 426  } else {
 427
 428  }
 429  __retres1 = 0;
 430  return_label: /* CIL Label */ 
 431  return (__retres1);
 432}
 433}
 434int is_transmit1_triggered(void) 
 435{ int __retres1 ;
 436
 437  {
 438  if (t1_pc == 1) {
 439    if (E_1 == 1) {
 440      __retres1 = 1;
 441      goto return_label;
 442    } else {
 443
 444    }
 445  } else {
 446
 447  }
 448  __retres1 = 0;
 449  return_label: /* CIL Label */ 
 450  return (__retres1);
 451}
 452}
 453int is_transmit2_triggered(void) 
 454{ int __retres1 ;
 455
 456  {
 457  if (t2_pc == 1) {
 458    if (E_2 == 1) {
 459      __retres1 = 1;
 460      goto return_label;
 461    } else {
 462
 463    }
 464  } else {
 465
 466  }
 467  __retres1 = 0;
 468  return_label: /* CIL Label */ 
 469  return (__retres1);
 470}
 471}
 472int is_transmit3_triggered(void) 
 473{ int __retres1 ;
 474
 475  {
 476  if (t3_pc == 1) {
 477    if (E_3 == 1) {
 478      __retres1 = 1;
 479      goto return_label;
 480    } else {
 481
 482    }
 483  } else {
 484
 485  }
 486  __retres1 = 0;
 487  return_label: /* CIL Label */ 
 488  return (__retres1);
 489}
 490}
 491int is_transmit4_triggered(void) 
 492{ int __retres1 ;
 493
 494  {
 495  if (t4_pc == 1) {
 496    if (E_4 == 1) {
 497      __retres1 = 1;
 498      goto return_label;
 499    } else {
 500
 501    }
 502  } else {
 503
 504  }
 505  __retres1 = 0;
 506  return_label: /* CIL Label */ 
 507  return (__retres1);
 508}
 509}
 510int is_transmit5_triggered(void) 
 511{ int __retres1 ;
 512
 513  {
 514  if (t5_pc == 1) {
 515    if (E_5 == 1) {
 516      __retres1 = 1;
 517      goto return_label;
 518    } else {
 519
 520    }
 521  } else {
 522
 523  }
 524  __retres1 = 0;
 525  return_label: /* CIL Label */ 
 526  return (__retres1);
 527}
 528}
 529int is_transmit6_triggered(void) 
 530{ int __retres1 ;
 531
 532  {
 533  if (t6_pc == 1) {
 534    if (E_6 == 1) {
 535      __retres1 = 1;
 536      goto return_label;
 537    } else {
 538
 539    }
 540  } else {
 541
 542  }
 543  __retres1 = 0;
 544  return_label: /* CIL Label */ 
 545  return (__retres1);
 546}
 547}
 548int is_transmit7_triggered(void) 
 549{ int __retres1 ;
 550
 551  {
 552  if (t7_pc == 1) {
 553    if (E_7 == 1) {
 554      __retres1 = 1;
 555      goto return_label;
 556    } else {
 557
 558    }
 559  } else {
 560
 561  }
 562  __retres1 = 0;
 563  return_label: /* CIL Label */ 
 564  return (__retres1);
 565}
 566}
 567int is_transmit8_triggered(void) 
 568{ int __retres1 ;
 569
 570  {
 571  if (t8_pc == 1) {
 572    if (E_8 == 1) {
 573      __retres1 = 1;
 574      goto return_label;
 575    } else {
 576
 577    }
 578  } else {
 579
 580  }
 581  __retres1 = 0;
 582  return_label: /* CIL Label */ 
 583  return (__retres1);
 584}
 585}
 586void update_channels(void) 
 587{ 
 588
 589  {
 590
 591  return;
 592}
 593}
 594void init_threads(void) 
 595{ 
 596
 597  {
 598  if (m_i == 1) {
 599    m_st = 0;
 600  } else {
 601    m_st = 2;
 602  }
 603  if (t1_i == 1) {
 604    t1_st = 0;
 605  } else {
 606    t1_st = 2;
 607  }
 608  if (t2_i == 1) {
 609    t2_st = 0;
 610  } else {
 611    t2_st = 2;
 612  }
 613  if (t3_i == 1) {
 614    t3_st = 0;
 615  } else {
 616    t3_st = 2;
 617  }
 618  if (t4_i == 1) {
 619    t4_st = 0;
 620  } else {
 621    t4_st = 2;
 622  }
 623  if (t5_i == 1) {
 624    t5_st = 0;
 625  } else {
 626    t5_st = 2;
 627  }
 628  if (t6_i == 1) {
 629    t6_st = 0;
 630  } else {
 631    t6_st = 2;
 632  }
 633  if (t7_i == 1) {
 634    t7_st = 0;
 635  } else {
 636    t7_st = 2;
 637  }
 638  if (t8_i == 1) {
 639    t8_st = 0;
 640  } else {
 641    t8_st = 2;
 642  }
 643
 644  return;
 645}
 646}
 647int exists_runnable_thread(void) 
 648{ int __retres1 ;
 649
 650  {
 651  if (m_st == 0) {
 652    __retres1 = 1;
 653    goto return_label;
 654  } else {
 655    if (t1_st == 0) {
 656      __retres1 = 1;
 657      goto return_label;
 658    } else {
 659      if (t2_st == 0) {
 660        __retres1 = 1;
 661        goto return_label;
 662      } else {
 663        if (t3_st == 0) {
 664          __retres1 = 1;
 665          goto return_label;
 666        } else {
 667          if (t4_st == 0) {
 668            __retres1 = 1;
 669            goto return_label;
 670          } else {
 671            if (t5_st == 0) {
 672              __retres1 = 1;
 673              goto return_label;
 674            } else {
 675              if (t6_st == 0) {
 676                __retres1 = 1;
 677                goto return_label;
 678              } else {
 679                if (t7_st == 0) {
 680                  __retres1 = 1;
 681                  goto return_label;
 682                } else {
 683                  if (t8_st == 0) {
 684                    __retres1 = 1;
 685                    goto return_label;
 686                  } else {
 687
 688                  }
 689                }
 690              }
 691            }
 692          }
 693        }
 694      }
 695    }
 696  }
 697  __retres1 = 0;
 698  return_label: /* CIL Label */ 
 699  return (__retres1);
 700}
 701}
 702void eval(void) 
 703{
 704  int tmp ;
 705
 706  {
 707  {
 708  while (1) {
 709    while_9_continue: /* CIL Label */ ;
 710    {
 711    tmp = exists_runnable_thread();
 712    }
 713    if (tmp) {
 714
 715    } else {
 716      goto while_9_break;
 717    }
 718    if (m_st == 0) {
 719      int tmp_ndt_1;
 720      tmp_ndt_1 = __VERIFIER_nondet_int();
 721      if (tmp_ndt_1) {
 722        {
 723        m_st = 1;
 724        master();
 725        }
 726      } else {
 727
 728      }
 729    } else {
 730
 731    }
 732    if (t1_st == 0) {
 733      int tmp_ndt_2;
 734      tmp_ndt_2 = __VERIFIER_nondet_int();
 735      if (tmp_ndt_2) {
 736        {
 737        t1_st = 1;
 738        transmit1();
 739        }
 740      } else {
 741
 742      }
 743    } else {
 744
 745    }
 746    if (t2_st == 0) {
 747      int tmp_ndt_3;
 748      tmp_ndt_3 = __VERIFIER_nondet_int();
 749      if (tmp_ndt_3) {
 750        {
 751        t2_st = 1;
 752        transmit2();
 753        }
 754      } else {
 755
 756      }
 757    } else {
 758
 759    }
 760    if (t3_st == 0) {
 761      int tmp_ndt_4;
 762      tmp_ndt_4 = __VERIFIER_nondet_int();
 763      if (tmp_ndt_4) {
 764        {
 765        t3_st = 1;
 766        transmit3();
 767        }
 768      } else {
 769
 770      }
 771    } else {
 772
 773    }
 774    if (t4_st == 0) {
 775      int tmp_ndt_5;
 776      tmp_ndt_5 = __VERIFIER_nondet_int();
 777      if (tmp_ndt_5) {
 778        {
 779        t4_st = 1;
 780        transmit4();
 781        }
 782      } else {
 783
 784      }
 785    } else {
 786
 787    }
 788    if (t5_st == 0) {
 789      int tmp_ndt_6;
 790      tmp_ndt_6 = __VERIFIER_nondet_int();
 791      if (tmp_ndt_6) {
 792        {
 793        t5_st = 1;
 794        transmit5();
 795        }
 796      } else {
 797
 798      }
 799    } else {
 800
 801    }
 802    if (t6_st == 0) {
 803      int tmp_ndt_7;
 804      tmp_ndt_7 = __VERIFIER_nondet_int();
 805      if (tmp_ndt_7) {
 806        {
 807        t6_st = 1;
 808        transmit6();
 809        }
 810      } else {
 811
 812      }
 813    } else {
 814
 815    }
 816    if (t7_st == 0) {
 817      int tmp_ndt_8;
 818      tmp_ndt_8 = __VERIFIER_nondet_int();
 819      if (tmp_ndt_8) {
 820        {
 821        t7_st = 1;
 822        transmit7();
 823        }
 824      } else {
 825
 826      }
 827    } else {
 828
 829    }
 830    if (t8_st == 0) {
 831      int tmp_ndt_9;
 832      tmp_ndt_9 = __VERIFIER_nondet_int();
 833      if (tmp_ndt_9) {
 834        {
 835        t8_st = 1;
 836        transmit8();
 837        }
 838      } else {
 839
 840      }
 841    } else {
 842
 843    }
 844  }
 845  while_9_break: /* CIL Label */ ;
 846  }
 847
 848  return;
 849}
 850}
 851void fire_delta_events(void) 
 852{ 
 853
 854  {
 855  if (M_E == 0) {
 856    M_E = 1;
 857  } else {
 858
 859  }
 860  if (T1_E == 0) {
 861    T1_E = 1;
 862  } else {
 863
 864  }
 865  if (T2_E == 0) {
 866    T2_E = 1;
 867  } else {
 868
 869  }
 870  if (T3_E == 0) {
 871    T3_E = 1;
 872  } else {
 873
 874  }
 875  if (T4_E == 0) {
 876    T4_E = 1;
 877  } else {
 878
 879  }
 880  if (T5_E == 0) {
 881    T5_E = 1;
 882  } else {
 883
 884  }
 885  if (T6_E == 0) {
 886    T6_E = 1;
 887  } else {
 888
 889  }
 890  if (T7_E == 0) {
 891    T7_E = 1;
 892  } else {
 893
 894  }
 895  if (T8_E == 0) {
 896    T8_E = 1;
 897  } else {
 898
 899  }
 900  if (E_M == 0) {
 901    E_M = 1;
 902  } else {
 903
 904  }
 905  if (E_1 == 0) {
 906    E_1 = 1;
 907  } else {
 908
 909  }
 910  if (E_2 == 0) {
 911    E_2 = 1;
 912  } else {
 913
 914  }
 915  if (E_3 == 0) {
 916    E_3 = 1;
 917  } else {
 918
 919  }
 920  if (E_4 == 0) {
 921    E_4 = 1;
 922  } else {
 923
 924  }
 925  if (E_5 == 0) {
 926    E_5 = 1;
 927  } else {
 928
 929  }
 930  if (E_6 == 0) {
 931    E_6 = 1;
 932  } else {
 933
 934  }
 935  if (E_7 == 0) {
 936    E_7 = 1;
 937  } else {
 938
 939  }
 940  if (E_8 == 0) {
 941    E_8 = 1;
 942  } else {
 943
 944  }
 945
 946  return;
 947}
 948}
 949void reset_delta_events(void) 
 950{ 
 951
 952  {
 953  if (M_E == 1) {
 954    M_E = 2;
 955  } else {
 956
 957  }
 958  if (T1_E == 1) {
 959    T1_E = 2;
 960  } else {
 961
 962  }
 963  if (T2_E == 1) {
 964    T2_E = 2;
 965  } else {
 966
 967  }
 968  if (T3_E == 1) {
 969    T3_E = 2;
 970  } else {
 971
 972  }
 973  if (T4_E == 1) {
 974    T4_E = 2;
 975  } else {
 976
 977  }
 978  if (T5_E == 1) {
 979    T5_E = 2;
 980  } else {
 981
 982  }
 983  if (T6_E == 1) {
 984    T6_E = 2;
 985  } else {
 986
 987  }
 988  if (T7_E == 1) {
 989    T7_E = 2;
 990  } else {
 991
 992  }
 993  if (T8_E == 1) {
 994    T8_E = 2;
 995  } else {
 996
 997  }
 998  if (E_M == 1) {
 999    E_M = 2;
1000  } else {
1001
1002  }
1003  if (E_1 == 1) {
1004    E_1 = 2;
1005  } else {
1006
1007  }
1008  if (E_2 == 1) {
1009    E_2 = 2;
1010  } else {
1011
1012  }
1013  if (E_3 == 1) {
1014    E_3 = 2;
1015  } else {
1016
1017  }
1018  if (E_4 == 1) {
1019    E_4 = 2;
1020  } else {
1021
1022  }
1023  if (E_5 == 1) {
1024    E_5 = 2;
1025  } else {
1026
1027  }
1028  if (E_6 == 1) {
1029    E_6 = 2;
1030  } else {
1031
1032  }
1033  if (E_7 == 1) {
1034    E_7 = 2;
1035  } else {
1036
1037  }
1038  if (E_8 == 1) {
1039    E_8 = 2;
1040  } else {
1041
1042  }
1043
1044  return;
1045}
1046}
1047void activate_threads(void) 
1048{ int tmp ;
1049  int tmp___0 ;
1050  int tmp___1 ;
1051  int tmp___2 ;
1052  int tmp___3 ;
1053  int tmp___4 ;
1054  int tmp___5 ;
1055  int tmp___6 ;
1056  int tmp___7 ;
1057
1058  {
1059  {
1060  tmp = is_master_triggered();
1061  }
1062  if (tmp) {
1063    m_st = 0;
1064  } else {
1065
1066  }
1067  {
1068  tmp___0 = is_transmit1_triggered();
1069  }
1070  if (tmp___0) {
1071    t1_st = 0;
1072  } else {
1073
1074  }
1075  {
1076  tmp___1 = is_transmit2_triggered();
1077  }
1078  if (tmp___1) {
1079    t2_st = 0;
1080  } else {
1081
1082  }
1083  {
1084  tmp___2 = is_transmit3_triggered();
1085  }
1086  if (tmp___2) {
1087    t3_st = 0;
1088  } else {
1089
1090  }
1091  {
1092  tmp___3 = is_transmit4_triggered();
1093  }
1094  if (tmp___3) {
1095    t4_st = 0;
1096  } else {
1097
1098  }
1099  {
1100  tmp___4 = is_transmit5_triggered();
1101  }
1102  if (tmp___4) {
1103    t5_st = 0;
1104  } else {
1105
1106  }
1107  {
1108  tmp___5 = is_transmit6_triggered();
1109  }
1110  if (tmp___5) {
1111    t6_st = 0;
1112  } else {
1113
1114  }
1115  {
1116  tmp___6 = is_transmit7_triggered();
1117  }
1118  if (tmp___6) {
1119    t7_st = 0;
1120  } else {
1121
1122  }
1123  {
1124  tmp___7 = is_transmit8_triggered();
1125  }
1126  if (tmp___7) {
1127    t8_st = 0;
1128  } else {
1129
1130  }
1131
1132  return;
1133}
1134}
1135void immediate_notify(void) 
1136{ 
1137
1138  {
1139  {
1140  activate_threads();
1141  }
1142
1143  return;
1144}
1145}
1146void fire_time_events(void) 
1147{ 
1148
1149  {
1150  M_E = 1;
1151
1152  return;
1153}
1154}
1155void reset_time_events(void) 
1156{ 
1157
1158  {
1159  if (M_E == 1) {
1160    M_E = 2;
1161  } else {
1162
1163  }
1164  if (T1_E == 1) {
1165    T1_E = 2;
1166  } else {
1167
1168  }
1169  if (T2_E == 1) {
1170    T2_E = 2;
1171  } else {
1172
1173  }
1174  if (T3_E == 1) {
1175    T3_E = 2;
1176  } else {
1177
1178  }
1179  if (T4_E == 1) {
1180    T4_E = 2;
1181  } else {
1182
1183  }
1184  if (T5_E == 1) {
1185    T5_E = 2;
1186  } else {
1187
1188  }
1189  if (T6_E == 1) {
1190    T6_E = 2;
1191  } else {
1192
1193  }
1194  if (T7_E == 1) {
1195    T7_E = 2;
1196  } else {
1197
1198  }
1199  if (T8_E == 1) {
1200    T8_E = 2;
1201  } else {
1202
1203  }
1204  if (E_M == 1) {
1205    E_M = 2;
1206  } else {
1207
1208  }
1209  if (E_1 == 1) {
1210    E_1 = 2;
1211  } else {
1212
1213  }
1214  if (E_2 == 1) {
1215    E_2 = 2;
1216  } else {
1217
1218  }
1219  if (E_3 == 1) {
1220    E_3 = 2;
1221  } else {
1222
1223  }
1224  if (E_4 == 1) {
1225    E_4 = 2;
1226  } else {
1227
1228  }
1229  if (E_5 == 1) {
1230    E_5 = 2;
1231  } else {
1232
1233  }
1234  if (E_6 == 1) {
1235    E_6 = 2;
1236  } else {
1237
1238  }
1239  if (E_7 == 1) {
1240    E_7 = 2;
1241  } else {
1242
1243  }
1244  if (E_8 == 1) {
1245    E_8 = 2;
1246  } else {
1247
1248  }
1249
1250  return;
1251}
1252}
1253void init_model(void) 
1254{ 
1255
1256  {
1257  m_i = 1;
1258  t1_i = 1;
1259  t2_i = 1;
1260  t3_i = 1;
1261  t4_i = 1;
1262  t5_i = 1;
1263  t6_i = 1;
1264  t7_i = 1;
1265  t8_i = 1;
1266
1267  return;
1268}
1269}
1270int stop_simulation(void) 
1271{ int tmp ;
1272  int __retres2 ;
1273
1274  {
1275  {
1276  tmp = exists_runnable_thread();
1277  }
1278  if (tmp) {
1279    __retres2 = 0;
1280    goto return_label;
1281  } else {
1282
1283  }
1284  __retres2 = 1;
1285  return_label: /* CIL Label */ 
1286  return (__retres2);
1287}
1288}
1289void start_simulation(void) 
1290{ int kernel_st ;
1291  int tmp ;
1292  int tmp___0 ;
1293
1294  {
1295  {
1296  kernel_st = 0;
1297  update_channels();
1298  init_threads();
1299  fire_delta_events();
1300  activate_threads();
1301  reset_delta_events();
1302  }
1303  {
1304  while (1) {
1305    while_10_continue: /* CIL Label */ ;
1306    {
1307    kernel_st = 1;
1308    eval();
1309    }
1310    {
1311    kernel_st = 2;
1312    update_channels();
1313    }
1314    {
1315    kernel_st = 3;
1316    fire_delta_events();
1317    activate_threads();
1318    reset_delta_events();
1319    }
1320    {
1321    tmp = exists_runnable_thread();
1322    }
1323    if (tmp == 0) {
1324      {
1325      kernel_st = 4;
1326      fire_time_events();
1327      activate_threads();
1328      reset_time_events();
1329      }
1330    } else {
1331
1332    }
1333    {
1334    tmp___0 = stop_simulation();
1335    }
1336    if (tmp___0) {
1337      goto while_10_break;
1338    } else {
1339
1340    }
1341  }
1342  while_10_break: /* CIL Label */ ;
1343  }
1344
1345  return;
1346}
1347}
1348int main(void) 
1349{ int __retres1 ;
1350
1351  {
1352  {
1353  init_model();
1354  start_simulation();
1355  }
1356  __retres1 = 0;
1357  return (__retres1);
1358}
1359}
↑